テレンス・タオ：不等式定理を証明するためにGPT-4を使いました。論文はarXivにアップロードされます。

有名な数学者テレンス・タオ氏はここ数か月、ChatGPTやGPT-4などのAIツールを使用して数学の問題を解くことに熱心に取り組んでいます。私たちもこれに細心の注意を払ってきましたが、今日は彼が数学の定理を証明するために GPT-4 を使用しているのを見ました。

一体どんな数学の定理なのだろうかと不思議に思わざるを得ません。

テレンス・タオ氏によると、彼は最近、有限個の実変数を含む不等式理論の例示的な結果を完成させ、まもなく arXiv で公開される予定だという。

そこで彼は、最終的に、Lean4 インタラクティブ証明システムについて学習し、それを使用するために必要な補助 AI ツール (GPT-4) を使用することを決意しました。彼はかなり単純な形式化を達成することを望んだ。

また、マクローリン型不等式に関する Terence Tao の論文も見つけましたが、それが同じものかどうかはわかりません。

論文アドレス: https://browse.arxiv.org/pdf/2310.05328.pdf

Tao 氏は、IPAM の機械支援証明ワークショップで Lean のデモンストレーションをいくつか見ており、そこで、Lean で定理を証明するために使用される基本的な構文と戦略に慣れるために、自然数ゲームをプレイするようアドバイスされました。

彼は、ペアノの公理から乗算の交換法則や結合法則などの基本的な算術的事実を確立するなど、証明が学部生のときに読んだ実解析の本の初期の章の証明と非常によく似ていたため、簡単にゲームを始めることができることに気付きました。それはまた、彼がインタラクティブな教科書である QED でコード化した論理ゲームを思い出させました。

約3時間後、タオは上級の掛け算に到達し、自由時間にそれを続けるつもりでした。

自然数ゲーム アドレス: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game

しかし、自然数ゲームで利用できるツールのセットが限られているため、Tao は GPT-4 がゲームを解くのに直接役立つとは考えておらず、GPT-4 が提供するソリューションにはゲームに組み込まれていない方法が含まれていることがよくあります。しかし、彼は GPT-4 が Lean にとって確かに役立ち、そこから質問に対する有用な答えを得ることができることを発見しました。

レベルが難しくなるにつれて、GPT-4 はより便利になるでしょう。たとえば、Z が X の明らかな結果であり、Y が、そうでなければ非常にイライラするであろうあらゆる種類の微妙な文法問題を解決するような場合には、「X と Y がわかっている場合、Z をどのように証明すればよいですか?」と尋ねます。 Tao は、Natural Numbers ゲームには、ドキュメントに実際に記載されていたよりも多くのライブラリが含まれているようだということを発見しました。

一部のネットユーザーは、テレンス・タオの試みはクールだと表現した。リーンはとても良いです。 SAT、SMT、sharp-SAT など、Lean を使用する実証済みの証明チェッカーを作成する作業が数多く行われています。

また、ある人がタオ氏にこう尋ねました。「LLM がすべての人間を超える証明を書く能力を身につけるのに、何年かかると思いますか?」

この疑問に答えるために、タオさんの大型モデル実験の旅はこれからも続くようだ。