Oto przedstawiam kompletną autoformalizację niedawnego artykułu matematycznego (znowu!) Barańczuk, Stefan. "Redukcja liczby równań definiujących podzbiór n-przestrzeni nad ciałem skończonym." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, nr 1 (2024): 177–182. Spędziłem kilka dni nad tym projektem. Najpierw uruchomiłem Arystotelesa przez @HarmonicMath, który w około 15 godzin całkowicie autoformalizował dowód. Następnie, z wielką pomocą @PietroMonticone, udało mi się stworzyć wersję roboczą dowodu. To jest wersja, w której wszystkie części dokumentacji w LaTeX stają się interaktywne i mogą być badane oraz studiowane. Możemy zobaczyć zależności w dowodzie i badać ich relacje. W etapie przetwarzania końcowego użyłem również Grok Heavy i Codex CLI z GPT-5.2 w trybie xhigh, aby napisać analizę dowodu formalnego linia po linii. To jest wielka pomoc dla osób, które nie są profesjonalnymi programistami Lean 4. Można naprawdę przyswoić wszystkie kroki dowodu. Chcę podsumować moje wrażenia i to, czego nauczyłem się z tego doświadczenia. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei