26/01/20 23:36:08.10 gpfTHpPc.net
今月号のニュートンでこの事に関する特集記事が載ってたけどLeanの専門家でも論文全部をプログラミングするだけで10年以上、賛否が分かれる箇所に絞っても数年がかりになる見通しだそうだ
Leanのセミナーに望月氏も参加して好意的な感触を持ったそうだがニュートン編集部の質問には答えなかったっていう
45:名無しのひみつ
26/01/22 16:53:31.09 DojZpKk0.net
あのね
形式的な証明を書けるくらいなら
他の専門家にとって曖昧なところなんてあるはずがないんだよ
最先端の研究で証明系が活躍するのなんて
場合分けが多過ぎて人手では無理なケースが殆ど
門外漢は形式的な証明なんてすぐ書けると思っているかもしれないが
証明系をフルに使いこなせる人でも
人間が書いた「曖昧な証明」を形式的に書き直すのは相当な手間がかかる
サッカーボールを直接ゴールに蹴り込むんじゃなくて
一旦全部品に解体してゴールの中に持ち込んで組み立て直すに近い
分解してる時にようやくああ俺の証明の構造はこうなっていたのだと分かる
それに度々部品が足りなくなっていることが組立中に分かる
その時にようやく自分の証明の数学的構造が理解される
数学は意外と直感的なのだ
そして殆ど全ての数学者は死ぬまで直感的にしか数学をやらない
46:名無しのひみつ
26/01/22 16:59:25.24 DojZpKk0.net
例えば命題論理の完全性の証明でもこのくらいの記述量になる
Foundation/Foundation/FirstOrder/Completeness at master · FormalizedFormalLogic/Foundation · GitHub URLﾘﾝｸ(share.google)
47:名無しのひみつ
26/01/23 07:17:04.70 OqRSLrNT.net
リーマンの写像定理 を形式証明するとどんなもんだろうか。
48:【国際コピペ連合日本支部推薦】
26/01/30 13:43:55.00 kjmvPDKS.net
>>45
＞場合分けが多過ぎて人手では無理なケースが殆ど
いわんとするところは、ごもっとも。
が、以下のざまは個人的感想であることを願う。
＞分解してる時にようやくああ俺の証明の構造はこうなっていたのだと分かる
＞それに度々部品が足りなくなっていることが組立中に分かる
＞その時にようやく自分の証明の数学的構造が理解される
＞数学は意外と直感的なのだ
＞そして殆ど全ての数学者は死ぬまで直感的にしか数学をやらない
こんなんで証明した、論文を書いた、ことになるなんて、オカシイな、数学者の能力を過小評価してないかな、と思う。
49:名無しのひみつ
26/02/04 15:04:37.37 UGJlZdGL.net
既に証明されたとされる内容を、コンピュータを使って
コンピュータに証明を検証納得させるためのコードを
何十万行書いていても、それで証明が検証完了したとし
ても、数学上の業績としてはほぼ認められないことだろう。
五目並べ（連珠ではない）は先手必勝であることが江戸時代に
出版された本にその方法と共に既に記述され解明されている
そうであるが、それを形式証明したとしても数学の業績には
なるまい。定理検証系のデモにしかならない。
50:名無しのひみつ
26/02/04 17:31:04.03 WzjwzzYf.net
証明論文の査読が済んで数学界の誰もが認めるようになる事と証明の間に何の関係があるんだろうか
著者や他人が正しいと信じててそれ以上誰もツッコミを入れられなくなったってだけじゃないのか
51:名無しのひみつ
26/02/04 18:38:56.65 kV23Sb9t.net
>>50
スーガクなんて、そもそもそんなもんなのよ（笑）
52:名無しのひみつ
26/02/05 06:26:14.63 ZJKB9NXU.net
数学的には成り立つが、無限後退の罠にハマってて、『実在する宇宙』として成立せえへんが、
コンピューター的には、正解となるんじゃね。理屈で考えても分かることをやってるだけ。
53:名無しのひみつ
26/02/05 07:59:08.66 4tMdSiSk.net
定理証明系と最先端の数学の距離はかなり近いものになりました
Vladimir Voevodskyなんかも検証に使う事を勧めてましたし
数学と計算機工学の関係は
数学から計算機工学への貢献がほぼ一方的でした
ところが最近は圏論的といっていいような数学的手法の他の数学分野の移入が盛んになり
代数的トポロジーの手法を代数幾何学に導入みたいなことです
計算機工学の中の特にソフトウェア工学の手法が脚光を浴びています
ソフトウェア再利用の手法が、特に一般化の手法が
数学的手法の一般化の整理にも応用できることが分かってきたからです
もともとプログラムの形式的検証などの分野で
ソフトウェア手法の数学的構造もよく研究されていましたし
プログラムの意味論と数学の証明論の関係も詳しく研究されていたので下地はあったと思います
The Unreasonable Effectiveness of Mathematical Experiments: What Makes Mathematics Work
Asvin G.
URLﾘﾝｸ(arxiv.org)
がお勧めです
54:名無しのひみつ
26/02/05 15:56:17.40 4tviL2Ho.net
ピンの上で何人の天使が踊れるか、
を真剣に論じていたのがカトリックの神学だというね。
55:名無しのひみつ
26/02/05 16:09:11.78 wJtnRmRG.net
>>43
これらの批判に対して、証明の査読をした人たちはどう考えているのかな。
興味深いところだ。まさか目をつぶっているわけではなかろう。
56:名無しのひみつ
26/02/05 19:55:39.03 vdX3s2FK.net
>>55
よくわからなくて問題点を指摘できなかったんだと思う
割と本気で
57:名無しのひみつ
26/02/06 10:57:57.27 fXXk955T.net
所詮この世のすべての定理や命題を把握して
すべての証明に目を通してそれを理解して
正しさを自分自身の頭の中で検証し尽くす
ことなどもはや不可能・無理。他人が証明
した、他人が検証したというものを受け入
れてひたすら前に進むだけ。そうして時々
パラドックスが発見されたなら、その起源
を探して、穴を塞ぐ。最初から下絵があって
完成された体系を塗り絵として作っている
わけじゃないだろう。
58:名無しのひみつ
26/02/11 17:02:42.77 EKlToAnE.net
そのコンピュータシステムが
ＣＰＵチップやその周辺の回路などのハードウェア、
ＯＳ、コンパイラ、ネットワーク、エラー処理、
割り込み、基本ライブラリ、検証用ソフトなど
すべてを含めて、数学的に正しいことも証明して下さい。
そうでないと、証明は完全ではありません。
59:名無しのひみつ
26/02/11 17:15:14.98 EKlToAnE.net
証明の為にはこれ以上簡単なＣＰＵは無いというほど
単純な機械語命令を持つものを造り、それを複数並べて
各命令サイクルごとにすべて同じ結果をＣＰＵが
入力し、出力していることを監視しながら動作させます。
パイプラインとか先行制御とか命令の複数実行とか
命令の順序変更などの機構は含まない単純明快なCPUの
構造にします。もちろんマルチコアなど厳禁です。
チップの回路図を複数のチップ製造メーカーに送って、
独立にトランジスター・ゲートレベルで製造して貰います。
同じ製作所に頼むと、CPUの製造にバグがあれば、何個並べて
CPUへの入出力が一致するかを調べたとしても意味がありません。
また機械語命令が単純なものしかないことは重要です。
コンパイラも簡単な高級言語を最適化などせずに機械語に
翻訳することが必要です。そうして独立に作られた複数の
コンパイラが出してきた機械語命令を相互に使って結果を
検証します。。。。。。
不確定さを極力排除するために、外部からの割り込みや
ネットワークへの接続は厳禁です。
OSも単純明快なものとして、単一のプログラムだけが
走るようにして、並行処理などはせず、一種のプログラム
ローダーのような単純さに徹するべきです。。。。。
OSの正しさ、コンパイラの正しさの数学的検証は大変です。
そうして高級言語で書かれた、証明の正しさを検証する
プログラムやその周辺ライブラリの数学的正しさの証明や
検証も困難ではないでしょうか？
計算プログラムを走らせてその結果を目で観る役割の
人間の頭も狂っていたら、話が全部ダメになります。
頭や精神の正しさを数学的に証明することは、
たぶん無理です。なぜなら数学的にモデル化されていないし、
モデル化されたものが現実と一致していることをどうやって
保証・証明するのでしょうか。
60:名無しのひみつ
26/02/11 17:30:46.13 0srxEckw.net
>>59
Hoareさんこんにちはもう90歳超えてますよね？
61:名無しのひみつ
26/02/11 17:48:41.24 +wMtjwxJ.net
最初は宇宙祭りに見えたわ、一体どういう祭りかと
62:【国際コピペ連合日本支部推薦】
26/02/12 18:10:30.90 FBAp2ym4.net
>>59
中途半端な数学かぶれが現実世界の問題に口出しすると、こうなるよ、という典型例。
もうこの時点で破たんしている。：
＞チップの回路図を複数のチップ製造メーカーに送って、独立にトランジスター・ゲートレベルで製造して貰います
「複数のチップ製造メーカーに」って現実世界では高々《有限》しか存在できないチップ製造メーカーだから、そこから出荷される有限個の製品で、「数学の検証が可能」といえる保証が一体ドコにあろうか？
63:名無しのひみつ
26/02/13 15:06:59.01 blhdl1cf.net
>>1の照明に下記のAIを使用すればよいのでは
Gemini 3 Deep Thinkのアップグレード版が登場、知性を測定するARC-AGIで驚異的な記録を更新
2026年02月13日 13時00分
URLﾘﾝｸ(gigazine.net)
GoogleがGemini 3の推論能力強化版である「Gemini 3 Deep Think」のアップデートを実施したことを2026年2月12日に発表しました。アップデートは研究者と緊密に連携して困難な研究課題に取り組むことに焦点を当てたもので、各種ベンチマークで驚異的なスコアを記録しています。
Gemini 3 Deep ThinkはAIの知能を測定するベンチマーク「ARC-AGI-2」で高いスコアを記録しました。以下は左が2025年12月の発表時におけるGemini 3 Deep ThinkのARC-AGI-2スコアで、この時点で45％と他の主要モデルと比較してかなり高くなっていました。そして、アップグレード版では以下の画像右のグラフにあるように、ARC-AGI-2スコアが84.6％と驚異的な数値まで上昇しています。
そのほか、AIの知識の限界をテストするために設計されたベンチマーク「Humanity's Last Exam」では48.4％、マルチモーダルLLM向けテスト「MMMU-Pro」では81.5％と、いずれも高い水準を記録しています。さらに、競技プログラムベンチマークの「Codefoces」では、3455と驚異的な数値を達成しました。
Gemini 3 Deep Thinkは、数学や競技コーディングに加え、化学や物理学といった幅広い科学分野で優れた性能を発揮します。Googleによると、アップデートされたDeep Thinkモードは2025年国際物理オリンピックおよび化学オリンピックの筆記試験で金メダルレベルの成績を収めているとのこと。また、高度な理論物理学の指標である「CMTベンチマーク」で50.5％のスコアを達成し、高度な理論物理学における熟達具合も示されています。
GoogleはGemini 3 Deep Thinkが実際の科学研究に役立っていることをアピールしています。以下はデューク大学で新しい半導体材料を研究するラボにおいてGemini 3 Deep Thinkが活用されている様子。半導体の材料の潜在的発見を目指して、複雑な結晶成長のための製造方法を最適化するためにGemini 3 Deep Thinkが利用されており、従来の方法では達成が困難だった正確な目標値を達成することができたとのこと。
また、ラトガース大学の数学者であるリサ・カーボン氏は、既存の学習データがほとんどない分野の研究において、Gemini 3 Deep Thinkを用いて高度に技術的な数学論文の査読を行いました。これにより、人間の査読では見過ごされていた論理的欠陥を的確に特定することができたと報告しています。
アップデートされたGemini 3 Deep Thinkは、記事作成時点ではGoogle AI Ultraの加入者向けに展開されています。また、一部の研究者、エンジニア、企業に対してGemini API経由でGemini 3 Deep Thinkを利用できる早期アクセスプログラムが提供されています。
64:名無しのひみつ
26/02/17 15:03:23.40 JoZIVgau.net
たとえ100人が査読して正しいと判定した論文でも、
もしも抜けや穴や間違いがあれば、結局は正しく
は無い論文である。ただその欠陥が発覚していない
だけかもしれない。