MathCode: Un agente de codificación matemática con formalización en Lean 4

MathCode es un asistente de programación con IA para terminal que formaliza y demuestra problemas matemáticos usando Lean 4. En lugar de que escribas código Lean tú mismo, le das un problema en inglés sencillo, y genera un teorema e intenta una prueba, con un REPL persistente y una biblioteca de teoremas reutilizables.

Características principales

• REPL de Lean persistente: Tras un calentamiento único, las comprobaciones de compilación se reducen a ~0.4s (desde ~30s).
• Biblioteca de teoremas: Cada teorema demostrado se nombra automáticamente, se almacena y se puede importar para reutilizar.
• Biblioteca de axiomas: Almacena suposiciones conversacionales como declaraciones de Lean persistentes y verificadas por compilación.
• Integración con LSP de Lean: Busca lemas verificados de Mathlib en leansearch.net y Loogle, y utiliza diagnósticos LSP estructurados para reparaciones.
• Grafo de teoremas en Obsidian: Genera un grafo de dependencias visual de teoremas y lemas en Obsidian.
• Demostración en modo agente: Sesiones interactivas donde el agente itera sobre candidatos de prueba basándose en errores.
• Árbol de subobjetivos: Descompone teoremas complejos en subobjetivos independientes, los demuestra en paralelo y luego los une.
• Multiplanificador: Ejecuta múltiples planificadores en paralelo para diversas estrategias de prueba; el demostrador elige el mejor enfoque.

Inicio rápido

Requiere macOS (arm64) o Linux (x86_64), además del CLI codex para el backend predeterminado.

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

Pruébalo con:

mathcode -p "demostrar que el cuadrado de un número par es par"

Las salidas se escriben en LeanFormalizations/. Una interfaz de navegador está disponible mediante ./run webui.

Esta herramienta está dirigida a matemáticos, investigadores y desarrolladores que trabajan con verificación formal o demostración de teoremas asistida por IA.