Matemaattiset artikkelit vaativat muodollista validointia. Tämä tehdään yleensä epävirallisesti erotuomarin toimesta. Mutta entä jos voisimme luottaa johonkin vahvempaan, kuten autoformalisointiin Lean 4:ään, jossa tuomarin rooli rajoittuisi määritelmien ja lauseiden muotoilujen tarkkaavaiseen tarkistamiseen? Automaattisesti luodun koodin kokoaminen muuttuisi todistustodistukseksi. Näin kävi pidemmällä jaksolla, jonka tein Aristoteleen kanssa @HarmonicMath. Kiitos @PietroMonticone:lle ja @llllvvuu:lle avusta pohjapiirustuksen valmisteluissa. Tässä esittelen täydellisen oikean autoformalisoinnin ystäväni Stefan Barańczukin artikkelista, joka käsittelee Chebyshevin jaettavuusjonoja. Koodi on noin 5000 riviä erittäin ei-triviaalia Lean-linjaa. Se korjaa kaikki epäjohdonmukaisuudet ja aukot pääartikkelissa (jopa todistaa joitakin delegoituja väitteitä). Aion julkaista sarjan tällaisia kokeita, jotka todistavat, että joillakin matematiikan aloilla, kuten alkeislukuteoriassa, kombinatoriikassa ja analyysissä (kaikenlaisia Mathlibin kattamia asioita), emme ole kaukana valtavasta muutoksesta todistusten pätevyyden dokumentoinnissa. Luulen, että tästä tulee kiireinen vuosi!