Här presenterar jag en fullständig autoformalisering av en nyligen publicerad matematikuppsats (igen!) Barańczuk, Stefan. "Reducerar antalet ekvationer som definierar en delmängd av n-rummet över ett ändligt fält." Annales de la Faculté des sciences de Toulouse: Mathématiques, serie 6, vol. 33, nr 1 (2024): 177–182. Jag har lagt några dagar på det här projektet. Först körde jag Aristoteles av @HarmonicMath , som på ungefär 15 timmar helt autoformaliserade beviset. Sedan, med stor hjälp av @PietroMonticone, lyckades jag sätta upp en ritningsversion av beviset. Detta är en version där alla delar av dokumentationen i LaTeX blir interaktiva och kan granskas och studeras. Vi kan se beroendena i beviset och studera deras relationer. I efterbearbetningsfasen använde jag också Grok Heavy och Codex CLI med GPT-5.2 i xhigh-läge för att skriva en rad-för-rad-analys av det formella beviset. Detta är till stor hjälp för personer som inte är professionella Lean 4-programmerare. Du kan verkligen internalisera alla bevisens steg. Jag vill sammanfatta mina intryck och vad jag lärde mig av denna erfarenhet. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei