h1 permite que un modelo de lenguaje construya demostraciones en Lean 4. En distintos bancos de pruebas, sus autores comunican resultados destacados, cada uno ligado a un modelo y una tarea concretos; no es una medida única de capacidad matemática. El sistema, descrito por investigadores con afiliaciones a Meta FAIR y otras instituciones, combina un archivo de trabajo persistente con herramientas y comprobaciones formales. El artículo de investigación detalla el método y sus resultados.
Cómo trabaja h1 con Lean 4
h1 es un arnés: una estructura que conecta un modelo de lenguaje con Lean 4, un entorno para escribir y comprobar demostraciones matemáticas formales. El modelo modifica un mismo archivo de prueba en varios turnos. Tras cada cambio, Lean compila el código y devuelve errores y objetivos que siguen pendientes; el modelo puede usar esa respuesta para decidir qué probar después.
También puede buscar definiciones y lemas en Mathlib, la biblioteca matemática de Lean, probar fragmentos en el entorno interactivo de Lean y consultar información del lenguaje. h1 no impone una división fija del problema ni un árbol de búsqueda. Si una entrega es rechazada, un modelo de reflexión resume el avance y los comentarios del verificador para orientar otro intento.
La compilación no es el último control. SafeVerify contrasta la entrega con el enunciado original, comprueba las declaraciones objetivo y los axiomas permitidos, y después reproduce las declaraciones en el núcleo de Lean. Así se comprueba la demostración formal dentro de ese entorno.
Qué resultados comunican los autores
Las cifras corresponden a pruebas distintas y a modelos distintos. En PutnamBench, un conjunto de 672 problemas de competiciones universitarias Putnam anteriores, h1 con GPT-5.5 resolvió 670. El artículo informa de una ejecución por problema, sin repeticiones ni intentos en paralelo.
Con GPT-5.6 Sol, los autores comunican estos resultados en otros conjuntos:
- 90 de 100 problemas de FATE-X, una colección de álgebra de nivel de examen de acceso al doctorado o superior.
- 78 de 100 problemas de FC100-solved.
- 14 de 23 teoremas de FormalQualBench.
- 6 de 6 problemas de IMO 2026.
El artículo también informa de ocho objetivos de Formal Conjectures resueltos entre 236 que el estudio consideraba abiertos: variantes de Erdős 138 y 337, OEIS A108081, A211417 y A022030, Open Quantum Problem 35 y dos conjeturas de Written on the Wall II. Los autores señalan que las dos últimas, las conjeturas 100 y 314, se demostraron después de corregir sus enunciados formalizados.
Qué compara la cifra de coste frente a AlphaProof Nexus
La comparación destacada se limita a cinco problemas abiertos de Erdős en los que los tres sistemas evaluados lograron al menos un éxito. Con Gemini 3.1 Pro, h1 alcanzó un 82,5 % en pass@1, es decir, con un intento, frente al 76 % de AlphaProof Nexus completo.
| Sistema | Pass@1 en cinco problemas de Erdős | Coste medio por prueba exitosa, condicionado al éxito | Alcance del coste |
| h1 | 82,5 % | 121 USD | Media calculada solo con los grupos que tuvieron éxito. |
| AlphaProof Nexus completo | 76 % | 317 USD | Media condicionada al éxito; no incluye la inferencia de AlphaProof. |
Los importes son estimaciones experimentales equivalentes a costes de API, calculadas a partir del uso de tokens y tarifas de referencia. No son precios de un producto ni gastos necesariamente facturados. En el mismo subconjunto de cinco problemas, el gasto medio de h1 al pass@1 sube a 138 USD al incluir los grupos fallidos. Para alcanzar al menos el 82,5 % con pass@3, el estudio informa de un gasto medio de 202 USD, también con los fallos incluidos.
La comparación de cinco problemas deja fuera Erdős 125: las 16 réplicas de h1 terminaron en tiempos de espera del entorno interactivo de Lean. Al considerar los seis problemas, los autores comunican tasas pass@1 diferentes: 68,75 % para h1 y 71,67 % para AlphaProof Nexus completo. Son resultados de otro conjunto, no la misma frontera de éxito y coste de la tabla.
Qué valida una demostración formal
Una prueba aceptada por Lean acredita que el código demuestra el enunciado formal bajo las reglas y axiomas permitidos en ese entorno. Por sí sola, esa comprobación no determina si el enunciado formal recoge fielmente una conjetura expresada en lenguaje matemático informal. Las correcciones que precedieron a dos de los resultados de Written on the Wall II ilustran por qué ambas cuestiones deben evaluarse por separado.
