>>411
>そもそも証明検証ツールが本格的に運用されるようになったのは今世紀以降。

ショルツがやったやったやつみたいに
ホッカホカの最新の数学が検証されたのはたしかに最近

>いかなる非形式的証明もギャップが無いことが検証されていない。

これは言い過ぎでIsabelle, HOL, Coqは前世紀から使われてるし
利用する公理の範囲を検討する逆数学との関係で
ギャプ探しは結構行われてた