「２０２６年が明けてすぐに「人工知能が未解決の数学の定理を証明した」とする論文の公表が世界で相次いだ」「Ｌｅａｎの利用にはちょっとした難関がある。Ｌｅａｎ語ともいえる特殊な機械言語しか理解しない」
テストなどの応用例でちょくちょく見かけるleanの本領発揮だ。
leanの前から定理証明系は色々あったのにleanだけコレだけバズってるのなんでなんすかね。やっぱマーケティング？/未解決問題って別にいくらでも考えられるわけで、ヴェイユのいう「共鳴箱」を超える日が来るんだろうか
aiが解いたのを自分が解いたことにはしないのかな。
ここまでくるのが予想より早かった。2,3年前は東大二次試験もダメだったのに。 今、新井紀子著(2018年)「AI vs 教科書が読めない子供たち」を読んでいて、感慨深い。
もう少しすると、絶望して早まった決断を自らに下す数学者が出そう。門外漢だけど、次の役割はAIと世の中の翻訳者になるかな(テキトー)
ちょっとチャッピーに受験問題きいてもトンチンカンなんだけど……。 あいつがバカなのか、こっちがバカなのか…。 問題文がバカなのか……。はぁ………。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
こうやって便利な世の中になっていくのに未だに貧富の差を解決できない
テレンス・タオさんのお写真までAIっぽく感じるのは何故なのか。私も一刻も早く現代AIに追いつくため計算ドリルをしなくてはならない／しかし自然言語が解決したのってほんとデカかったんだね
プログラミングと同じで、論理をこねくり回す数学はAIと相性良すぎなんだろうなーと思う
バイブ数学？
IUT理論が量産されるだけでは？少なくとも論文が量産されると査読者が足らなくなるが、それもLLMにやらせるの？
自律的にってどういう意味だ？この問題解こうって自ら決心したってことか？
ワシの人生の未解決問題も解いてくれ
数学の難問解いても世の中に還元されるの相当先なんだよなあ。そう言う意味ではイタズラに数学屋を失業させて終わるのでは。
なんでこういう記事読んでそのまま受け取っちゃうんだろう。「一般向けにかなり端折った説明なんだろうな」って思わないのかな。
現状は演算機能でゴリ押すだけなんじゃないかな。まあでもそれなら検証もしやすい。
宇宙際タイヒミュラー理論を用いたABC予想の証明をlean語で何億行のAI出力により記述しきれたら/しきれなかったら、かわんごは賞金を出すのだろうか
「特殊な機械言語」とかランダウ記号のこととか、全体的にちょっと用語の解説の仕方が雑な感じがしますね…
数学といった極度にルールに閉じた世界ならでは、理論側から使えるのかどうか
AIを使って問題解決できるスキルがこれからは求められるんだろうなぁ
そのうちAIが何を研究しているのか理解できなくなるんだろうな、それをシンギュラリティと呼んでいいかはわからんが
数学の難問の還元スピードもAIが加速させるやろ。
AIが解いて、人類にわかるようにまとめるまでが仕事だからな。
ギャップが見つかったら見つかったでそれを埋める証明を作ってくれそうな気もする
“これまで「ＡＩが解いた」としている学者たちはほぼ、ＡＩの思考過程をＬｅａｎで検証しながら間違いを回避している”
旧ZK tokyoがリブランドしたがLeanについて推してたな
ほえーよく分からんがすごいね
AIが正しい答えを導き出しているかどうかを確認する仕事が残るだろうな。
“数学の証明支援ソフト「Ｌｅａｎ（リーン）」だ。ブラジル人の科学者が作り上げ、多くの数学者も関わったというこのソフトは、ある命題（例：ＰならばＱである）に対する証明を書いて渡すと、それに誤りがないか”
人間にはもう楽しくないテストしかのこってないのは数学でも同じなのか。数学者にとって無から新しい定理が生えてくるのって楽しいの？
「ＡＩが数学の未解決問題を解いた」報告ラッシュ、リーマン予想もいずれ… 高まる思考力、疲れ知らずの働き者。人間に残された仕事は？ | NEWSjp
「２０２６年が明けてすぐに「人工知能が未解決の数学の定理を証明した」とする論文の公表が世界で相次いだ」「Ｌｅａｎの利用にはちょっとした難関がある。Ｌｅａｎ語ともいえる特殊な機械言語しか理解しない」
テストなどの応用例でちょくちょく見かけるleanの本領発揮だ。
leanの前から定理証明系は色々あったのにleanだけコレだけバズってるのなんでなんすかね。やっぱマーケティング？/未解決問題って別にいくらでも考えられるわけで、ヴェイユのいう「共鳴箱」を超える日が来るんだろうか
aiが解いたのを自分が解いたことにはしないのかな。
ここまでくるのが予想より早かった。2,3年前は東大二次試験もダメだったのに。 今、新井紀子著(2018年)「AI vs 教科書が読めない子供たち」を読んでいて、感慨深い。
もう少しすると、絶望して早まった決断を自らに下す数学者が出そう。門外漢だけど、次の役割はAIと世の中の翻訳者になるかな(テキトー)
ちょっとチャッピーに受験問題きいてもトンチンカンなんだけど……。 あいつがバカなのか、こっちがバカなのか…。 問題文がバカなのか……。はぁ………。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
こうやって便利な世の中になっていくのに未だに貧富の差を解決できない
テレンス・タオさんのお写真までAIっぽく感じるのは何故なのか。私も一刻も早く現代AIに追いつくため計算ドリルをしなくてはならない／しかし自然言語が解決したのってほんとデカかったんだね
プログラミングと同じで、論理をこねくり回す数学はAIと相性良すぎなんだろうなーと思う
バイブ数学？
IUT理論が量産されるだけでは？少なくとも論文が量産されると査読者が足らなくなるが、それもLLMにやらせるの？
自律的にってどういう意味だ？この問題解こうって自ら決心したってことか？
ワシの人生の未解決問題も解いてくれ
数学の難問解いても世の中に還元されるの相当先なんだよなあ。そう言う意味ではイタズラに数学屋を失業させて終わるのでは。
なんでこういう記事読んでそのまま受け取っちゃうんだろう。「一般向けにかなり端折った説明なんだろうな」って思わないのかな。
現状は演算機能でゴリ押すだけなんじゃないかな。まあでもそれなら検証もしやすい。
宇宙際タイヒミュラー理論を用いたABC予想の証明をlean語で何億行のAI出力により記述しきれたら/しきれなかったら、かわんごは賞金を出すのだろうか
「特殊な機械言語」とかランダウ記号のこととか、全体的にちょっと用語の解説の仕方が雑な感じがしますね…
数学といった極度にルールに閉じた世界ならでは、理論側から使えるのかどうか
AIを使って問題解決できるスキルがこれからは求められるんだろうなぁ
そのうちAIが何を研究しているのか理解できなくなるんだろうな、それをシンギュラリティと呼んでいいかはわからんが
数学の難問の還元スピードもAIが加速させるやろ。
AIが解いて、人類にわかるようにまとめるまでが仕事だからな。
ギャップが見つかったら見つかったでそれを埋める証明を作ってくれそうな気もする
“これまで「ＡＩが解いた」としている学者たちはほぼ、ＡＩの思考過程をＬｅａｎで検証しながら間違いを回避している”
旧ZK tokyoがリブランドしたがLeanについて推してたな
ほえーよく分からんがすごいね
AIが正しい答えを導き出しているかどうかを確認する仕事が残るだろうな。
“数学の証明支援ソフト「Ｌｅａｎ（リーン）」だ。ブラジル人の科学者が作り上げ、多くの数学者も関わったというこのソフトは、ある命題（例：ＰならばＱである）に対する証明を書いて渡すと、それに誤りがないか”
人間にはもう楽しくないテストしかのこってないのは数学でも同じなのか。数学者にとって無から新しい定理が生えてくるのって楽しいの？