Un equipo de investigación ha desarrollado un modelo de lenguaje de gran escala (LLM) de 27.000 millones de parámetros diseñado para predecir la dificultad de las pruebas matemáticas. El objetivo principal no es solo generar teoremas, sino identificar aquellos que son intrínsecamente interesantes y útiles para la comunidad científica. Los autores definen la 'interés intrínseco' de un teorema como la relación entre la longitud de su demostración y la de su enunciado. Sus resultados indican que esta métrica se correlaciona fuertemente con la utilidad práctica del teorema en aplicaciones posteriores.
El modelo ha sido entrenado para superar a los modelos de frontera generales en la predicción de la dificultad de las pruebas. Al optimizar el sistema para maximizar esta métrica, se logró una reducción significativa de la superposición con Mathlib, una biblioteca formal de matemáticas, pasando del 91,9% al 30,6%. Esto demuestra la capacidad del sistema para generar matemáticas fuera de la distribución, es decir, contenido nuevo y no redundante.
El framework permite generar candidatos a teoremas, seleccionar los más interesantes y construir iterativamente una biblioteca matemática autoexpandida. Este enfoque ofrece una vía práctica para crear bibliotecas matemáticas verificadas por máquina que pueden elegir declaraciones valiosas sin depender de objetivos proporcionados por humanos, facilitando la expansión del conocimiento matemático a escala sin precedentes.