Ricerca
Un dataset di enunciati di teoremi formalizzati tratti dagli Annals of Mathematics
I recenti progressi nell’autoformalizzazione della matematica mediante l’IA sono stati notevoli. Per misurarli servono dataset di enunciati formali che siano difficili e affidabili. Presentiamo Annals
- arXiv
- 2610.18301
- Pubblicato
- 2026-10-13
- Autori
- Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su, Jack McKoen, Kevin Buzzard
Abstract degli autori
I recenti progressi nell’autoformalizzazione della matematica mediante l’IA sono stati notevoli. Per misurarli servono dataset di enunciati formali che siano difficili e affidabili. Presentiamo AnnalsChallenge: 50 enunciati di teoremi formalizzati a mano in Lean 4 usando Mathlib. Ciascuno è il risultato principale di un articolo pubblicato negli Annals of Mathematics dal 2020. Ogni formalizzazione è stata esaminata manualmente e poi sottoposta a verifica mediante l’IA. Li rendiamo disponibili senza dimostrazioni formalizzate.
Il riassunto di questo paper è disponibile solo in inglese: leggilo nella pagina inglese.
Leggi il paper originale su arXiv