用 Lean 4 形式化难题,让 AI 定理证明器自动为定理找证明

satnam6502 · x · 2026-09-21

作者 satnam6502 回应「理论计算机科学家将最先被 AI 自动化取代」的观点，表达相反期待：希望 AI 能把理论计算机科学的成果用于解决实际问题。他所在的团队正用 Lean 4 形式化语言把问题编码，让 AI 定理证明器自动寻找证明，从而把复杂系统的分析与验证自动化，让更广泛的用户可用。他认为 AI 的魔力在于连接「冷僻数学」与「晶体管里电子怎么走」。

他同时承认，对理论计算领域来说，理论工作率先被自动化确实是严峻的现实。