Wiskundige artikelen hebben formele validatie nodig. Dit gebeurt meestal informeel door een referee. Maar wat als we konden vertrouwen op iets robuuster zoals auto-formalisatie in Lean 4, waarbij de rol van de referee zou worden verminderd tot het nauwkeurig controleren van de formuleringen van de definities en stellingen? De compilatie van automatisch gegenereerde code zou een bewijs certificaat worden. Dit is wat er gebeurde in een langere run die ik deed met Aristoteles door @HarmonicMath. Dank aan @PietroMonticone en @llllvvuu voor het helpen met de opzet voor het blauwdruk. Hier presenteer ik een complete correcte auto-formalisatie van een paper van mijn vriend Stefan Barańczuk over Chebyshev deelbaarheidsequenties. De code is ongeveer 5000 regels van zeer niet-triviale Lean. Het corrigeert alle inconsistenties en hiaten in het hoofdartikel (zelfs het bewijzen van enkele gedelegeerde proposities). Ik ga een serie van dergelijke experimenten posten, die bewijzen dat we in sommige gebieden van de wiskunde, waaronder elementaire getaltheorie, combinatoriek en analyse (alle soorten dingen behandeld door Mathlib), niet ver verwijderd zijn van een massale verschuiving in de documentatie van de geldigheid van bewijzen. Ik denk dat dit een hectisch jaar gaat worden!