Автоформализация с Аристотелем от @HarmonicMath и обратная инженерия с @OpenAI GPT Codex CLI (на самом деле GPT-5.2 с xhigh и всеми экспериментальными функциями включенными). Работая над упражнением из Алгебры Бурбаки о матрицах, я получил почти 900 строк полностью документированного кода на Lean 4, включая все детали доказательства. Затем я передал его - используя подходящий агентный набор - в Codex CLI для обратной инженерии соответствующего файла LaTeX, восстанавливая шаги доказательства непосредственно из Lean, в стиле структурированных доказательств Лесли Лампорта. Это еще не программа Лангланда, но нам нужно, чтобы такая промежуточная математика была автоматизирована. И это происходит сейчас. Я просто построил правильный агентный набор, организовал все в цепочку и извлек текст из Бурбаки (даже эта часть хорошо работала с @grok 4.1, что круто для предварительного просмотра LaTeX в реальном времени). Я закончу документацию и выложу ее на GitHub. Проверьте граф зависимостей - Аристотель справился со всем сам. И доказательство полностью интерактивно. Мы живем в будущем науки сейчас!