AxiomProver はますます強力になっています。 そして@axiommathaiは成長し続けています。 Ken Ono 教授 @KenOno691 が Axiom の創立数学者および FTE #15 として参加したことを嬉しく思います。 彼は、私たちとともに AI 数学者を育成するために、バージニア大学の STEM 担当学長の終身在職権を持つアドバイザーの職を辞めました。 ケンの物語です。(1)
5年前、ケンは、名門の数論 REU プログラムの学部 1 年生だった私にチャンスを与えてくれました。 それは私の人生の中で最も大きな転機となった経験の一つでした。数学オリンピックの経験を持つ私にとって、数学研究とはどのようなものかを教えてくれた夏でした。(2)
私が出席できるだけの経済的余裕があることを確認するために、彼は私にスピリット・ラマヌジャン・フェローシップを授与しました。このフェローシップは、ケンが数十年かけて研究し、拡張してきた膨大な作品の持ち主である独学の天才にちなんで名付けられました。 その後、彼は私にラマヌジャンの理論からの未解決の予想を解決するよう指導してくれました。(3)
アメリカ数学会元会長でカリフォルニア大学バークレー校のケン・リベット教授は、ケン氏を「数学界の偉大な人物」と呼んでいる。 そうです。ケンは、分配関数の深い結果の証明からオリンピック水泳選手の指導、そしてラマヌジャンに関するハリウッド映画の制作まで、あらゆることを成し遂げてきました。(4)
なぜ移転したのか？ウォール・ストリート・ジャーナル（@WSJ）との独占インタビューで、ケンは私よりも的確にこう説明してくれた。 「私は、世界の実際の仕組みを変えることに貢献できるという贅沢な立場にあります。純粋数学者として、このような機会に恵まれたことは滅多にありません。」(5)
実際、Axiom を立ち上げたとき、私は数学的発見のための AI には、宇宙や脳の理解から現在をシミュレートして未来を設計する方法まで、あらゆるものを変革する力があると信じていました。(6)
ラマヌジャンはインドで一人で研究し、数学界が完全に理解するまでに数十年かかった定理をノートに書き綴った。 Axiom が構築している AI 数学者は、次のラマヌジャンに取って代わるものではありません。ラマヌジャンに力を与え、協力し、彼らの才能をかつてない規模で増幅させるのです。(7)
Axiom の 4 か月前にリリースされたシステムは、Lean において人間の介入なしにエルデシュ問題 124 と 481 を解決しました。 ラマヌジャンの直感の魔法のように、証明のコードがリアルタイムで画面上で展開されます。 科学者仲間の皆さんへ: 数学的発見の未来はここにあります。 ぜひご参加ください。（8）
今朝の@WSJから続きを読む: https://t.co/Fpk9hKBIby (9)