Autoformalizzazione a lungo orizzonte di un teorema fondamentale alla base di MIP* = RE

Abstract degli autori

Le formalizzazioni matematiche di riferimento hanno richiesto anni di lavoro a team specializzati. Presentiamo FormalFlow, un sistema che coordina agenti di dimostrazione basati sull’IA sotto la supervisione umana per affrontare lo slittamento degli enunciati e la composizione delle dimostrazioni nella formalizzazione a lungo orizzonte. Attingendo a principi e pratiche dell’ingegneria del software, usa uno schema condiviso per guidare cicli annidati di pianificazione, dimostrazione e revisione. Con FormalFlow abbiamo completato in 63 giorni una dimostrazione in Lean 4, verificata automaticamente, della solidità quantistica del test classico del basso grado individuale, un teorema fondamentale alla base di MIP* = RE. La libreria finale contiene 126.367 righe di codice Lean, tutte generate da agenti. Oltre a fornire una base verificata per la complessità quantistica, la formalizzazione corregge condizioni laterali e limiti intermedi dell’errore nella dimostrazione pubblicata e migliora l’esponente dell’errore del teorema principale. Il resoconto dello sviluppo mostra cosa occorre per fidarsi delle dimostrazioni scritte da agenti di IA e fornisce strumenti riutilizzabili per verificare la matematica di ricerca su larga scala.