Auto-formalization with Aristotle by @HarmonicMath and reverse engineering with @OpenAI GPT Codex CLI (actually GPT-5.2 with xhigh and all the experimental perks enabled). Working on an exercise from Bourbaki’s Algebra about matrices, I obtained almost 900 lines of fully documented Lean 4 code, including all the details of the proof. I then passed it-using a suitably designed agentic setup-to Codex CLI to reverse-engineer the corresponding LaTeX file, reconstructing the proof steps directly from Lean, in the style of Leslie Lamport's structured proofs. This is not the Langlands program yet, but we do need this kind of intermediate-level mathematics to be automated. And this is happening now. I simply built the right agentic setup, pipelined everything, and scraped the text from Bourbaki (even that part worked well with @grok 4.1 which is cool for previewing LaTeX live). I will finish the documentation and post it on GitHub. Check the dependency graph-Aristotle handled it all by itself. And the proof is fully interactive. We are living in the future of science now!