25/12/21 18:51:52.79 IMnp+6Hg.net
>>211-219
面白いやつらだ （＾＾
>そもそも日本人が賞をとったとかそんなことで喜ぶのがマジ狂ってる
>自分と全然関係ない他人のことじゃん（笑）
しかし
今年のノーベル賞 ダブル受賞を喜ぶ日本人は多いだろう
今年の10大ニュースに入ると思うぞ
>> 命題：leanで形式化できるほど曖昧さなく記述されているなら、数学者は皆その論文が読める筈
>> と言い換えてみようね
命題：leanで形式化できるほど曖昧さなく記述されているなら、数学者は皆その論文が読める筈
↓
命題：コンピューター証明で形式化できるほど曖昧さなく記述されているなら、数学者は皆その論文が読める筈
と言い換えてみよう
そもそも 「数学者」の数学的定義がないｗ （＾＾
もし「コンピューター証明で形式化できるほど曖昧さなく記述されているなら、数学者は皆その論文が読める」
が成立するならば、コンピューター証明なぞ 必要性は薄いな
が 話は真逆で、現代数学の論文は 長大化していて
かつ IUT論文など 本体だけで700ページで
準備論文を入れると 数千ページだという
こんなものを 数学者といえど だれでも かれでも 「読め！」と言われても 実行できなよね
例えば 下記のフェイト・トンプソンの定理が有名で、1960年代初頭に出されて後 2012年9月に
完全に形式化された証明は、Rocq証明支援システムによって検証されという （＾＾
URLﾘﾝｸ(ja.wikipedia.org)
フェイト・トンプソンの定理（奇数位数定理とも呼ばれる