LANAプロジェクトと
・コラッツ予想の「AIによる偽証明=Lean 4のカーネルバグ
すり抜け事件(>>657)
・scholzeの警告　(>>658)
proof assistant such as lean

AIに聞いてみた、

➖➖
数学界の外部や批判派の目から見れば、彼らの動きは「純粋な数学的検証」というよりも、ご指摘の通り「Lean 4のコンパイラを何とかして通過させ、『証明成功』という御墨付き（称号）を手に入れるためのハッキング行為」に見えてもおかしくない構造があります。
そう言わざるを得ない背景と、彼らの「真の目的」がどこにあるのかを分析します。

1.
「コンパイラ通過の事実」が喉から手が出るほど欲しい理由。
現在、望月教授のIUT理論は、世界の主要な数学者（ショルツ教授ら）から「ギャップがあるため解決していない」と無視され、論文の検証自体をボイコットされている状態です。
人間同士の議論（ピアレビュー）の場ではこれ以上相手にしてもらえないため、容認派が膠着状態を打破する唯一のウルトラC（大逆転劇）が、「人間ではなく、絶対に客観的であるはずの計算機（Lean 4）に『正しい』と言わせること」でした。

・Lean 4が証明完了（プロンプトが緑色）と判定した」という揺るぎない事実さえ作れれば、「ほら見ろ、世界最先端の数学検証AIが正しいと言っている。認めない海外の数学者が間違っているのだ」と主張する強力な武器になります。
だからこそ、彼らにとっては「現代数学のフレームと違う」と言いつつも、現代数学の基礎論で動くLean 4にIUT理論をねじ込む必要があったのです。