MathCode: agente que formaliza matemática e prova teoremas em Lean

O que é

MathCode é um assistente de codificação para terminal com um mecanismo integrado de formalização matemática. O usuário descreve um problema em linguagem natural, e a ferramenta o converte em um teorema em Lean 4 e tenta produzir uma prova formal. O sistema combina o ambiente Lean 4, provas formais, Mathlib e recursos de agente para conduzir esse processo.

Como funciona

A ferramenta mantém um REPL persistente do Lean, permitindo realizar verificações de compilação em cerca de 0,4 segundo após um aquecimento inicial, em vez dos aproximadamente 30 segundos indicados para execuções sem essa persistência. Teoremas provados são nomeados automaticamente, armazenados e disponibilizados para importação, de modo que possam ser reutilizados pelo planejador e pelo provador.

MathCode também oferece uma biblioteca de axiomas para registrar suposições feitas durante a conversa como declarações persistentes em Lean. Essas declarações passam por verificação de compilação e revisão de consistência. Na busca por resultados já formalizados, a ferramenta consulta leansearch.net e Loogle para localizar lemas verificados da Mathlib e usa diagnósticos estruturados do LSP do Lean para orientar reparos.

Estratégias de prova e uso

Cada prova é tratada como uma sessão interativa: o agente escreve candidatos, lê os erros e recompila o código. Para teoremas complexos, o recurso Tree-of-Subgoals divide o problema em subobjetivos independentes, tenta prová-los em paralelo e depois os reúne. O sistema também executa vários planejadores simultaneamente para explorar estratégias diferentes, deixando que o provador escolha a abordagem considerada melhor.

As dependências entre teoremas e lemas podem ser visualizadas em um grafo de conhecimento gerado como um cofre do Obsidian. As formalizações são gravadas no diretório LeanFormalizations/, e há uma interface web opcional disponível pelo comando ./run webui.

Requisitos e origem

O projeto requer macOS em arquitetura arm64 ou Linux em x86_64, além da interface de linha de comando codex, usada como back-end padrão. A instalação clona o repositório, prepara o ambiente, baixa o tempo de execução e a cadeia de ferramentas do Lean e instala um lançador local. O projeto informa que seu fluxo de formalização e prova matemática é baseado no AUTOLEAN.