Lean 中正素数费马大定理的完整形式化
形式语言与自动机理论
2025-06-16 v3 计算机科学中的逻辑
数论
摘要
我们在 Lean4 定理证明器中对正素数情形的费马大定理进行完整形式化。我们的形式化包含对 Kummer 引理的证明，这是费马大定理针对正素数的主要障碍。与其遵循通过类域论证明 Kummer 引理的现代方法，我们采用 Hilbert 定理 90-94 的方式进行证明，这种方法更适合形式化处理。
引用
@article{arxiv.2410.01466,
title = {A complete formalization of Fermat's Last Theorem for regular primes in Lean},
author = {Alex Best and Christopher Birkbeck and Riccardo Brasca and Eric Rodriguez Boidi and Ruben van De Velde and Andrew Yang},
journal= {arXiv preprint arXiv:2410.01466},
year = {2025}
}