MathCode: Um Agente de Codificação Matemática com Formalização em Lean 4

MathCode é um assistente de codificação com IA baseado em terminal que formaliza e prova problemas matemáticos usando Lean 4. Em vez de escrever código Lean você mesmo, você fornece um problema em inglês simples, e ele gera um teorema e tenta uma prova, com um REPL persistente e uma biblioteca de teoremas reutilizáveis.

Recursos Principais

• REPL Lean Persistente: Após um aquecimento único, as verificações de compilação caem para ~0,4s (de ~30s).
• Biblioteca de Teoremas: Cada teorema provado é automaticamente nomeado, armazenado e importável para reutilização.
• Biblioteca de Axiomas: Armazene suposições conversacionais como declarações Lean persistentes e verificadas por compilação.
• Integração LSP Lean: Pesquisa em leansearch.net e Loogle por lemas Mathlib verificados, usa diagnósticos LSP estruturados para reparos.
• Grafo de Teoremas Obsidian: Gera um grafo de dependência visual dos teoremas e lemas no Obsidian.
• Prova em Modo Agente: Sessões interativas onde o agente itera sobre candidatos a prova com base em erros.
• Árvore de Subobjetivos: Decompõe teoremas complexos em subobjetivos independentes, prova-os em paralelo e depois os une.
• Multi-Planejador: Executa vários planejadores em paralelo para diversas estratégias de prova; o provador escolhe a melhor abordagem.

Início Rápido

Requer macOS (arm64) ou Linux (x86_64), além do CLI codex para o backend padrão.

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login

Teste com:

mathcode -p "prove que o quadrado de um número par é par"

As saídas são escritas em LeanFormalizations/. Uma interface web está disponível via ./run webui.

Esta ferramenta é destinada a matemáticos, pesquisadores e desenvolvedores que trabalham com verificação formal ou prova de teoremas assistida por IA.