既存の証明を面倒な方法や人間には分かりにくい形で再構成したり、よく考えられた手法を新しい方法で使ったりすることが、超人的なスピードで行われるようになるよ。それによって、AGIについて心配する前に、いろんな能力が解放されるんだ。数学者たちがAIツールを使って何を始めるのか、すごく楽しみだよ。ツールが数学者が求めるものに本当に追いつけるようになったら、ね。最初は非数学者には大きな直接的な利益はないかもしれないけど、抽象的で複雑な結果が直接的な応用を持たないとしても、ミレニアム問題が本物のフロンティアモデルのベンチマークとして解決されるのを見られるかもしれない。テレンス・タオみたいな人が、誰よりも上手にAIを使いこなして、一気にいくつかの問題を解決するかもしれないし。今年は何が起こるのか、ワクワクしてるよ。

これが私を何年もワクワクさせてきたアイデアなんだ。「科学的リファクタリング」って呼んでるんだけど、もし上に向かって推論して、いくつかの普遍的な定数を変えたらどうなるんだろう？ どこでもπの代わりにタオを使ったらどうなるんだろう？ こういう楽しい質問は、通常はものすごい知的努力が必要だけど、思考の機械化と自動化が進めば、実際に試してみることができるかもしれないね！

既存の証明を再構成する部分には賛成だよ。それがここでの価値だと思う。ただ、LLMが言うことを確認するのはまだかなり面倒かもしれないけど、少なくとも人間がこの作業の半分をやるのを待つよりはマシだよ。言語で表現できるすべてのトピックにおいて、LLMの価値は、出力を読む人間から異なる視点を引き出すために物事をシャッフルすることだと思う。これがAIを理解して実用化するための唯一の現実的な方法だよ。タオを尊敬してるけど、彼のAI使用についてのコメントは、リンクされた投稿を注意深く読まないと誤解を招くかもしれないと感じてる。

これがAGIじゃないなら、何がAGIなの？複雑な数学的定理を証明できるAIがあれば、すぐにAGIに繋がるのは避けられない気がする。

> 既存の証明を人間には面倒だったり隠れていたりする方法で再構成すること。素人からすると、それってあんまりAIっぽくないよね？数学はかなり論理的だから、効果的にこの領域を検索するアルゴリズムはすでに十数個あるはずだよね？

既存の証明を再構成することと、既存の方法を組み合わせること、そして「本当に新しい」数学との間には、実際の境界はないと思うよ。

今日、アリストテレスを自分で試してみてね！ https://aristotle.harmonic.fun/ 待機リストはもうないよ！

これは独立したHNスレッドに値するよね！これを提出して、hn@ycombinator.comにメールして、SCPに載せてもらうことはできる？（https://news.ycombinator.com/item?id=26998308）追記：あ、https://news.ycombinator.com/item?id=46296801を見て気づいたけど、あなたがCEOなんだね！それなら、あなたか、あなたの組織で最も適切だと思う人が、これを提出して、何なのか、どうやって試すのが一番簡単で楽しいかを説明するテキストを添えてもらえるといいな。

物理や数学のような複雑な分野に詳しい人に聞きたいんだけど、AIモデルと定期的に話してる？ 何か学べることがあると感じる？ プログラマーとして、問題を持ってAIに相談すると、いくつかの解決策を提案してくれるんだ。考えたことがあるものもあれば、そうでないものもある。君たちの分野でも同じような価値を得てる？

コンテキスト: 2025年に純粋数学の博士号を取得して、データサイエンティストに転職したんだ。今はMLや統計の研究もしてる。私にとって、深い研究ツールは、分野を移行する際に今持っている研究アイデアについての文献レビューを素早く追いつくために欠かせないものになってる。あまり詳しくないけど、比較的確立されたルーチンの数学（約5年前の標準的なランダム行列理論の結果など）にもかなり役立ってる。ユーティリティの幅は、期待されるものとかなり一致してる気がするよ：ルーチンプログラミング > 応用ML研究 > 統計/応用数学研究 > 純粋数学研究。約1年前には、私の数学研究分野にはまだ役に立たなかったけど、状況は急速に変わってきてる。

物理や数学の学位は持ってないけど、AIが助けてくれるのは、目の前の仕事に集中できるようにしてくれることなんだ。山のような教科書やウィキペディアのページ、科学論文を掘り返して、どこかで見たけど場所を記憶してない方程式を探す必要がなくなるから、毎日何日も節約できるよ。それでも、見つけたら参考文献を確認するけど、ソフトウェアが生成するものにはエラーが入り込むことがあるからね。大きなエラーもあるし（それは簡単に見つけられるけど）。だから、ここには価値があるし、かなりのものだけど、プロンプトの構造を考えるのにかなりの前思考が必要だし、出力に対しても超懐疑的で、細かくチェックできる能力が求められるよ。データをたくさん入力してクエリを作成し、その答えを批判的に使わないと、砂の上に城を築いていることに気づいたときには、痛い目に遭って時間を無駄にすることになるよ。

他の人が言ったように、Deep Researchは非常に貴重だよ。でも、仮説を生成するのは研究の最前線ではあまり良くない。ガードレールなしのChatGPT 4.0は、短い間に本当に素晴らしい仮説を生成してくれたけど、その後はこの方向では使えないほど抑制されちゃった。

深層学習モデルやカスタム・ノベルなアテンションレイヤー、アーキテクチャの研究をしてるんだけど、AI（ChatGPT）は、探してる論文のキーワードや用語がよくわからない時に、（意味的な）検索を手助けしてくれるからめっちゃ助かるよ。関連するアイデアや論文をつなげてくれるのもすごくいい。数学的な直感を探る時にも役立つことがあるね。例えば、ドロップアウトレイヤーが学習した重みや行列の性質にどう影響するかとか。時々、すごく難解な数学を見つけてくれて、それが直感を修正するのに役立つこともある。

俺は量子コンピューティングの仕事をしてるんだけど、量子コンピューティングに関する資料はたくさんあって、これらのLLMもそれに基づいて訓練されてるはず。いくつか試してみたけど、基本的なこと以外は全部ナンセンスを言い出すんだよね。でも、もしかしたら俺だけかも。テレンス・タオのトランスクリプトをいくつか読んだけど、彼がLLMに聞く質問は俺が聞くよりも複雑だよ。それでも、彼はよく合理的な答えを得てる。どうやったらこれらのツールをもっと上手く使えるのか、まだわからないんだ。

文献検索のスタートには確かにいいね。

彼ら（代数幾何学の数学研究）と話すけど、残念ながら文献検索以外ではあまり役に立たない。周りの人たちはもっと役立ててるから、バラつきがあるね。（私が試した中で最も強力なモデルはGemini 2.5 Deep ThinkとGemini 3.0 Proだけど）新しいGPTがどれだけ良くなってるかは分からないな。

参考までに、テレンス・タオは「AIがエルデシュ問題に貢献する」というウィキページを始めたんだ：https://github.com/teorth/erdosproblems/wiki/AI-contribution...（以前の投稿でも言及されてたね：https://mathstodon.xyz/@tao/115818402639190439） — 彼がこのページを始めてからまだ2週間も経ってないけど（12月31日）、現在の結果（問題[728]）はマイルストーンを示してる。ウィキページのセクション1で初めてのグリーンなんだ。

2026年は面白くなりそうだね。この技術は魔法じゃないし、進歩は常に徐々に進むもので、最初はあまり面白くない問題や「簡単な」問題の解決から始まるだろうけど、AIが未解決の数学の周りを少しずつ解決していくマイルストーンがもっと見られると思う。もちろん、それにはたくさんの人間の専門知識も必要だよね。この問題も「ある程度自律的にAIによって解決された（最初の試みからのフィードバック後）」だけだったし。人々はこのことについてゴールポストを動かし続けて、あまり感心しないとか、解決策は訓練データにあったに違いないとか言うだろうけど、今のところそれはテレンス・タオが何を言ってるかわからないと主張するのに近いから、かなり危険な立場だと思う。今の時点で、LLMがただの確率的なオウムで、訓練データをリミックスするだけで新しいことは決してできないって言ってる人と議論するのをやめるっていう遅れた新年の決意をしてる気がする。その議論はもう終わったと思う。LLMを面白い問題にどう適用するか（あるいは良いコードを書かせるか）については、解決すべき魅力的な問題がたくさんあるけど、それを始めるには、少なくとも彼らが新しいことをする能力があることを認めなきゃいけない。2023年には、ここまで来るなんて絶対無理だと思ってたけど（「チャットボットが新しい数学を推論できるわけがない！」）、3年後の今、ここにいる。次は何が来るんだろう？

うーん、これはまさに似たような証明の「リミックス」だね。おそらくそれらはトレーニングデータに含まれていたものだろうし。ただ、一部の人はその「リミックス」能力がどれだけ魅力的になり得るかを過小評価していると思う。特に、自分の証明での形式的な論理エラーを直接意識し、それが典型的なケースでどう対処されるかを考慮するとね。

ゴールポストはまだ同じだよ。AIが何かできるっていうのを、企業からの主張を聞くだけじゃなくて、独立して確認できるようにしたいんだ。企業はお金が欲しいがために、平気で嘘をつくからね。

2026年には数学のAIで驚くべき進展があると思う（AI全般でもそうかもしれないけど）。

ドキュメンタリーで、ある人が30桁のπを計算するのに人生を捧げたって話を見たことがある。俺のコンピュータが1秒もかからずにできることに、彼はどれだけの時間をかけたんだろう。コードを書くのに使ったアルゴリズムを使えば、1日か2日でできるし、ニュートン法を使えば10分で済むのに。

あなたが考えているのは、Veritasiumのエピソードかもね。https://youtu.be/gMlf1ELvRzc?si=Qwevl2GwHCzSFcsQ

タオの証明の経緯についての説明によると、人間が2つの別々のAIツールの間で結果を行き来させて、見つけたギャップを埋めるためにAIツールを使ってるってこと？それなら、自律的に行われたとは言えないんじゃないかな？超専門家の人間と50/50のパートナーシップに見えるから、俺の意見ではこれがもっと曖昧になると思う。俺のAIテストの結果とも一致するけど、彼らは結構バカだよ、OPUS 4.5とかでも、すでに専門家でないとボイラープレートをやるのは難しい。編集：タイトルが「解決済み」から「ほぼ解決済み」に修正されたのが見えるけど、まだ大きな誇張だと思う。

あなたの理解は正しいよ。これはアリストテレスとChatGPT、そして（非常に賢い）ユーザーとのやり取りだね。

LLM$の重要性を少し盛り上げるのは、良い経済的判断だと思うよ。

証明の隙間を見つけるのに、超専門家である必要があるの？それは議論の余地があるね。

私の印象では、タオやコミュニティはギャップを見つけてすらいないと思った。自動証明検証器を使っているって言ってたし、主なやり取りはエルデシュの論文を再読して、エルデシュが意図した正しい問題を見つけることに関わっていたから。だから、90/10くらいでLLMと人間の比率かな。もしかしたら私が読み間違えたかも。

この技術がどれだけ進化したかを見るのは本当にクールだね！これは整数に関する定理で、かなり基本的な証明があって、既存のMathlibインフラにしっかり支えられていることを覚えておいてほしい。AIは記号的な証明チェッカーに依存しているみたいで、チェックしている証明はこの結果においてあまり複雑な定義を使ってないみたい。私の経験では、既存のインフラから一歩離れた証明は、うまくいく可能性がすごく高いよ。改めて、これは本当にすごいね！！

フェルマーの最終定理のよりエレガントな証明が誰かから引き出せるか見てみたいな、ワイルズの証明と比べて。

ハーモニックで働いてるんだ、アリストテレスの会社ね。いくつか誤解を解いておくと： - アリストテレスは現代のAI技術を多く使っていて、言語モデルも含まれてる。 - アリストテレスは非公式な（英語の）証明に導かれることができる。もし証明が正しければ、アリストテレスはそれをLeanに翻訳するチャンスが高い（これはあなたの英語の証明がしっかりしてるっていう強い信頼の証だと思う）。ここでそうなったと思う。 - 一度証明がLeanに形式化されれば（正しく命題を形式化したと仮定して）、その証明が正しいことに疑いはない。これが私たちのアプローチの核心で、たくさんの（AI駆動の）検索ができて、答えを見つけたら、その解決策がどんなに複雑でも正しいって確信できるよ。質問があれば喜んで答えるよ！

まずはおめでとう！新しいLLMを使ってるとき、進歩なのかただのベンチマークハッキングなのか分からないことがあるけど、形式化された数学の結果はいつも進展が本物で大きいことを示してる。ハーモニックがほとんどの（難しい）人間が書いた数学を形式化するのはいつだと思う？クリスチャン・ゼゲディとのインタビューを見たけど（あなたの競争相手だと思う）、彼は今年だと信じてるみたい。

誰か、これらの技術をソフトウェアの形式的検証に応用することに取り組んでいる人いる？私の限られたRustの理解では、固定されたルールのセットを使ってメモリの安全性を保証してるみたい。ルールは理解しやすく実装しやすいけど、決定不可能性のせいでちょっと単純で制限的なんだよね。プログラマーは、自分のコードがメモリエラーを引き起こさないってわかってるのに、そのルールに従わない状況に直面することがある。もしアリストテレスみたいなものがコンパイラに統合されたら、すごくない？正しさの証明が書けるコードは、もっとルールを追加しなくても通ったりコンパイルされたりするんだ。

AIの翻訳がLeanに正しい形式化をしているかどうか、どうやって確認するの？他の分野では、生成AIが信じられそうな嘘を作るのが得意だから、この使い方でもそうなる可能性があるのか気になる。

アリストテレスの利点は、Claude Codeみたいな汎用コーディングアシスタントに対して何なの？

この技術を歴史的な数学文献に広く応用する予定はあるの？