I documenti matematici necessitano di una validazione formale. Questo di solito viene fatto informalmente da un revisore. Ma cosa succederebbe se potessimo fare affidamento su qualcosa di più robusto come l'auto-formalizzazione in Lean 4, dove il ruolo del revisore sarebbe ridotto a un controllo meticoloso delle formulazioni delle definizioni e dei teoremi? La compilazione del codice generato automaticamente diventerebbe un certificato di prova. Questo è ciò che è accaduto in un progetto più lungo che ho fatto con Aristotele da @HarmonicMath. Grazie a @PietroMonticone e @llllvvuu per aver aiutato con la configurazione del progetto. Qui presento un'auto-formalizzazione completa e corretta di un articolo del mio amico Stefan Barańczuk riguardo alle sequenze di divisibilità di Chebyshev. Il codice è di circa 5000 righe di Lean altamente non banale. Corregge tutte le incoerenze e le lacune nel documento principale (inclusa la dimostrazione di alcune proposizioni delegate). Pubblicherò una serie di esperimenti di questo tipo, dimostrando che in alcune aree della matematica, inclusa la teoria dei numeri elementare, la combinatoria e l'analisi (tutte le cose coperte da Mathlib), non siamo lontani da un cambiamento massiccio nella documentazione della validità delle prove. Penso che quest'anno sarà frenetico!