在這裡，我呈現了一篇最近數學論文的完整自動形式化（又一次！） Barańczuk, Stefan. "在有限域上定義 n-空間子集的方程數量減少。" 《圖盧茲科學學院年報：數學》，第 6 卷，第 33 期，第 1 期（2024）：177–182。 我在這個項目上花了幾天時間。首先，我運行了 @HarmonicMath 的 Aristotle，這在大約 15 小時內完全自動形式化了證明。然後，在 @PietroMonticone 的大力幫助下，我成功設置了一個證明的藍圖版本。這是一個所有 LaTeX 文檔部分變得互動並可以檢查和研究的版本。我們可以看到證明中的依賴關係並研究它們的關係。 在後處理階段，我還使用了 Grok Heavy 和 Codex CLI，搭配 GPT-5.2 的 xhigh 模式，逐行分析了正式證明。這對於不是專業 Lean 4 程式設計師的人來說是很大的幫助。你真的可以內化證明的所有步驟。 我想總結一下我的印象以及我從這次經歷中學到的東西。@vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei

數學論文需要正式的驗證。這通常由裁判非正式地進行。但如果我們能依賴更穩健的東西，比如自動形式化到 Lean 4，那麼裁判的角色將減少到對定義和定理的表述進行仔細檢查？自動生成代碼的編譯將成為一個證明證書。這就是我與 @HarmonicMath 一起進行的長期運行的結果。 感謝 @PietroMonticone 和 @llllvvuu 幫助設置藍圖。在這裡，我展示了我朋友 Stefan Barańczuk 關於切比雪夫可除序列的論文的完整正確自動形式化。這段代碼大約有 5000 行高度非平凡的 Lean。它修正了主論文中的所有不一致和漏洞（甚至證明了一些委託的命題）。 我將發佈一系列這樣的實驗，證明在數學的某些領域，包括初等數論、組合學和分析（所有由 Mathlib 涵蓋的各種內容）中，我們距離證明有效性的文檔大規模轉變並不遙遠。我認為這將是一個忙碌的一年！

如果我今天是一名學生，與最先進的LLM互動幾乎會讓人感覺像是在作弊。今天早上，我隨意拍了一張黑板的照片，並請ChatGPT-5.2-Pro解釋上下文、解決方案以及一些關於著名的Chevalley定理在可構造集合上的附註。我收到了一份相當深入的報告，綜合了來自互聯網的高質量代數幾何材料。 這引發了一個嚴肅的問題：今天的學生真正的努力和挑戰是什麼？成本無疑是一個因素，但一旦可以訪問這些模型，應該如何在這個豐富的土地上學習，這裡的解釋、參考資料和互動探索都能立即獲得？ 也許掙扎不再是獲取信息或理解個別論點，而是發展判斷力：知道該問哪些問題，信任哪些解釋，如何識別深度與表面似是而非，如何內化思想而不僅僅是消費它們。在一個答案豐富的環境中，真正的困難可能在於形成品味、數學直覺，以及在這突如其來的知識過剩中導航的能力，而不是淹沒在其中。