フェルマーの最終定理の形式化の進捗状況
(xenaproject.wordpress.com)- FLT の証明を Lean に移植する作業は2か月目に入っており、Wiles の「R=T」定理に必要な R と T の定義はまだ完成していないが、抽象可換代数の結果の1つはすでに証明された
- 目標は 1990年代の元の証明をそのまま複製することではなく、Diamond/Fujiwara、Kisin、Taylor、Scholze らの後続研究によって一般化・単純化された証明を Lean と mathlib の上に構築すること
- 現代的な証明に必要なcrystalline cohomologyを形式化する過程で、divided power 構造の標準文献である Roby の 1965年論文にある重要補題が誤っているように見える問題が明らかになった
- Brian Conrad が Berthelot-Ogus 本の付録で代替証明を見つけ、Arthur Ogus もその付録の誤りを修正する方法を知っていると答えたことで、プロジェクトは再び進められるようになった
- この事例は、現代数学の詳細な証明が専門家の記憶や暗黙知に依存する危うさを示しており、形式システムに証明を記録すべき実務的理由を強めている
Lean に FLT の証明を移植する現在の状況
- フェルマーの最終定理（FLT）の証明をコンピュータに教える作業は2か月目に入っている
- Wiles 証明の中核である「R=T」定理では、R と T が何であるかを Lean 上で定義するのに多くの作業が必要で、まだ両方の定義とも完成していない
- PhD 学生の Andrew Yang は必要な抽象可換代数の結果をすでに証明している
- 「抽象的な環 R と T がいくつかの技術的条件を満たせば互いに等しい」という形の結果
- 現在の草稿は blueprint として公開されている
- 使用しているシステムは Lean と数学ライブラリ mathlib
- Lean と数論を少し知っている人は、contribution guidelines、project dashboard、issue を通じて参加できる
1990年代の証明をそのまま移植しない理由
- プロジェクトはWiles の 1990年代の証明をそのまま形式化するわけではない
- その後、Diamond/Fujiwara、Kisin、Taylor、Scholze らの研究によって証明はより一般化され、単純化されてきた
- 目標は FLT を証明するだけにとどまらず、より一般的で強力な結果まで Lean の中に構築すること
- AI 数学革命が本当に起こり、Lean が重要な構成要素になるなら、コンピュータが現代数論の中核定義を理解可能な形で備えることは役に立つかもしれない
crystalline cohomology に必要な divided powers
- 形式化しようとしている証明では、Wiles の元の証明にはなかったcrystalline cohomologyが使われている
- この理論は 1960〜70年代のパリで発展し、Grothendieck のアイデアをもとに Berthelot が基礎を築いた
- 古典的な指数関数や対数関数は微分幾何や de Rham cohomology を理解するうえで重要だが、characteristic p のような算術的状況ではそのままでは機能しない
- 1960年代の Roby の論文群で発展したdivided power structuresは、算術的状況で使える類似の関数を構成するうえで重要な役割を果たす
- Lean に crystalline cohomology を教えるには、まず divided powers を形式化しなければならない
Lean 作業の中で明らかになった Roby 文献の問題
- Antoine Chambert-Loir と Maria Ines de Frutos Fernandez は Lean 上でdivided powers理論を形式化していた
- 夏のあいだに Lean が標準文献の人間的な議論の問題をあぶり出し、確認の結果、Roby の仕事にある重要補題が誤っているように見えることが分かった
- 技術的には、Berthelot の論文は divided powers 理論を最初から展開せず、Roby の「Les algebres a puissances divisees」を利用している
- この論文は Bull Sci Math, 2ième série, 89, 1965, pp.75-91 に掲載された
- p.86 の Lemme 8 は偽であるように見え、証明をどう修正すべきかも明確ではなかった
- その証明は Roby の 1963年 Ann Sci ENS 論文にある別の補題を誤って引用していた
- 正しい命題は
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R)だが、適用の過程で tensor product が1つ抜け落ちていた
- この問題により、module の divided power algebra が divided powers を持つという Roby の証明が崩れ、その結果
A_cris環の定義が妨げられた
「理論が間違っている」というより「証明に穴がある」に近い状況
- これは crystalline cohomology 自体が実質的に間違っているという意味ではない
- 主要定理は依然として正しいように見えるが、Antoine と Maria Ines がたどっていた証明は不完全だった
- Roby、Grothendieck、Berthelot はすでに全員亡くなっており、元の専門家に直接たずねることはできなかった
- 複数の専門家は、中間補題が偽であっても主要結果の証明は修正可能だと見ている
- 形式化では「修正できそうだ」という判断だけでは不十分で、実際に修正された証明が必要になる
Berthelot-Ogus 付録が開いた迂回路
- Tadashi Tokieda がこの話を Stanford で Brian Conrad に伝え、Conrad は crystalline cohomology が間違っているという話の中身を尋ねた
- 技術的な詳細を聞いた Conrad は問題がありそうだと同意し、検討に入った
- 数時間後、Conrad は Berthelot-Ogus の crystalline cohomology 本の付録に、module の universal divided power algebra が divided powers を持つことの別証明があると知らせた
- Conrad の見立てではこのアプローチはうまくいきそうで、そのおかげで証明は再び進められるようになった
- その後 Berkeley で Arthur Ogus と昼食をとり、この付録が問題を解決したと伝えると、Ogus はその付録にもいくつか誤りはあるが修正方法は分かっていると答えた
現代数学文献が形式化を必要とする理由
- この過程は、人間が現代数学を文書化するやり方が十分に頑健ではない可能性を示している
- 多くの事実が「専門家なら知っていること」のままに残り、文献には正確に整理されていないことがある
- 重要なアイデア自体はこうした衝撃に耐えるほど頑健でも、実際の細部の証明は期待した場所に存在しないことがある
- 数学を形式システムにきちんと記録すれば、誤りの可能性を大きく減らせる
- 形式主義者ではない数学者にとっても、機械が人間の議論を学んで自ら数学をするようにするには、まず議論を機械に教える過程が必要になる
- Maria Ines は Cambridge Formalization of Mathematics seminar で divided powers の形式化について発表しており、当該の問題は整理されたものと理解されている
- プロジェクトは再び軌道に乗ったが、文献がまた足を引っ張る可能性は残っている
1件のコメント
Hacker Newsのコメント
大学院時代、指導教員の Birch–Swinnerton-Dyer予想 の計算的アプローチを手伝うために高速なコードを書いていたことを思い出した。
近隣都市の整数論セミナーで「予想を裏づける証拠を強めようとしているのか」と聞かれ、笑いながら「いいえ、むしろ反例を見つけたいのです」と答えたところ、専門家たちがひどく怒った。
整数論はあまりに古く深い分野なので、その分野で博士論文を書くことは初心者になるための第一歩に近く、記法や定義は分かっても、その下にある直観には届かなかった。
だから「反例を期待している」という言葉に専門家たちが示した怒りは、恐れよりも好奇心を残し、彼らがまだ言葉にできていないが見えているものが何なのか気になった。
こうした 形式化の進展 は、プログラミングにより親しんでいる人にとって数学をはるかに身近なものにしてくれる。
形式性が不足していることへの不安はもっともだが、不安への正しい反応は回避ではなく好奇心だと思う。
あなたのような青臭い新参者が荒っぽい計算で反例を見つけ、一夜にして有名になったら、その努力と築き上げた構造がすべて崩れかねないので腹を立てたのだろう。
昔の若い自分に数学の大学院について助言するなら、些末ではない「Xを証明せよ」という課題ごとに、時間の少なくとも1/4は 反例探し に使えと言いたい。
課題では99%失敗するだろうが、問題への洞察はずっと深まり、残り1%では天才のように見えるかもしれない。
実際の数学研究に入ると、その確率は反例優先アプローチにずっと有利な方向へ変わる。
学生時代、友人が、ある人物がセミナー初日を終え、皆がその人が フェルマーの最終定理 を証明するのだと興奮していたという話をしてくれたのを覚えている。
その人物は Andrew Wiles で、その後、出版前に見つかった問題を数か月かけて補い、ついに全体が出版された。
数学を学んでいた身としては途方もなく興奮する出来事で、だから「古風な1990年代の証明」という表現を見ると本当に年を取った気分になる。
クラスのほとんど全員が数学の大学院生で、資料の20%も理解できていなかったと思う。
Lean がときどきやる苛立たしいことをやった、というくだりが好きだ。標準文献にある人間的な議論の提示に文句をつけ、詳しく見ると実際に人間の議論には欠けている部分があった。
冗談交じりの苛立ちは別として、これはすごいことであり、Lean や他の定理証明器は今後の数学で重要な道具になると思う。
現代数学の文書化が不十分だという話は、UI/UX/ウェブデザイン に似ているように感じる。
デザイナーが非形式的で不正確なモックアップやプロトタイプ、インタラクションフローを作って開発者に渡すと、開発者はそれをコードとして形式化し、機械に正確に説明しなければならない。
その過程で、設計が考慮していなかったインタラクションのシナリオやコードパスのような穴を必然的に発見し、ときには大きな設計上の欠陥が露わになり、開発者またはデザイナーがそれを埋めなければならない。
設計と開発は別の役割であり、異なる考え方を要求し、たいていのデザイナーは開発者のように働き考えることに強い抵抗を示す。
その失敗以後、私たちは数学を完全に形式化することはできないと学んだのであり、これは AI で数学をやろうとするアプローチの根本的な問題を指し示している。
このテーマに関心があるなら、実際のコードを見るとよい。
例: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
コード全体の構造を説明する青写真も見る価値がある: https://imperialcollegelondon.github.io/FLT/blueprint/
部外者として見ている立場だが、Lean コード がどのようなものか、そして人々がどう貢献しているのかを見るのはとても興味深い。
単体テストが不要だという点も気に入っている。ある意味では、最終的な証明命題が単体テストなのだ。
たとえば、ある定義が空虚ではないことを確認するための些細な例や反例が、その役割を果たす。
純粋数学をやっていた立場からすると、大きな問題は数学者が自己完結した証明をほとんど提供しないことだと思う。
そうするインセンティブがなく、著者が「詳細は省略」と書くことを誇らしく思っている場合さえある。
結局、あらゆる論理の段階を追える厳密な証明を求めるなら、文献では簡単に見つからない穴を専門家が埋めなければならない。
そういう人がすべてを説明する本を書いてようやく可能になることもあり、ときにはそれでも十分ではない。
記録された内容だけを見れば、現代数学の多くは不安定な基盤の上にある。
数学の研究論文はその分野のほかの専門家に向けて書かれており、詳細があまりに少ない場合もあって、査読の際によく不満を言いたくなる。
だが本当にすべての詳細を示すと、論文はずっと長くなる。
高校数学の素養がしっかりしていれば解ける例として、ある実数 x > X について
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cxとなるような定数 C, X > 0 が存在することを証明する問題がある。この種の命題は解析的整数論では常に現れ、専門家には自明なので、論文ではほとんどいつも証明なしで書かれる。
完全で厳密な証明を作れば長くて退屈になり、専門家の誰も読みたがらないだろう。
こうした態度にはトレードオフのコストがあるが、管理可能な水準に見える。
Tao が言う第三段階の 情報を備えた直観 のことのように聞こえる。
「あることを100回やったなら、『容易にわかるように』と言って先へ進んでよい」と言っていた。
つまり、頭の中にデータベースを持つ人が、ある定理の前提条件と次の文の結論が合っているかを探し出す仕事をする、という意味だと理解した。
それとも現在の証明チェッカーが評価できる形で表現できない数学があるのだろうか。
あるいは、証明チェッカーの利用が思ったほど広まっていないのかもしれない。プログラミングにおける静的型付け言語の位置づけに似ているように聞こえる。
つまり、ごまかして済ませた部分のせいで、広く受け入れられていた証明に致命的な欠陥があった例があったのかを知りたい。
そうしたことがなかったのなら、細部を明示することに対して緩い態度が見られる理由も理解できる。
「crystalline cohomology は1970年代からあまりに多く使われてきたのだから、問題があるならもっと前に露見していたはずだ」という直観が本当に正しいのか、ずっと気になっていた。
欠陥のある証明の上に数学の一分野全体が発展し、その分野が単に偽だと判明するようなことは、本当にそんなにありえないのだろうか。
彼は基礎論文の「最初のページの最初の補題」にあるミスによって一つの分野が崩れるのを実際に見た。
UniMath に関する初期の作業と IAS の特別年、そして HoTT 本へと続く流れは、数学の形式化という話題を今日の位置にまで押し上げたと言える。
基礎が間違っているなら、その反例の一つが基盤となる定理そのものを反証するかもしれないので、誤った基礎の上に積み上げることは、むしろ基礎の欠陥を露呈させる可能性が高い。
同様に、数学がときどき応用されて予測を生むとき、数学が間違っていれば予測も間違い、その誤った予測は大きな注目を集める。
実のところ「分野」という言い方は少し誤解を招きやすく、多くの理論は数学全体の中のほかのさまざまな理論と結びついた結び目に近い。
それらの理論もまた別の理論とつながっている。
この結び目のほかの部分にまったく影響を及ぼさず、基盤だけが論理的に崩れるのだとしたら、かなり奇妙な状況だろう。
内部的には完全に整合していながら、ただ一つの誤りだけを含む巨大な宙に浮いた数学の塊というものは、この記事のコホモロジーの例では想像しにくい。
厳密には哲学的な態度に近いが、現在の数学の多くが、ある意味では自然に発見されたものだと信じたい。
ネタバレすると、それでも世界は回り続けた。
この1年ほど、学部の複素解析学の課程の一部をLeanで形式化しようと断続的に試みてきた。
学ぶことも多くやりがいもあったが、ときにはもどかしくもあった。
最近になってようやく、
C*から(-pi,pi] x Rへの全単射として 極形式 を完全に定義できたが、複素数、べき級数、exp、sinがmathlibにすでにあるにもかかわらず、それらを「最初から」定義しようとこだわっていたためでもある。困難のかなりの部分は、数学の学士号しかなくLean/mathlibに不慣れで、指導してくれる人もいなかったことから生じた可能性が高い。ただし、Zulipコミュニティは非常に助けになった。
mathlibの多くの結果はかなり抽象的に述べられているため、標準的な学部レベルの定理とどう結びつくのか、あるいはそうした定理がmathlibに存在するのかを把握しにくい。
研究数学コミュニティにとっては妥当なのだろうが、個人的には大きな障害であり、Leanが教育にもっと使われるなら同様の問題になるかもしれない。ただし、時間がたてば整理できる部分ではある。
証明の自動化は、まだ十分ではないと見ている。
あまりにも多くのことが、本来そうあるべきよりも証明しにくく、特に 型変換 がいちばん不満だ。
通常の数学では実数は複素数の部分集合なので、すべての複素数について成り立つことは自動的にすべての実数についても成り立つが、Leanではそれらは別の型であり、単射写像や型変換演算で行き来しなければならないため、証明の核心がぼやけてしまう。
自然数を実数に、さらに複素数に変えるといった型変換が積み重なると、特に煩雑になる。
もちろん、これはこの題材特有の問題かもしれず、代数学のように明示的な写像を扱う分野では、はるかに自然なのだろう。
mathlibの使い方、何が存在するのか、どこにあるのかについて案内してもらうのは本当に簡単だ。
何重にも積み重なった型変換の問題は、たいてい
norm_cast戦術で解決する。特定の質問でなくても、何気なく触れたり、コード内で不必要に複雑な証明スタイルが見えたりすると、自分の知らなかった戦術を提案してもらえることがある。
形式化が難しすぎるという感覚だけがあって、どんな手法を使えばよいかわからないなら、苦労して作った満足のいかない証明を1つ、切り離した例として取り出し、人にもっと短くできるか試してもらう形で質問できる。
こうした質問はたいてい歓迎され、みんなが多くを学ぶ。
このスレッドは、数学をうまく書く方法に関するもののように見える。
何十年にもわたって数学を読み、書き、教え、応用し、出版してきており、応用数学の博士号も持っている。
数学の文章に問題があるのは確かで、一部の数学はひどい書かれ方をしている。
しかし、かなりうまく書かれた数学もある。
少なくとも、すべての記号は使う前に定義すべきであり、数学を提示する前に動機を与えるのは助けになるし、ときには直感的な説明も有用だ。
うまく書かれた数学を注意深く読むことは、数学の文章作法 を学ぶ助けになる。
例として、Paul R. Halmosの Finite-Dimensional Vector Spaces、R. Creighton Buckの Advanced Calculus、Tom M. Apostolの Mathematical Analysis、H. L. Roydenの Real Analysis、Walter Rudinの Real and Complex Analysis、Leo Breimanの Probability、Jacques Neveuの Mathematical Foundations of the Calculus of Probability が挙げられる。
筆者は文献で展開されているそのままのやり方で フェルマーの最終定理 を検証しようとし、その過程で、ある下位分野を支えていた補助定理が使われていた形では真ではないことを発見した。
それでもその分野が概ね救済可能だと信じる理由は、本当に間違っているなら誰かがすでに否定的な結果を見つけていたはずだという信頼による。
そこで今度は、その分野を支える適切な代替物を見つけなければならなかった。
筆者はかなり面白く書く人で、半分ほどは理解できなかったのに読みやすかったので、不思議な体験だった。
証明が反駁されたり欠陥が見つかったりしたときに使うよい語として vitiated を知った。
結論そのものが偽だと証明されたという誤解をあまり招かずに、その証明は損なわれており、新しい証明や修復が必要だという意味を込められるのが気に入った。