ケビン　バザードはleanによる形式化
の専門家。

>数学はどこへ行くのか？

過去2500年間、数学のやり方は驚くほど変化していません。
ユークリッドの『原論』には補題.定理. 証明が記されており、その内容は過去の研究を基盤としつつ現代の数学の教科書と基本的に同じスタイルで提示されています。

こうした惰性(慣性)の結果として、人類は今や驚異的な数学的知識の集積を誇っています。

この知識は大部分は正しいものの、 時には提示が不十分で参考文献も乏しく「専門家だけが知っている」という場合もあり、多くの誤り（中には深刻なものも）を含み、ABC予想のような茶番劇的な状況を生み出しています。
ABC予想は、著名な学術誌に証明が掲載されたものの、多くの人が正しいとは信じていない重要な予想です。

注意.
著名な学術誌は京大数理研
の数学誌PRIMS (望月新一編集委員長)