証明の物語 · 1 / 6
余白
1637年——本の余白に書かれた一文が、数学史上もっとも長い待合室を始めた。
フェルマーはディオファントスを読みながら、ある問題の横にこう書き込む。立方数を二つの立方数に、四乗を二つの四乗に、そして一般に二乗より大きい累乗を、同じ累乗二つに分けることはできない——しかも、この余白にはとても書ききれないほど見事な証明を自分は持っている、と。
それは公表されなかった。三世紀半のあいだ、この書き込みは数学でもっとも有名な約束か、あるいはもっとも有名な冗談であり続け、どちらなのか誰にも分からなかった。
残ったのは一文ではなく方法だった:無限に続く一族を丸ごと排除するために、その一員が存在すると仮定し、最小のものを選び、さらに小さいものを導く。フェルマーはこれを四乗に使った。オイラーは立方数でこれが働く亀裂を見つけ、その代価として新しい数をひとつ受け入れた——1の立方根である。
現代の結末は橋だった。1995年に公表されたワイルズとテイラー–ワイルズの仕事による半安定曲線のモジュラー性と、FLTの反例から非モジュラーな曲線が生まれるというリベの定理が出会う。2001年の後続の定理は有理数上のすべての楕円曲線を扱う。半安定の場合の証明年とは区別しよう。
隠れている数学累乗と正の整数 · 四乗は二乗にたためる
章を読む →
証明の物語 · 2 / 6
降下の階段
存在しないことを証明するには、永遠に下り続ける階段を建てる——そして、その階段が始まれないことに気づく。
無限降下法は棚でいちばん礼儀正しい矛盾である。反例が存在すると仮定する。その全体から、最小のものを選ぶ——整列性がそれを許す。その一つから、さらに厳密に小さい別の反例を作る。それを永遠に繰り返す。自然数の階段には底がある。だから、降下は最初から始まり得なかった。
職人技は矛盾ではなく構成にある。フェルマーの四乗の段は、一つの図形の内側に新たな直角三角形を二つ見つける。オイラーの立方数の段は、三乗の和が因数分解できる新しい環を必要とする。どちらも、新しい証人が非ゼロだと示さねばならない——さもなければ階段は、一段だけ遅れて礼儀正しく止まってしまう。
証明支援系の中では、最小の証人は実在の対象で、順位も実在し、「厳密に小さい」は身振りではなく検査される。階段は、だれでも覗ける機械になる:すべての段、すべての不等式、すべての非ゼロの証人。
隠れている数学いちばん小さい解を選ぶ · 必ず終わる階段 · アイゼンシュタインの世界の三つの因子
章を読む →
証明の物語 · 3 / 6
怪しい小包
1985年——破れた等式が幾何学的な対象として梱包され、その対象は有罪に見えた。
ゲルハルト・フライの着想は、その単純さゆえにほとんど無礼だった:FLTの反例aᵖ + bᵖ = cᵖがあると仮定し、それを使って、あまりに奇妙で本当とは思えない算術を持つ楕円曲線を組み立てる。曲線は反例の指紋を引き継ぐ——導手、判別式、半安定性の来歴まで。
ジャン=ピエール・セールが手紙で正確な処方箋を送り、ケン・リベがそれを定理に変えた。小包は有罪だった:そのような反例から作られる曲線は、モジュラーになり得ない。フライの観察はまだ証明ではなかったが、全欄が埋まった事件簿だった——このサイトのfrey-packageページが原文で押さえているのは、まさにその欄である。
議論の向きが、これを奇妙で美しいものにしている:誰も等式に解がないことを直接証明しない。代わりに、解があれば「ある特定の曲線が存在する」証拠になる;そして幾何学が、その曲線を住まわせることを拒む。反例は、自分自身の書類によって溶かされる。
隠れている数学等式から曲線へ · 半安定性 · 導手とレベル下げ
章を読む →
証明の物語 · 4 / 6
ビスケット一枚のリハーサル
二種類の数学についての予想が、期限つきの計画になる——そして期限が、あと一歩のところで勝ちかけた。
モジュラー性定理は、有理数上の楕円曲線に形式の相方を与える。良い還元の素数pでは、対応する係数は aₚ = p + 1 − #E(𝔽ₚ)。点の数には無限遠点も含める。形式は適切な重さとレベルを持ち、一致は近似ではなく厳密だ。
ワイルズの戦略は、変形環Rとヘッケ代数Tを比べる。R = Tという記号は、比較写像による同型を表し、Leanの型が文字どおり等しいという意味ではない。この比較の確立は、1993年に見つかった穴をリチャード・テイラーと修復した仕事も含め、証明の中心だった。
あとは日付つきのドラマだ:7年の秘密の研究、1993年6月のケンブリッジでの3回講演、「ここで止めます」で終わる最終日、その秋に見つかった致命的な穴、テイラーとの1年の修理、そして1995年のAnnalsの2本の論文。二重奏は本物だった。ビスケットの予算は、最後まで足りなかった。
隠れている数学曲線のモジュラー性 · 変形環と普遍性 · R = T——二つの工房をつなぐ等式 · ヘッケ環
章を読む →
証明の物語 · 5 / 6
空っぽの部屋
終幕はわざと地味だ——証人が、定理がすでに「空」と認定した部屋へ歩いて入る。
レベル下げは静かな奇跡である。怪しい曲線から、重さ2・レベル2のモジュラー形式が得られる——きわめて小さな空間だ。同じ手続きが、その形式が非ゼロであることも証明する:お客は生きて到着する。この非ゼロの証人がすべてである;それがなければ、矛盾させる相手がいない。
そして部屋はすでに空だと分かっている:重さ2・レベル2のカスプ形式の空間は次元ゼロ。その中のどの形式もゼロに等しい——消える空間についての定理で、部分群の指数を数え、沈黙が記録済みの重さ6・レベル1の空間と比べて証明される。
二つの証明書を並べれば、事件は崩れる:f ≠ 0 と f = 0、同じf、同じ空間。無限も、極限も、ドラマもない——認定済みの空箱のとなりに、非ゼロの石がひとつ。記録上もっとも短い矛盾であり、そこへ至る道はもっとも長かった。
隠れている数学重さとレベル · カスプ形式 · 誰もいない部屋
章を読む →
証明の物語 · 6 / 6
フクロウと三つの名前
機械は拍手をしない。仮定を列挙する——その一覧が、この物語でもっとも謙虚な一文である。
最後の場面は、余白でも、講堂でも、歴史の法廷でもない。端末である:証明支援系がすべての行を読み、すべての推論を検算し、評判で何も受け取らない——ワイルズの評判さえも。
形式化がついに定理を読み込むとき、正直な問いは「それは真か」ではなく「何を仮定したか」である。答えは短い:propext、Classical.choice、Quot.sound。検査系の三つの土台であって、フェルマーについての追加の信じごとではない。この区別が、この営みの倫理そのものである。
フクロウは拍手をしない。Leanは証明項を、その主張と仮定に照らして検査する。ここで読むのは固定したソースのチェックポイント。このサイトはFLTの開発全体を再コンパイルしておらず、検査時間も測定していない。読者たちは同じ食卓で、まだ余白について語り合っている。
隠れている数学公理と証明の検査 · 同じ対象についての矛盾
章を読む →