いくら人間が無能でも、もうすぐ、おそらくClaude-Fable5とLean4で確実に決着がつくだろう。
検算担当の数学者がこの領域で素人だったとしても、地盤を整えたら確実にAI+Leanで突破できる。
素人がバイブコーディングでアプリ作れてしまうのと一緒。
Leanが証明不成立を形式証明したらそれで終わり、ご本人がどう言っても揺るがない、
そして、じゃあどうしたら証明できる？とプロンプト投げたら、それまでの知識で、こうやればいいです、とAIが証明して大騒ぎになるに決まってる。