Investigadores de Meta y de la Universidad de Nueva York han construido un sistema de inteligencia artificial simplificado para demostrar teoremas matemáticos que igualó o superó a flujos de trabajo de demostración en Lean cuidadosamente diseñados, y lo hizo a un costo menor.

El sistema, llamado h1, plantea un argumento simple: en la demostración automática de teoremas, la simplicidad puede vencer a la complejidad, siempre que el modelo reciba buena retroalimentación.

Un bucle agéntico minimalista

El trabajo proviene del equipo de investigación FAIR de Meta y de la NYU. En un artículo titulado "h1: A Taste of the Bitter Lesson in Automated Theorem Proving", publicado el 25 de octubre de 2026, los investigadores describen h1 como un bucle agéntico minimalista que conecta grandes modelos de lenguaje de frontera con Lean 4 y les proporciona los resultados del verificador en tiempo real.

Lean 4 es un asistente de pruebas de código abierto en el que los argumentos matemáticos se escriben como código, por lo que un compilador, en lugar de un revisor humano, verifica cada paso. Esa configuración le da al verificador la última palabra: una prueba solo cuenta una vez que compila.

La mayoría de los demostradores automáticos envuelven el modelo de lenguaje en un andamiaje elaborado, usando flujos de trabajo predefinidos que dividen los problemas en partes, enrutan subtareas y orquestan muchos componentes. El marco h1 prescinde de esa maquinaria y en su lugar se apoya en algunos mecanismos simples:

• Edición persistente de archivos, de modo que el modelo trabaja sobre un archivo de demostración que conserva su estado entre pasos
• Retroalimentación inmediata del compilador tras cada edición, de modo que los errores se detectan de inmediato
• Reflexión, utilizando la capacidad del propio modelo de lenguaje de razonar sobre qué salió mal

Según el artículo, el desempeño de h1 proviene principalmente de una interfaz eficiente con Lean, y no de una orquestación sofisticada.

Resultados de los benchmarks

La investigación reporta que h1 alcanzó un desempeño de vanguardia en varios benchmarks de demostración formal de teoremas. En PutnamBench, un benchmark construido a partir de problemas de la Competencia William Lowell Putnam, el concurso anual de matemáticas para estudiantes de pregrado de Norteamérica, obtuvo 670 de 672 usando GPT-5.5. En la evaluación FATE-X, h1 obtuvo 90 de 100.

El sistema también resolvió ocho problemas abiertos de la colección FormalConjectures. Estos incluyen variantes de los problemas de Erdős, un conjunto de preguntas nombradas en honor al prolífico matemático Paul Erdős. Como estos problemas se plantean en el lenguaje formal de Lean, resolverlos significa producir demostraciones verificadas por máquina en lugar de argumentos en prosa.

La comparación más directa es con AlphaProof Nexus de DeepMind. En la resolución de problemas de Erdős, h1 registró una tasa de éxito de 82.5%, mientras que AlphaProof Nexus alcanzó 76%. La brecha de costo fue mayor que la brecha de precisión: h1 gastó $121 por cada prueba exitosa, frente a $317 de AlphaProof Nexus.

La lección amarga, aplicada a las matemáticas

El título del artículo alude a la "lección amarga", el término que el investigador de IA Rich Sutton acuñó en un ensayo de 2019 para la idea de que los métodos escalables y de propósito general, impulsados por una gran capacidad de cómputo, tienden a superar con el tiempo a las técnicas especializadas hechas a mano.

Este no es el primer intento de Meta en el problema. La investigación se basa en trabajos previos de Meta, incluido el demostrador de teoremas neuronal HTPS presentado en 2022, y refleja un cambio de enfoque. Los sistemas anteriores se centraban en construir búsquedas más inteligentes alrededor del modelo, mientras que h1 se centra en permitir que el modelo interactúe directamente con el verificador.

El momento también importa. Los resultados de h1 dependen de modelos de frontera como GPT-5.5, y la fuerte puntuación en PutnamBench se logró con ese modelo.

Qué significa esto

Las cifras de costo son la parte más práctica del trabajo. Una reducción de $317 a $121 por prueba exitosa cambia qué problemas valen la pena intentar. Cuando cada intento cuesta menos, los equipos pueden realizar más intentos sobre conjeturas más difíciles o más especulativas. La naturaleza verificada por máquina de los resultados también es parte del atractivo: el progreso en la demostración formal atrae atención mucho más allá de las matemáticas, ya que los asistentes de pruebas también se usan para verificar diseños de software y hardware.

Aplican algunas advertencias. Las puntuaciones de los benchmarks muestran el desempeño en conjuntos de prueba específicos, y PutnamBench está cerca de saturarse con 670 de 672, por lo que el desempeño en colecciones de problemas abiertos como FormalConjectures será la medida más relevante a observar. El enfoque de h1 también depende en gran medida del modelo de frontera que lo sustenta.

El mensaje más amplio del artículo es que un modelo base potente combinado con una retroalimentación limpia del verificador puede importar más que un andamiaje elaborado, una apuesta que, en estos benchmarks, dio resultado.

Fuente: CryptoBriefing