IXThinker·2026-06-23 16:50

陶哲軒指AI證明湧現 數學界陷驗證滯後困境

數學家陶哲軒分享形式化項目最新體驗：人工智能數小時即完成過往需志願者數周的證明任務，但生成證明冗長，人類審閱嚴重滯後。他把這種落差稱為「阻抗不匹配」，並指十七世紀「證明易產難驗」的矛盾被推到極致。

數周任務數小時完成

在該形式化項目中，過往需要志願者花數周認領完成的證明任務，如今人工智能數小時即可搞定，數學證明產出速度出現數量級躍升，令項目推進明顯加速。