Automatická formalizace s Aristotelem od @HarmonicMath a reverzní inženýrství s @OpenAI GPT Codex CLI (ve skutečnosti GPT-5.2 s povoleným xhigh a všemi experimentálními perky). Při práci na cvičení z Bourbakiho algebry o maticích jsem získal téměř 900 řádků plně zdokumentovaného Lean 4 kódu, včetně všech detailů důkazu. Poté jsem jej – pomocí vhodně navrženého agentického nastavení – předal Codexu CLI k reverznímu inženýrství odpovídajícího LaTeX souboru, přičemž jsem rekonstruoval důkazní kroky přímo z Lean, ve stylu strukturovaných důkazů Leslie Lamportové. To zatím není Langlandsův program, ale potřebujeme automatizaci tohoto druhu matematiky na střední úrovni. A to se děje právě teď. Jednoduše jsem vytvořil správné agentické nastavení, všechno pipelinel a text z Bourbaki převzal (i tahle část fungovala dobře s @grok 4.1, což je super pro naživo LaTeX). Dokončím dokumentaci a zveřejním ji na GitHubu. Zkontrolujte graf závislostí – Aristoteles to zvládl sám. A důkaz je plně interaktivní. Žijeme v budoucnosti vědy už teď!