“Formalizing Fermat”工作坊

摘要

“Formalizing Fermat”工作坊将于2026年7月6日至10日在伦敦举行，目标是推进EPSRC资助的、在Lean中形式化费马大定理的项目。组织者称，项目最初设想是把FLT化归到1980年代已知定理，即形式化Wiles/Taylor–Wiles论文；实际路线则是更现代、思路可追溯至Khare策略的证明。组织者刚完成11讲相关课程，并将与数论/Lean专家及自动形式化专家合作，试验AI能否形式化所需前提乃至核心证明思想。他认为自动形式化虽有进步，但尚不能可靠地自主形式化定义或定理陈述；定义密集的复杂部分可能效果差，而mathlib中定义齐备、人类文献记录充分的部分可能效果好。