>ああ Lean形式化の発表でギャップ見つかった話？ ギャップ埋めればいいだけでしょ？
ああ リーマン予想は未証明って話？ 証明すればいいだけでしょ？