Lucrările matematice necesită validare formală. Acest lucru se face de obicei informal de către un arbitru. Dar dacă ne-am putea baza pe ceva mai robust, cum ar fi auto-formalizarea în Lean 4, unde rolul arbitrului s-ar reduce la verificarea meticuloasă a formulărilor definițiilor și teoremelor? Compilarea codului generat automat ar deveni un certificat de dovadă. Asta s-a întâmplat într-o perioadă mai lungă, așa cum am făcut cu Aristotel de @HarmonicMath. Mulțumiri lui @PietroMonticone și @llllvvuu pentru ajutorul la configurarea planului. Aici prezint o auto-formalizare corectă completă a unei lucrări a prietenului meu Stefan Barańczuk despre secvențele de divizibilitate ale lui Chebyshev. Codul conține aproximativ 5000 de linii de Lean, foarte netrivial. Corectează toate inconsecvențele și lacunele din lucrarea principală (ba chiar dovedește unele propoziții delegate). Voi posta o serie de astfel de experimente, demonstrând că în unele domenii ale matematicii, inclusiv teoria elementară a numerelor, combinatorica și analiza (tot felul de aspecte acoperite de Mathlib), nu suntem departe de o schimbare masivă în documentarea validității demonstrațiilor. Cred că va fi un an agitat!