我個人已經越過了一條界線，現在有點敬畏。 這是我第一個完全自動化、由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. 成功完成這類任務需要多少訓練？...