Fermat’s Last Theorem in Lean: The Community Project and Claude’s Real Role

The formalization of Fermat’s Last Theorem (FLT) in the Lean proof assistant remains an ongoing community-led effort. It should not be attributed to Claude as a completed, first formalized proof. The