El campo de la demostración automática de teoremas se enfrenta a un
obstáculo fundamental: a pesar del enorme potencial de los modelos de
lenguaje para el razonamiento matemático, su progreso se ve frenado por
la drástica escasez de datos de entrenamiento formales y de alta
calidad. A diferencia de los vastos corpus de texto general, las
bibliotecas matemáticas como Mathlib son relativamente pequeñas, lo que
limita la capacidad de estos sistemas para aprender y mejorar.
Para resolver este desafío, en el artículo LeanConjecturer: Automatic
generation of mathematical conjectures for theorem
proving se presenta una innovadora metodología para generar nuevas
conjeturas de manera automática. El sistema adopta un enfoque híbrido:
primero, extrae el contexto matemático (definiciones, variables) de un
archivo de Lean existente, y luego utiliza un modelo de lenguaje
exclusivamente para la tarea creativa de proponer nuevos enunciados de
teoremas. Estas propuestas se someten a un proceso de filtrado iterativo
para garantizar que sean sintácticamente correctas, novedosas y no
triviales, alimentando las conjeturas válidas de nuevo al sistema para
inspirar generaciones futuras cada vez más complejas.
El resultado es un éxito rotundo: el sistema no solo logra generar miles
de conjeturas válidas y desafiantes, sino que demuestra su utilidad
práctica al ser utilizadas para entrenar y mejorar el rendimiento de un
demostrador de teoremas de vanguardia. Más allá de simplemente crear
datos, LeanConjecturer fue capaz de formular y verificar teoremas
genuinamente interesantes en el campo de la topología, estableciendo
nuevas conexiones entre conceptos matemáticos. Con ello, el proyecto no
solo ofrece una solución escalable al problema de la escasez de datos,
sino que también abre una prometedora vía hacia la colaboración entre
humanos y máquinas en el descubrimiento de nuevas matemáticas.