我個人已經越過了一條界線，現在有點敬畏。 這是我第一個完全自動化、由LLM生成並自動形式化的新數學定理的證明。 讓我來設置這個問題：我們有三個旋轉的圓，每個圓有六個位置，這三個圓在總共六個點上相交。 證明它們生成的運動群是完整的對稱群 S_{12}。 這是一個我最初在Amanita Design的遊戲《Machinarium》中注意到的可愛謎題。 這個任務並不是特別困難，但顯然有兩個證明： 1. 對共軛類進行暴力搜索以表示所有的置換（我在很多年前做過這個，但從未發表過）。 2. 一個LLM生成的證明（在這種情況下是三個月前由GPT-5-Pro生成的），實際上有兩個證明，兩者都以精彩的方式使用了喬丹關於原始群的定理（或一個更直接的相關變體）。 直到今晚，我才缺少一個自動形式化這個證明的工具。 多虧了@HarmonicMath，我獲得了他們卓越的軟體Aristotle的訪問權限。總結來說，我做了以下幾點： A. 使用LLM自動生成證明（並多次運行以獲得更好的版本）。 B. 將證明修剪到最基本的數學文本——定義、命題、引理、定理——由LLM提供的證明。 C. 通過API在夜間運行Aristotle系統。今天早上我收到了Lean中的完全形式化版本（大約700行代碼）。 這段代碼可以編譯，所以我現在有一個證明，確認LLM生成的證明確實導致了一個正確的解決方案。此外，我得到了比我自己的暴力證明更好的概念證明。我計劃將其推進到更廣泛的此類代數問題。 這是一個小項目，但對我個人來說，它標誌著一個里程碑。我現在擁有的工具，通過我的協調，確實可以幫助我發現、形式化和研究數學定理的證明。這並非易事。 問題： 1. 這在未來將如何擴展？ 2. 成功完成這類任務需要多少訓練？ 3. 我們應該如何對待這些證明的著作權？ 4. 數學家的更深層角色是什麼？

有誰計劃參加嗎？ 這將會非常有趣！

我非常期待新架構的原因之一是，代數拓撲中的問題根本上需要超越簡單符號操作的直覺。通常，呈現基於同倫/同調的論證的視覺草圖要比設計精確的公式並使其完全正式容易得多。 我希望世界模型、符號操作和物體動態的表示的結合能成為通往全新架構的道路。如果我們想解決超越單純文本的困難數學問題，我們需要這些架構。 在這張圖片中（基於 arXiv: 2107.01664），你可以看到直覺理解手銬悖論是多麼容易，但用公式正式寫出來又是多麼困難。