Zde představuji kompletní automatickou formalizaci nedávné matematické práce (znovu!) Barańczuk, Stefan. "Snížení počtu rovnic definujících podmnožinu n-prostoru nad konečným tělesem." Annales de la Faculté des sciences de Toulouse: Mathématiques, série 6, sv. 33, č. 1 (2024): 177–182. Strávil jsem na tomto projektu několik dní. Nejprve jsem spustil Aristotela podle @HarmonicMath , což za asi 15 hodin důkaz zcela automaticky formalizovalo. Pak jsem s velkou pomocí @PietroMonticone dokázal vytvořit blueprintovou verzi korektury. Jedná se o verzi, ve které se všechny části dokumentace v LaTeXu stávají interaktivními a lze je kontrolovat a studovat. Můžeme vidět závislosti v důkazu a studovat jejich vztahy. Ve fázi postprocessingu jsem také použil Grok Heavy a Codex CLI s GPT-5.2 v režimu xhigh k napsání analýzy řádek po řádku formálního důkazu. To je velká pomoc pro lidi, kteří nejsou profesionální programátoři Lean 4. Všechny kroky důkazu si opravdu můžete osvojit. Chci shrnout své dojmy a co jsem se z této zkušenosti naučil. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei