Aici prezint o auto-formalizare completă a unei lucrări recente de matematică (din nou!) Barańczuk, Stefan. "Reducerea numărului de ecuații care definesc un subset al spațiului n-dimensional peste un corp finit." Annales de la Faculté des sciences de Toulouse: Mathématiques, ser. 6, vol. 33, nr. 1 (2024): 177–182. Am petrecut câteva zile la acest proiect. Mai întâi, am rulat Aristotele după @HarmonicMath , care în aproximativ 15 ore a auto-formalizat complet demonstrația. Apoi, cu ajutorul lui @PietroMonticone, am reușit să configurez o versiune blueprint a demonstrației. Aceasta este o versiune în care toate părțile documentației din LaTeX devin interactive și pot fi inspectate și studiate. Putem vedea dependențele din demonstrație și să studiem relațiile lor. În etapa de post-procesare, am folosit și Grok Heavy și Codex CLI cu GPT-5.2 în modul xhigh pentru a scrie o analiză linie cu linie a demonstrației formale. Acesta este un mare ajutor pentru cei care nu sunt programatori Lean 4 profesioniști. Poți cu adevărat să internalizezi toți pașii demonstrației. Vreau să rezum impresiile mele și ce am învățat din această experiență. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei