Osobně jsem překročil hranici a jsem trochu ohromený. Toto je můj první plně automatizovaný, LLM generovaný a automaticky formalizovaný důkaz nové matematické věty. Dovolte mi nastavit problém: máme tři rotující kruhy se šesti polohami, všechny tři se protínají v celkovém počtu šesti bodů. Dokažte, že grupa pohybů, kterou generují, je plná symetrická grupa S_{12}. Tento problém jsem si původně všiml v krásné hádance ve hře Machinarium od Amanita Design. Úkol není extrémně těžký, ale zřejmě má dva důkazy: 1. Hrubé vyhledávání konjugace tříd za účelem reprezentace všech transpozic (udělal jsem to před mnoha lety, ale nikdy jsem to nepublikoval). 2. Důkaz generovaný LLM (v tomto případě vytvořený asi před třemi měsíci GPT-5-Pro), nebo vlastně dva důkazy, oba brilantně využívající Jordanovu větu o primitivních grupách (nebo příbuznou variantu, která je ještě přímočařejší). ( Co mi chybělo až do dnešního večera, byl nástroj na automatickou formalizaci tohoto důkazu. Díky @HarmonicMath jsem získal přístup k jejich pozoruhodnému softwaru Aristoteles. Shrnuto, tady je, co jsem udělal: A. Automaticky vygeneroval důkaz pomocí LLM (a spustil ho několikrát, aby získal mnohem lepší verzi). B. Zkrátil důkaz na holý matematický text – definice, výroky, lemata, věty – pomocí důkazů poskytnutých LLM. C. Spustil systém Aristotel přes noc (přes API). Dnes ráno jsem obdržel plně formalizovanou verzi v Lean (asi 700 řádků kódu). Kód se zkompiluje, takže nyní mám certifikát, který potvrzuje, že důkaz generovaný LLM skutečně vedl ke správnému řešení. Navíc jsem získal konceptuální důkaz, lepší než moje vlastní hrubá síla. Plánuji to posunout dál k širší třídě takových algebraických problémů. Je to malý projekt, ale pro mě osobně je to milník. Nyní mám nástroje, které mi díky mé orchestraci skutečně pomáhají objevovat, formalizovat a studovat důkazy matematických vět. To není triviální. Otázky: 1. Jak se to bude v budoucnu rozvíjet? 2. Kolik školení bude potřeba k úspěchu v těchto úkolech?...