Claude 证 FLT 走了 Wiles 原始证明而非简化版，团队考虑贡献 Tau Ceti

jacobaustin132 · x · 2026-09-07

在 Claude 形式化费马大定理证明后的后续讨论中，@jacobaustin132 透露团队打算继续推进：Claude 走的是 Wiles 的原始证明路径，而非 Kevin Buzzard 一直在做的简化版本，因此难度更大。

后续选项包括向 Lean 社区孵化中的 Tau Ceti 项目贡献，或整理清理自己的证明。littmath 在上下文中表示，更好的做法本可以是先与 Kevin 沟通其项目目标（如高质量、可复用地形式化大量中间结果），并兼顾这些目标与最终结果。