與亞里士多德的自動形式化，@HarmonicMath 和 @OpenAI GPT Codex CLI（實際上是啟用了 xhigh 和所有實驗性功能的 GPT-5.2）。在處理 Bourbaki 的代數中有關矩陣的練習時，我獲得了將近 900 行的完整文檔 Lean 4 代碼，包括證明的所有細節。 然後，我使用一個適當設計的代理設置將其傳遞給 Codex CLI，以反向工程相應的 LaTeX 文件，直接從 Lean 重建證明步驟，模仿 Leslie Lamport 的結構化證明風格。 這還不是 Langlands 計劃，但我們確實需要這種中級數學的自動化。而這正在發生。我只是建立了正確的代理設置，將所有內容串聯起來，並從 Bourbaki 擷取文本（即使那部分也與 @grok 4.1 一起運行良好，這對於實時預覽 LaTeX 很酷）。 我將完成文檔並將其發布在 GitHub 上。檢查依賴圖——亞里士多德自己處理了所有事情。而且證明是完全互動的。 我們現在正生活在科學的未來中！