Learning to Discover Interesting Mathematics

L'article définit l'intérêt intrinsèque d'un théorème comme le rapport entre la longueur de sa preuve et celle de son énoncé, en corrélation avec l'utilité en aval. Les auteurs entraînent un modèle de 27B pour prédire la difficulté des preuves. L'optimisation de cette métrique produit des théorèmes plus intéressants tout en réduisant le chevauchement avec Mathlib de 91,9% à 30,6%, illustrant la création de mathématiques hors distribution. Le système génère des candidats, sélectionne les plus intéressants et construit une bibliothèque mathématique auto-expansive.

Un modèle de 27B est entraîné pour prédire la difficulté des preuves plus précisément que les modèles généralistes de pointe.

L'optimisation de notre métrique réduit le chevauchement avec Mathlib de 91,9% à 30,6%.