userbox020/math-workflow

Fluxo de trabalho matemático

Resolva o problema declarado pelo usuário. Não o transforme em um amplo projeto de pesquisa.

Fluxo de trabalho

1. Reformule o problema e identifique seu domínio matemático. Determine se o usuário deseja uma prova, cálculo, consulta ao corpus ou verificação formal; esclareça apenas ambiguidades bloqueadoras.
2. Use math_search para manuscritos e estratégias relacionados. Comece amplo, depois restrinja por terminologia ou hipóteses. Use math_manuscript para ler apenas o resumo, esboço ou seção LaTeX relevante. Se o código-fonte TeX estiver ausente ou você precisar da redação publicada, use math_pdf_text em páginas selecionadas.
3. Para uma prova, forneça um plano de lemas antes da álgebra. Separe os resultados citados do corpus da nova derivação e verifique se as hipóteses de cada resultado citado se aplicam.
4. Para verificação formal solicitada ou uma declaração em Lean, use math_lean_search para localizar declarações existentes, math_lean_check em pequenos trechos primeiro, depois math_lean_build para o alvo focado. Use math_comparator apenas quando existir uma configuração de desafio correspondente. Não construa o pacote inteiro por padrão.
5. Para trabalho numérico ou simbólico, use math_compute para operações SymPy permitidas. Caso contrário, mostre o cálculo e indique a limitação de execução. Evidência numérica não é prova de uma afirmação exata.
6. Verifique de forma independente casos extremos, quantificadores, hipóteses e etapas intermediárias. Confirme se cada verificação Lean realmente passou e qual declaração ela verificou; um trecho não relacionado que passa não verifica o teorema solicitado.

Salvaguardas do corpus e verificação

• math/CONTENTS.md mapeia 721 manuscritos em 373 famílias de resultados. O arquivo contém resultados brutos de pesquisa, não resultados certificados independentemente.
• Atualmente 175 artigos possuem formalizações Lean; math/lean/formalization.yaml é o catálogo. A presença no catálogo não certifica todas as afirmações de um artigo.
• Verifique math/history.md quando um resultado parecer suspeito; ele registra revisões e retiradas. Não confie silenciosamente em um resultado retirado.
• Nunca afirme que um artigo está verificado simplesmente por estar no corpus.
• Nunca afirme verificação Lean a menos que a invocação relevante de math_lean_check, math_lean_build ou math_comparator tenha realmente sido bem-sucedida. Relate falhas, verificações ignoradas, pré-requisitos ausentes e lacunas remanescentes explicitamente.
• math/lean/ é o único pacote Lake OAI, fixado em leanprover/lean4:v4.34.1. Prefira alvos focados como OAI.Analysis.
• Use math_status para inspecionar a disponibilidade atual; não trate uma verificação indisponível como sucesso. Builds de Lean para Windows nativo podem ser bloqueados por um caminho NTFS inválido no conjunto de dependências fixado, e Comparator/landrun exigem Linux/WSL. Relate tais bloqueadores em vez de silenciosamente alterar as afirmações.
• Cite caminhos de origem relativos a math/, por exemplo lean/formalization.yaml, com identificadores de manuscrito e nomes de seção quando disponíveis.

Padrões de uso de ferramentas

• Consulte primeiro de forma ampla, depois restrinja; não realize descoberta em todo o repositório para uma questão localizada.
• Leia seções relevantes em vez de PDFs inteiros. Resolva caminhos de PDFs publicados a partir de metadados em vez de assumir um nome de arquivo; use math_pdf_text apenas para páginas selecionadas.
• Prefira math_grep para nomes ou notações exatas em TeX, Markdown e Lean; use math_lean_search para nomes de declarações. Escopo as pesquisas para arquivos ou diretórios relevantes quando possível.
• Use math_compute para verificações simbólicas, mas indique a operação e verifique a expressão retornada de forma independente.
• Mantenha a saída limitada: resuma correspondências e cite apenas as declarações ou etapas de prova necessárias.
• Use math_reindex após alterações em math/ quando o índice precisar ser atualizado.

Estrutura da resposta

1. Teorema / afirmação: declaração precisa, suposições e escopo.
2. Prova / derivação: plano de lemas e etapas justificadas, ou o cálculo ou consulta solicitada.
3. Status da verificação: verificações realmente executadas, resultados e limites de sua cobertura.
4. Fontes: caminhos e seções relevantes do corpus; distinga citações de trabalho novo.
5. Lacunas em aberto: etapas não resolvidas ou verificações ausentes, ou explicitamente nenhuma identificada.