MathCode convierte problemas en lenguaje natural en teoremas de Lean 4 e intenta demostraciones formales

Why it matters

MathCode shows how AI math tools are shifting from one-off answers toward persistent, reusable proof libraries, with Lean's compiler providing a hard verification layer.

Los materiales públicos asocian más claramente a Yifan Zhang (@yifanzhang_) con Math-AI, la comunidad de investigación abierta detrás de MathCode, un asistente de codificación de IA para terminal que convierte las matemáticas escritas en lenguaje ordinario en enunciados de Lean 4, intenta pruebas formales y guarda los resultados exitosos para uso posterior.

La página del proyecto de MathCode fecha el proyecto en abril de 2026. MathCode debe entenderse como un proyecto de investigación de código abierto en curso más que como un lanzamiento nuevo.

La distinción importa porque la idea más fuerte de MathCode es más amplia que su versión inicial: el grupo de Zhang trata las matemáticas formales como una base de código que un agente puede ampliar, buscar y reutilizar gradualmente. Cada teorema exitoso puede convertirse en infraestructura para la siguiente prueba.

Zhang se describe a sí mismo como estudiante de doctorado en Princeton University y Princeton AI Lab Fellow que trabaja en razonamiento de modelos de lenguaje, aprendizaje por refuerzo, preentrenamiento y arquitectura de modelos. Su portafolio de investigación pública incluye curación de texto matemático y sistemas de razonamiento, trabajo que ayuda a explicar el énfasis de MathCode en convertir lenguaje matemático no estructurado en objetos duraderos legibles por máquina.

Math-AI se presenta como una comunidad de investigación abierta, con código, modelos y materiales de investigación publicados a través de GitHub y Hugging Face. Sus materiales públicos no presentan a MathCode como un servicio comercial, y el proyecto no divulga precios, ingresos ni cifras de clientes.

A proof assistant built like a coding agent

El repositorio de MathCode de código abierto empaqueta el flujo de trabajo como una aplicación de terminal para macOS en procesadores Arm y Linux en sistemas x86_64. Un usuario puede enviar un prompt como "demuestra que el cuadrado de un número par es par." MathCode formaliza la solicitud como un teorema de Lean, genera candidatos de prueba, los compila y usa los errores de Lean para guiar otro intento.

La configuración local es una elección deliberada de producto. MathCode instala una cadena de herramientas de Lean agrupada, mantiene un servidor de lenguaje persistente y escribe el trabajo generado en un directorio LeanFormalizations. También se incluye una interfaz de navegador, pero el terminal sigue siendo el flujo de trabajo principal.

La ruta predeterminada depende de OpenAI's Codex CLI y su sistema de autenticación. El repositorio también documenta backends compatibles con Anthropic y OpenAI. Esa flexibilidad da a los investigadores cierto control sobre el modelo subyacente, aunque la calidad de las pruebas de MathCode, la latencia y el costo operativo siguen dependiendo en parte del proveedor de modelo externo que elijan.

La documentación de MathCode dice que su proceso persistente de Lean reduce las comprobaciones de compilación a aproximadamente 0.4 segundos tras el calentamiento, en comparación con unos 30 segundos cuando Lean debe iniciarse y cargar sus bibliotecas repetidamente. Esas cifras provienen del proyecto y no son un benchmark independiente. El diseño sigue abordando un problema concreto de agente: los ciclos largos de retroalimentación hacen que la reparación iterativa de pruebas sea costosa, mientras que un compilador persistente permite al modelo fallar y reintentar rápidamente.

El agente puede dividir un teorema en subobjetivos, ejecutar varias estrategias de planificación en paralelo y unir piezas exitosas en una prueba final. También busca en LeanSearch y Loogle lemas existentes de Mathlib, alimentando diagnósticos de compilador estructurados de vuelta al bucle de prueba.

MathCode se construye sobre el proyecto AUTOLEAN, que suministra la formalización subyacente y la canalización de demostración. La contribución de Math-AI es el entorno de trabajo circundante: estado persistente, búsqueda en la biblioteca, reparación iterativa, planificación en paralelo e interfaces para retener lo que el agente ya ha demostrado.

Zhang is betting on memory, not disposable answers

La característica más trascendente es el manejo del trabajo previo por parte de MathCode. Los teoremas que se compilan con éxito pueden nombrarse automáticamente, escribirse en una biblioteca reutilizable de Lean e importarse en sesiones posteriores. Los usuarios también pueden almacenar supuestos conversacionales como declaraciones de axiomas comprobadas por compilación.

Eso crea riesgos además de utilidad. Lean puede verificar que una prueba se sigue de sus premisas declaradas, pero no puede garantizar que las premisas de un usuario describan con precisión el mundo. MathCode incluye herramientas de revisión de consistencia para axiomas almacenados, según su documentación, pero la fiabilidad de la base de conocimiento resultante sigue dependiendo de una especificación cuidadosa y la gestión de la biblioteca.

MathCode también genera una bóveda de Obsidian que mapea las dependencias entre teoremas y lemas. El grafo es una expresión práctica de la dirección de investigación más amplia de Zhang: la producción matemática debería acumularse en una estructura navegable en lugar de desaparecer cuando termina una sesión de chat.

Este enfoque da a MathCode una forma de producto diferente a la de un sistema alojado de preguntas y respuestas. Su valor crece cuando el mismo investigador lo sigue usando, curando teoremas y construyendo un cuerpo local de conocimiento formal. Eso podría adecuarse a ingenieros de pruebas y matemáticos técnicamente capaces que quieran archivos inspectables y control sobre la cadena de herramientas. Los requisitos de instalación y el flujo de trabajo centrado en Lean estrechan la audiencia inicial.

Formal mathematics is becoming an agent category

MathCode entró en un campo donde varios grupos intentan emparejar modelos de lenguaje con asistentes de pruebas. Harmonic's Aristotle acepta problemas en inglés, produce formalizaciones en Lean y puede trabajar directamente dentro de repositorios Lean existentes. Harmonic dice que su agente alojado puede operar de forma autónoma durante hasta 24 horas.

Math Inc.'s Gauss apunta a formalizaciones de investigación a gran escala con cómputo extenso y guía matemática humana. Math Inc. también ha lanzado OpenGauss, un arnés de código abierto con un marco de evaluación público. Axiom Math's AXLE y proyectos de investigación como LeanDojo abordan otras partes de la pila de generación y verificación de pruebas.

MathCode no ha publicado un benchmark independiente de éxito de pruebas que establezca que supera a esos sistemas. Su documentación pública tampoco ofrece cifras sobre usuarios activos, gasto en inferencia o la proporción de problemas en lenguaje natural que alcanzan una prueba válida.

Su contribución defendible es la experiencia de desarrollador que Zhang y Math-AI han elegido construir alrededor de la prueba formal. MathCode pone el bucle del compilador, la memoria de teoremas, la gestión de axiomas, la planificación en paralelo y el grafo de dependencias en un solo entorno local. Esa combinación lo hace útil como sistema de investigación inspectable incluso antes de que pueda reclamar una fiabilidad matemática amplia.

Para Zhang, MathCode conecta varias vertientes de su trabajo: selección de datos de entrenamiento matemáticos, mejora de sistemas de razonamiento y uso de la verificación formal como una comprobación estricta sobre la salida del modelo. El repositorio da a esa investigación una superficie de producto que la gente puede ejecutar, modificar y auditar. Su siguiente prueba es empírica: si la memoria acumulada realmente ayuda a los usuarios a completar formalizaciones difíciles, y si esas ganancias pueden medirse frente a alternativas cada vez más capaces.