Tässä esittelen täydellisen automaattisen formalisoinnin tuoreesta matematiikan esseestä (taas!) Barańczuk, Stefan. "Yhtälöiden määrän vähentäminen, jotka määrittelevät n-avaruuden osajoukon äärellisellä kentällä." Annales de la Faculté des Sciences de Toulouse: Mathématiques, sarja 6, vol. 33, nro 1 (2024): 177–182. Käytin tämän projektin parissa muutaman päivän. Ensin ajoin Aristoteleen @HarmonicMath , joka noin 15 tunnissa autoformalisoitui todistuksen täysin. Sitten, @PietroMonticone:n suurella avustuksella, onnistuin laatimaan todisteesta pohjapiirustusversion. Tässä versiossa kaikki LaTeXin dokumentaation osat muuttuvat interaktiisiksi ja niitä voidaan tarkastella ja tutkia. Voimme nähdä riippuvuudet todistuksessa ja tutkia niiden suhteita. Jälkikäsittelyvaiheessa käytin myös Grok Heavyä ja Codex CLI:tä GPT-5.2:n kanssa xhigh-tilassa kirjoittaakseni rivikohtaisen analyysin muodollisesta todistuksesta. Tämä on erinomainen apu niille, jotka eivät ole ammattimaisia Lean 4 -ohjelmoijia. Voit todella sisäistää kaikki todistuksen vaiheet. Haluan tiivistää vaikutelmani ja mitä opin tästä kokemuksesta. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei