「ＡＩが数学の未解決問題を解いた」報告ラッシュ、リーマン予想もいずれ…　高まる思考力、疲れ知らずの働き者。人間に残された仕事は？ | NEWSjp

「２０２６年が明けてすぐに「人工知能が未解決の数学の定理を証明した」とする論文の公表が世界で相次いだ」「Ｌｅａｎの利用にはちょっとした難関がある。Ｌｅａｎ語ともいえる特殊な機械言語しか理解しない」

テストなどの応用例でちょくちょく見かけるleanの本領発揮だ。

leanの前から定理証明系は色々あったのにleanだけコレだけバズってるのなんでなんすかね。やっぱマーケティング？/未解決問題って別にいくらでも考えられるわけで、ヴェイユのいう「共鳴箱」を超える日が来るんだろうか

aiが解いたのを自分が解いたことにはしないのかな。

もう少しすると、絶望して早まった決断を自らに下す数学者が出そう。門外漢だけど、次の役割はAIと世の中の翻訳者になるかな(テキトー)

ここまでくるのが予想より早かった。2,3年前は東大二次試験もダメだったのに。　今、新井紀子著(2018年)「AI vs 教科書が読めない子供たち」を読んでいて、感慨深い。

ちょっとチャッピーに受験問題きいてもトンチンカンなんだけど……。　あいつがバカなのか、こっちがバカなのか…。　問題文がバカなのか……。はぁ………。AIを使いこなせてないぜ……………。

予想外にざっくりした回答だったwww「ｎと比べると圧倒的に小さい」

AIに丸投げして、AIが出力した文書で話を進める、というスタイルはどの仕事でも、最も効率的かつ有効になってきた。AIに性能限界はあるが、人間よりは遥かに上。人間リストラの季節だな。

おもしろい

野尻抱介が書いていた、エージェントが研究を進める話が現実になりつつあるなあ

dp212氏、それランダウ記号の小文字の方を通常言語に訳しただけ。物理系からすると本来の純粋数学でのランダウ記号の使い方見てると卒倒して後頭部地面直撃してしまう

未解決問題をAIが発案し、別のAIが解くループができないと意味がないのでは？

実は私もある野望のためにLeanを勉強中。間に合いますように！

これまで「AIが解いた」としている学者たちはほぼ、AIの思考過程をLeanで検証しながら間違いを回避している > 例の望月教授のABC予想証明もLean言語による検証プロジェクトが始まってますね。

これもなあ・・・ https://www.asahi.com/articles/ASV3V3VPBV3VDIFI00NM.html

じゃあ、疲れるところと働かないところが私の受け持ちかな？

土台の理論から手順を明確にして証明まで持って行く手伝いをLEANがしてるので「AIが」と限定するのは誤解を招く表現。今後はこう言うアルゴリズムを取り込んだハイブリッド型AIが伸びていくんだろうな。

ABC予想のゴタゴタについてもAIに整理してもらえないだろうか

この一週間、コードの設計やリファクタリングさせてるけど、感心する。理由も教えてくれるから、勉強なるし。20年前の知識でコード書いてること指摘され、本気で凹んだわw