＞こちらは驚き
＞”それに近いものが存在します。形式検証プログラムです”

＞つまりコンピューターによる定理証明のことである......つ、ついに

これができないのが問題なんだよな。lean にしても coq にしても通常の述語論理の上に帰納的な公理群を導入した理論の検証しかできない。全然別の言語体系、推論体系でもそれがきちんと明記されていればそれに準ずる検証プログラムをつくることはできるけど、今回はそもそもそれがない。
大体それができる状況でも難しいのはそのプログラムに乗せるためには曖昧な自然言語で書かれた論文を論理体系の要求する言語におとす時点で行間を埋める作業が発生する。一応曖昧な部分が２０～30か所くらいで選択枝が二択～三択しかないなら全数検査もできなくはないだろうけど、それとて「その選択枝のなかにはなかっただけ」という言い訳が成立してしまう。
結局こういう曖昧な「自然言語」で論文が記述されてる現状では「正しい」ことの検証はできても「まちがってる」ことの検証はできない、今みたいな「それはあなたの読み間違い」という言い訳を許す限り。
そんな言い訳はしてはならないというのが不文律。そんな不文律お構いなしなんだからどうしようもない。