>>211-219

面白いやつらだ　（＾＾

>そもそも日本人が賞をとったとかそんなことで喜ぶのがマジ狂ってる
>自分と全然関係ない他人のことじゃん（笑）

しかし
今年のノーベル賞 ダブル受賞を喜ぶ日本人は多いだろう
今年の10大ニュースに入ると思うぞ

>>　命題：leanで形式化できるほど曖昧さなく記述されているなら、数学者は皆その論文が読める筈
>>　と言い換えてみようね

命題：leanで形式化できるほど曖昧さなく記述されているなら、数学者は皆その論文が読める筈
　↓
命題：コンピューター証明で形式化できるほど曖昧さなく記述されているなら、数学者は皆その論文が読める筈
と言い換えてみよう

そもそも 「数学者」の数学的定義がないｗ　（＾＾
もし「コンピューター証明で形式化できるほど曖昧さなく記述されているなら、数学者は皆その論文が読める」
が成立するならば、コンピューター証明なぞ 必要性は薄いな

が 話は真逆で、現代数学の論文は 長大化していて
かつ IUT論文など 本体だけで700ページで
準備論文を入れると 数千ページだという
こんなものを 数学者といえど だれでも かれでも 「読め！」と言われても 実行できなよね

例えば 下記のフェイト・トンプソンの定理が有名で、1960年代初頭に出されて後 2012年9月に
完全に形式化された証明は、Rocq証明支援システムによって検証されという　（＾＾

https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A7%E3%82%A4%E3%83%88%E3%83%BB%E3%83%88%E3%83%B3%E3%83%97%E3%82%BD%E3%83%B3%E3%81%AE%E5%AE%9A%E7%90%86
フェイト・トンプソンの定理（奇数位数定理とも呼ばれる）は、奇数位数の有限群はすべて可解群であることを述べている。この定理は1960年代初頭にウォルター・フェイト（英語版）とジョン・グリッグス・トンプソンによって証明された[1]。
証明はCA定理やCN定理と同じ概要に従っているが、詳細ははるかに複雑である。最終的な論文は255ページで、パシフィック・ジャーナル・オブ・マスマティクスの第13巻第3号全体を占めた[7][8]。
証明の重要性
この証明の最も革新的な側面はその長さであった。フェイト・トンプソンの論文以前は、群論における議論は数ページを超えるものはほとんどなく、ほとんどが1日で読むことができた。群論の研究者たちがそのような長い議論が可能であることを認識すると、数百ページに及ぶ一連の論文が発表されるようになった。
証明の改訂
完全に形式化された証明は、Rocq証明支援システムによって検証され、2012年9月にジョルジュ・ゴンティエ（英語版）とマイクロソフトリサーチおよびINRIAの研究者によって発表された