テレンス・タオはコパイロットに夢中です。コパイロットは1ページの証明を完成させるのに役立ち、その後のプロセスを推測することさえできました。

GPT-4 を「推奨」した後、Copilot は Terence Tao 氏からも熱烈に推奨されました。

彼は、プログラミングをする際に、Copilot は次に何をするかを直接予測できると率直に語りました。

Copilot により研究がより便利になり、Terence Tao 氏も最新の研究結果を完成させるために Copilot を使用しました。

タオ氏は、この論文では、この部分に関連する内容は実際には1ページしか占めていないと述べた。

しかし、この 1 ページの証明を完成させるために、彼は新しく習得したプログラミング言語 Lean4 を使用して 200 行を超えるコードを書きました。

Tao 氏がコードを公開した GitHub ページによると、Copilot によりコード作成速度が半分以上向上します。

Tao 氏は、Lean4 を選択した理由は、長い表現に対して対象を絞った部分的な置き換えを行う「書き換え戦略」にあると述べました。

たとえば、複雑な関数 f(x) を定義した場合、f(114514) という式を入力するときは、コードを使用して x を 114514 に「書き換える」だけで済みます。

タオ氏は、この機能は数式を繰り返し入力する必要があるLaTeXよりもはるかに便利だと語った。

それで、今回、テレンス・タオの「1ページの証明」はどんな新しい結果をもたらしたのでしょうか?

1ページで新しい不等式を証明する

この論文では、マクローリンの不等式に関連する問題について議論します。

マクローリンの不等式は数学における古典的な不等式です。これは、「非負の実数の算術平均は幾何平均以上である」という法則に基づいて導かれ、次のように表すことができます。

y ₁ …y _{n を}非負の実数とし、k = 1…n に対して平均_Skを次のように定義します (分母は分子の項の数です)。

これは、根を持つ n 次多項式の正規化された係数として表示されます。

（この式を覚えておいてください。これを式1と呼びます）

この場合、マクローリン不等式は次のように表されます。

ここで、等式はすべての_yiが等しい場合にのみ成立します。

微積分学では、古典的なニュートン不等式も存在します。

1≤k<n の任意の値に対して、実変数 y1…y _nがすべて非負であれば、ニュートンの不等式はマクローリンの不等式を簡単に記述できます。

しかし、この制限を追加しないと、つまり負の項の存在を許可しないと、ニュートンの不等式を使用してマクローリンの不等式を表現することは不可能です。

したがって、ニュートンの不等式に負の項が存在する可能性があることに対応して、タオは新しい不等式の変形を提案しました。

r>0かつ1≤ℓ≤nの場合、式2または式3のいずれかが成立する必要があります。

これが、このページで Tao が証明したいことです。具体的な証明プロセスは次のとおりです。

複素変数zに関する多項式P(z)を構築してみましょう。

前の式 1 と三角不等式から、次の式が得られます。

したがって、下限を設定するだけで済みます。

P(z)の絶対値をとり、対数をとると次のようになります。

任意の実数tに対して、t↦log(e ^t +a)は凸であり、a>0なので、不等式が得られます。

a=r ² 、t=2log y _jのとき、次のことが言えます。

上記は Terence Tao が示した証明プロセスです。ただし、正規化された |S _n |=1 の場合、次の式が成り立ちます。

次のステップ: 改良版を作成する

今回言及した「1ページの証明」に加えて、タオの論文では、任意の1 ≤ k ≤ ℓ≤ nに対して、次の新しい定理も提案されています。

タオ氏はブログ投稿で、次の計画としてこの不等式の改良版を提案することを明らかにした。

タオ氏は、証明は「練習のように」簡単で、微積分を使って行うことができると述べた。

しかし、彼はまた、議論のこの部分では漸近記法を使用しているため、少し困難があるだろうとも述べました。

新たな結論がどうなるか、待って見てみましょう。

もう一つ

Terence Tao 氏は AI ツールの熱心なファンです。彼は Copilot、GPT-4、その他の補助ツールを推奨しています。

今回、彼は大規模モデルの開発に対する新たな期待も提示し、いつの日かモデルが直接不平等の変種を生成できるようになることを期待している。

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