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.