MathCode: el asistente de IA que convierte problemas matemáticos en pruebas formales con Lean 4
MathCode, Mathematical Coding Agent
MathCode es un asistente de codificación para terminal que integra un motor de formalización matemática. Convierte problemas en lenguaje natural en teoremas de Lean 4 e intenta demostrarlos formalmente, gracias a un REPL persistente, bibliotecas de teoremas y axiomas reutilizables, y un modo agente. Incluye un grafo de conocimiento en Obsidian y descompone teoremas complejos en subobjetivos que se prueban en paralelo. Requiere macOS (arm64) o Linux (x86_64) y la CLI de codex.
Un servidor de lenguaje Lean persistente reduce los chequeos de compilación a ~0.4s después de un calentamiento inicial, en lugar de ~30s.