【海外の反応】AIがフェルマーの最終定理を形式化、1300万行のコードに驚きの声
姉妹サイトの新着
他サイトの新着
- 5chまとめMAP【中国】日本の高校の文化祭が中国ネットで大反響＝「うらやましすぎる」「来世は絶対日本の学校に…」
- ニュース速報まとめMAP【サッカー】背番号18の重み。上田綺世はリールで「第二の鎌田」になるか、それとも「期待外れ」に終わるのか？
- なんJ傑作まとめアンテナMAP【悲報】トヨタさんが頑なに小型ミニバンを作らない理由、ルーミーはダイハツ製・・・・・・・・・
- アニメ声優まとめアンテナMAP【悲報】戦争反対のアニメーターさん、異論を拒絶 対話で解決は不可能ということを身を持って証明
- VTuberまとめアンテナMAP【Vtuber】園長駅長委員長って委員長以外はVTuber界隈でこの人って印象つかないようになってるのか
- だめぽアンテナ【ウマ娘】ルラち「やっぱセ●なんてダッセーよな～！」
- ヌルポあんてな元F1TD「アストンマーチンが問題はすべてホンダのせいだと世界に訴える関係はパートナーとは呼べない」
- 2chまとめアプリ+小学生中学生時代は足早い奴がモテる←これ
- News人PS版『ドラゴンクエスト7』のディスクに隠された秘密が話題に！気付いた人すげえええええええ！！他
- ブルーアンテナ佐藤理亜 画像666枚【セミヌード】
- ウマーあんてなうんこ拭いた紙でちんこ拭いてしまった
- まとめクローラ生活は母親に依存、ひきこもり状態「葬儀代に大きな金がかかり、払ってしまえば生活ができなくなる」 ８９歳母の遺体３か月放置した女性の困窮・・・中高年になった子どもを高齢の親が支える８０５０問題 9/4
- ２ちゃんねるまとめるまとめ【衝撃】ナルトさん、一人ぼっちだったの実は完全に嘘だったｗｗｗ
- 勝つるあんてな！【速報】36歳・年収1100万円の婚活男性、ガチで究極すぎる2択に悩まされてしまう
- ぷぅアンテナ【画像】超絶ヤバイ！伊織もえのエチエチ写真におっさん達の股間が限界突破ｗｗｗ 他
- 5chnavi【芸能】死んだ時に良い人扱いされたのが謎だった芸能人・俳優👈だれそうぞうした？
- にゅーもふ【個人撮影】 妊婦の嫁のために泊まりで家事の手伝いに来てた嫁の妹とめちゃくちゃセ●クスしたｗｗｗｗｗｗ
- 海外の反応アンテナ.com海外「日本の食べ物この3つの組み合わせは世界最高だよ」
- 海外反応・海外ニュースまとめ【海外の反応】ドラゴンボール超、映画とアニメでやった話をまた作り直すと発表→「もう3周目だぞ」
- キター！アンテナ【長崎】「会話するため近づいた」70代の男性作業員が使っていた草刈り機の刃が66歳男性作業員の右脚に
Anthropicが、AIモデルClaudeを使ってワイルズによるフェルマーの最終定理の証明を形式検証言語Lean上で完全に形式化したと発表した。作業にかかった期間は約11日で、その過程で1300万行のLeanコードと29500個の中間定理が生成されたという。この報告はHacker Newsで大きな話題になり、「人間には読み切れない量のコードを何が検証しているのか」という信頼性への疑問と、「数学的発見という体験そのものが機械に奪われるのでは」という寂しさ、両方の反応が入り混じった。
フェルマーの最終定理の形式化
出典: anthropic.com / 元記事はこちら
ちょうど投稿されたKevin Buzzardのブログ記事も読むといいよ。今回の成果が何を意味していて、何を意味していないのかがよく分かる
数学は得意じゃないけど、Kevinはもっと彼女と旅行に行くべきなんじゃないか、数学界全体のために
『自分のプロジェクトには5年で100万ポンドの予算がついたが、Anthropicはわずか11日で終わらせた。ただ、お金はもっとかけているのではとも思う』——規模感が伝わってくる
あの『Anecdote』の項が好きだ
1300万行のコード、Leanの証明システムに潜む未知のバグを突いてしまっている可能性はないのか?
『その過程で1300万行のLeanコードを書き、29500個の中間定理を証明した』とのこと。正気とは思えない量だ。正しさが検証可能なことなら、モデルにできない仕事はないという説にまた説得力が増した
これをフェルマーが余白に書けたはずがない。彼の名誉は完全に守られたわけだ
余談だけど、Simon Singhのこの本は本当におすすめ
間違いない、とても示唆に富む本だ
おお、Claudeのおかげで、Leanがまたひとつチェックボックスを埋めたみたいだ
しかもそれが最後の1個らしい
FLTの証明はAndrew Wilesにとって深く感情的で精神的な体験だったようで、読んでいて涙が出そうになった。機械がこの驚きと体験を人間から奪ってしまうのは本当に悲しい。でも、生物としての限界の先に何があるのか想像すると、それはそれでわくわくする
奪われることはないと思う。Brandon Sandersonの最近の動画で見た話が、創作に限らず好きなもの全般に当てはまる
形式化することと発見することは別物。人間の創意工夫が入り込む余地はまだたくさん残っている
生物としての『限界』を快適さや進歩と引き換えにするとき、その代償が精神的な充足感なんじゃないかと思う。かつて屋外でしていた仕事や、何千年も従ってきた昼夜のサイクルなど、いろんなところで同じことが起きている気がする
コードはここで公開されている
すごい。Buzzardのグループは先を越されたわけだ
AIはどんな知的作業も、人間よりはるかに速く、確実に、大規模にこなせるポテンシャルがあるのは明らかだと思う。問題は、それがどこまで許されるのか、そしてそうなったあと人間はどうなるのか、ということだ
行き着く先は大規模な貧困と暴力で、それをAIを持つ側がAI監視とAI兵器で抑え込む未来だと思う。AIは人々を分断させ、戦争を正当化して忙しくさせておくために使われる。楽しい未来が待っているものだ。このテクノロジーの何にそんなに興奮できるのか分からない
フェルマーの最終定理の全貌を描いたSimon Singhの本はおすすめ。とても面白いし、最終的な解決に関わった、本当に本当に変わった人物たちが次々出てくる
詳しい人に頼みたいんだけど、頭の中にある素朴な疑問に答えてほしい。『その過程で1300万行のLeanコードを書き、29500個の中間定理を証明した』とあるけど、この1300万行を人間がチェックしたのか?こういう仕事のQAってどうやるんだ?
Leanでコードを書く意味は、Lean自身がそれをチェックしてくれるという点にある。Leanは数学的な推論を、誤魔化しがきかない形でエンコードするための専用言語だ
定理証明支援系のいいところは、途中の行を人間が読む必要がないこと。確認すべきなのは、目標(結果)が本当に自分の思っている主張と一致しているかどうかだけで、途中経過はすべて証明系が検証してくれる
LLMは地道な作業をこなすのは得意なようだ。では、Andrew Wilesのような天才的なブレイクスルーを生み出すのはいつになるんだろう?
2ヶ月くらい前にもう起きてる
さて、ガラス玉演戯はこのあたりで置いておいて、山の湖にでも飛び込みに行くとするか
素朴な質問だけど、生成された証明にバグがあって、本当は正しくないのに『正しい』と判定されてしまう可能性はないのか?それとも、最初に証明しようとしている命題さえ正しく指定できていれば、あとの過程は関係ないということなんだろうか
次は/simplifyだ。半分のサイズにできないか?いつかこの証明がこれ以上簡略化できないことを証明する人も出てくるんじゃないか
できる。FLTは『n-単体が2次元より高い次元でハイパーキューブと等価な表現に変換できない』という事実から従う(※文末の/sは皮肉のサイン。でたらめな説明であることを示している)
他サイトの新着
[github]のステータスは『自己申告』となっている。1300万行のLeanコード、LeanとNanodaのカーネルはCollatzハックを見逃していた、と。Fable、これをHOL-lightに翻訳してくれ。間違えるなよ。よくやってる!
信頼のレベルは劇的に上がっているのに、『人間の証明は信用できない』から『Leanの証明は信用できない』へと不信の矛先が移っていくのは、ある意味喜劇だ。HOL-lightに移せば信頼度はもう少し上がるかもしれないが、HOL-lightの実装にバグが一度もなかった、そのカーネルにバグがあり得ないと考えるのは思い上がりだ
マジか、これって長さと複雑さからして、形式化するのが最も難しい証明のひとつなんじゃないか?
その通り。Wilesの証明を本当に理解していると言える人間は、今この世界に25人から50人程度しかいないと言われている。そこにLLMが加わったわけだ。まったくもって衝撃的だ
フェルマーが余白に書いたという証明を特定してくれるまでは驚かないぞ(※/sは皮肉のサイン)
ふと思ったんだけど、AIは a, b, c の数値を生成したり探したりして aⁿ+bⁿ=cⁿ になるかチェックしたってこと?それって普通にコードで書けばいいんじゃないの?
a, b, c, nの全部の値をループで回せばいいってこと?
どうぞ、やってみて 😉
Leanもコードだよ。ただFLTは総当たりでは証明できない。対象になるのが『2より大きい自然数』という無限集合だから
それは起きないと思う。AIモデルは意図的に制限されている。こうした用途にツールを使える立場にある人間なんて、ほんの一握りしかいない
興味深いコメントだ。自分も形式手法に手を出し始めたところで、昨日Rocq(旧Coq)のチュートリアルをやってみた(本当に基礎的なものだけど)。Rocqでの証明は、紙とペンで書く証明に近い感覚があると感じた
この話題の背景と論点
ここで使われているLeanは数学的な証明を機械的に検証できる形式言語で、研究者コミュニティには「100の定理」という形式化の達成度を測るチェックリストがある。フェルマーの最終定理はその中でも最難関とされ、Imperial College Londonの研究チームなど複数のグループが手作業で形式化を進めていた。スレでは、Claudeが書いた1300万行のコードを人間が全て読むわけではなく、Lean自体が証明の正しさを検証する仕組みになっている点が繰り返し説明された一方、その検証系(カーネル)自体にバグがあり得るという指摘も出ており、「何を信用の根拠にするか」という論点は完全には決着していない。またAndrew Wilesが証明にかけた歳月や情熱を引き合いに、発見の体験がAIに置き換わることへの寂しさを語るコメントも多く、技術的な達成と心情的な受け止めの両方が交錯するスレになっている。
※本記事は5ch(Hacker News)スレッド「Formalizing Fermat’s Last Theorem」より抜粋・要約して構成しています。
この記事のリアクション
まだコメントはありません。