ケビン.バザードkevin Buzzard
はleanによるproof formarism
communityの有力な一員。

・IUT論文によるabc予想の証明へ
批判は(>>881)。

・現在FLTの証明形式化のprojectが進行している。
The Fermat's Last Theorem Project

> However, I attend the London Number Theory Seminar on a regular basis, and most weeks I note that Lean does not know enough modern mathematical definitions to even state the results announced in the seminar, let alone to check their proofs.

>しかし、私は定期的にロンドン数論セミナーに参加しているが、ほとんどの週に、リーンはセミナーで発表された結果を述べるのにさえ十分な現代数学の定義を知らず、ましてやそれらの証明を確認することなど到底できないと気づく。
deepl

➖ ➖
https://leanprover-community.github.io/blog/posts/FLT-announcement/