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