Her presenterer jeg en fullstendig autoformalisering av en nylig matematikkartikkel (igjen!) Barańczuk, Stefan. "Reduksjon av antall ligninger som definerer en delmengde av n-rommet over et endelig felt." Annales de la Faculté des sciences de Toulouse: Mathématiques, ser. 6, vol. 33, nr. 1 (2024): 177–182. Jeg brukte noen dager på dette prosjektet. Først kjørte jeg Aristoteles av @HarmonicMath, som på omtrent 15 timer fullstendig autoformaliserte beviset. Deretter, med stor hjelp fra @PietroMonticone, klarte jeg å sette opp en blåkopiversjon av beviset. Dette er en versjon der alle deler av dokumentasjonen i LaTeX blir interaktive og kan inspiseres og studeres. Vi kan se avhengighetene i beviset og studere deres relasjoner. I etterbehandlingsfasen brukte jeg også Grok Heavy og Codex CLI med GPT-5.2 i xhigh-modus for å skrive en linje-for-linje-analyse av det formelle beviset. Dette er til stor hjelp for folk som ikke er profesjonelle Lean 4-programmerere. Du kan virkelig internalisere alle trinnene i beviset. Jeg vil oppsummere mine inntrykk og hva jeg lærte av denne opplevelsen. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei