MathCode es un asistente de programación para terminal que incorpora un motor de formalización matemática. Acepta un enunciado matemático en lenguaje natural y lo traduce automáticamente a un teorema en Lean 4 para intentar demostrarlo de forma formal. La herramienta combina un REPL persistente de Lean, bibliotecas reutilizables de teoremas y axiomas, un demostrador agéntico y un grafo de conocimiento en Obsidian.
Funciona sobre macOS en arquitecturas arm64 y Linux x86_64, y utiliza el CLI codex como backend por defecto. La instalación se realiza clonando el repositorio y ejecutando un script que prepara el entorno, descarga el runtime incluido y la cadena de herramientas de Lean, e instala un lanzador local. Un comando de ejemplo genera el teorema que demuestra que el cuadrado de un número par es par, y los resultados se guardan en el directorio LeanFormalizations/.
Entre sus capacidades destaca un servidor de lenguaje persistente que reduce el tiempo de compilación a unos 0,4 segundos tras un calentamiento inicial, frente a los aproximadamente 30 segundos habituales. Cada teorema demostrado se nombra, almacena y queda disponible para que el demostrador y el planificador lo reutilicen. El sistema busca lemas verificados en Mathlib mediante leansearch.net y Loogle, y emplea diagnósticos estructurados del LSP para reparar errores. Además, genera una bóveda de Obsidian que visualiza las dependencias entre teoremas y lemas, descompone teoremas complejos en submetas independientes que resuelve en paralelo, y ejecuta varios planificadores de forma concurrente para explorar estrategias de demostración distintas. La canalización de formalización y demostración se basa en el proyecto AUTOLEAN. Para usos de investigación, el repositorio incluye una cita en BibTeX.