>>346-347
>Scholzeさんの例は有名すぎるのでもう一つ。。。Tim GowersさんやTerence TaoさんのMarton conjecture>解決の論文も、Lean4での形式化が企画されてますね。
>[https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/]

・いいね。それありかも
・つまり、川上懸賞金の100万ドル（1.5億円）を狙って
　コンピュータ検証にかける
・IUTがダメなら懸賞金ゲット！
　IUTが白でも、それなりに賞貰えそう（10万ドル（1.5千万円））
・やった人は、一躍有名人だ