Hier presenteer ik een complete auto-formalisering van een recent wiskundig artikel (weer!) Barańczuk, Stefan. "Het verminderen van het aantal vergelijkingen dat een subset van de n-ruimte over een eindig veld definieert." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024): 177–182. Ik heb een paar dagen aan dit project gewerkt. Eerst heb ik Aristotle uitgevoerd door @HarmonicMath, dat in ongeveer 15 uur de bewijsvoering volledig auto-geformaliseerd heeft. Daarna, met de geweldige hulp van @PietroMonticone, is het me gelukt om een blauwdrukversie van het bewijs op te zetten. Dit is een versie waarin alle delen van de documentatie in LaTeX interactief worden en kunnen worden geïnspecteerd en bestudeerd. We kunnen de afhankelijkheden in het bewijs zien en hun relaties bestuderen. In de post-processing fase heb ik ook Grok Heavy en Codex CLI met GPT-5.2 in xhigh-modus gebruikt om een regel-voor-regel analyse van het formele bewijs te schrijven. Dit is een grote hulp voor mensen die geen professionele Lean 4 programmeurs zijn. Je kunt echt alle stappen van het bewijs internaliseren. Ik wil mijn indrukken samenvatten en wat ik van deze ervaring heb geleerd. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei