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

Matematické práce potřebují formální ověření. Obvykle to dělá neformálně rozhodčí. Ale co kdybychom se mohli spolehnout na něco robustnějšího, například automatickou formalizaci do Lean 4, kde by role recenzenta byla redukována na pečlivé ověřování formulací definic a vět? Kompilace automaticky generovaného kódu se stala důkazním certifikátem. To se stalo v delším období, které jsem udělal s Aristotelem do @HarmonicMath. Díky @PietroMonticone a @llllvvuu za pomoc s nastavením plánu. Zde předkládám úplně správnou autoformalizaci článku mého přítele Stefana Barańczuka o Čebyševových sekvencích dělitelnosti. Kód má asi 5000 řádků vysoce netriviálního Lean. Opravuje všechny nesrovnalosti a mezery v hlavním článku (dokonce dokazuje některé delegované tvrzení). Chystám se zveřejnit sérii takových experimentů, které dokazují, že v některých oblastech matematiky, včetně elementární teorie čísel, kombinatoriky a analýzy (všelijaké věci pokrývá Mathlib), nejsme daleko od masivního posunu v dokumentaci platnosti důkazů. Myslím, že to bude hektický rok!

Kdybych byl dnes studentem, interakce s nejmodernějšími LLM by mi připadala téměř jako podvádění. Dnes ráno jsem náhodně vyfotil tabuli a požádal ChatGPT-5.2-Pro, aby vysvětlil kontext, řešení a pár poznámek k slavné Chevalleyově větě o konstruktibilních množinách. Dostal jsem pozoruhodně hlubokou zprávu, která syntetizovala kvalitní materiály o algebraické geometrii z internetu. To vyvolává vážnou otázku: jaké je skutečné úsilí a výzva pro dnešní studenty? Cena je jistě jedním z faktorů, ale jakmile je k těmto modelům přístup, jak by se měl člověk učit v této zemi hojnosti, kde jsou vysvětlení, odkazy a interaktivní průzkum okamžitě dostupné? Možná už boj není o získávání informací nebo pochopení individuálních argumentů, ale o rozvoji úsudku: vědět, které otázky klást, kterým vysvětlením důvěřovat, jak rozpoznat hloubku versus povrchovou věrohodnost a jak si myšlenky internalizovat místo toho, abychom je jen konzumovali. V prostředí, kde je odpovědí dostatek, může skutečná obtíž spočívat v formování vkusu, matematické intuice a schopnosti se v tomto náhlém přebytku znalostí orientovat – místo aby se utopil – v něm.