証明の誤りは、結論まで届くのか

by

証明の途中に誤りが見つかったとき、何が間違いと確定するのだろうか。数学の証明は、前提から結論までを正しい推論で接続することで成立する。その途中に成り立たない等式や、適用条件を満たしていない補題が含まれていれば、その推論によって結論を導いたとは認められない。しかし、証明の失敗と結論の真偽は、異なる対象についての判断である。誤った推論によって導かれた結論にも、真であるものと偽であるものの両方があり得る。問題のある証明を退けるには推論上の欠陥を示せばよいが、その証明が目指した命題を否定するには、命題そのものが成立しない根拠が必要になる。

この違いは、証明がどのような役割を果たすかを考えると明確になる。ある命題が真であることを証明するには、認められた前提からその命題へ到達する正しい推論を示す。一つの証明に誤りが見つかれば、その証明は命題の成立を保証する根拠として使えなくなる。一方、命題の真偽は、特定の証明が成功したかどうかによって変化する性質ではない。同じ命題に別の正しい証明が存在すれば、最初の証明が誤っていたとしても、命題の成立を示す根拠は残る。別の証明が確認できない場合には、少なくとも問題のある証明によって命題が確立されたという判断を撤回する必要がある。その段階で確定するのは証明の不足であり、命題が偽であるという結論ではない。

複数の補題を組み合わせた証明では、誤りの影響をさらに細かく調べる必要がある。補題とは、別の定理を証明するために利用する中間的な命題である。補題に反例が見つかれば、その補題は主張された条件のままでは成立しない。続く定理がその補題を利用していれば、当該定理の証明も再検証の対象になる。ただし、補題を使わずに同じ結論を導く経路がある場合や、補題の適用条件を修正しても後続の推論が成立する場合には、証明を回復できる可能性がある。誤りが発見された箇所と、最終結論の間にどのような依存関係が存在するかによって、必要な修復範囲は変わる。

数万行、数千万行に及ぶ形式証明でも、この論理的な区別は変わらない。形式証明では、数学的な命題と推論を形式言語で記述し、証明検査器が定められた論理体系のもとで導出の成立を確認する。証明の規模が大きくなるほど、多数の中間命題が別の命題の前提として利用されるため、一つの誤りがどこまで影響するかを把握することが難しくなる。誤った補題を修正するだけでは、その補題を使った後続の推論が引き続き成立するとは限らない。補題の仮定を追加した場合には、その新しい仮定を後続の証明でも満たす必要がある。結論を変更せずに証明を修復するには、修正された条件から最終結論までの推論を改めて接続しなければならない。

1. 証明の途中に誤りがあったら、結論も間違いなのか

「偶数の平方は偶数である」という命題を考える。偶数とは、ある整数を 2 倍した形で表せる整数である。したがって、調べる偶数を \(n\)、任意の整数を \(k\) とすると、\(n=2k\) と表せる。この命題を証明するには、\(n\) が偶数であるという前提から、\(n^2\) も 2 の倍数として表せることを示せばよい。平方を計算すると、次の等式が得られる。

\[n^2=(2k)^2=4k^2=2(2k^2)\]

最初の等号は、偶数を \(2k\) と表した定義に基づく。次の等号では、積を平方する計算規則によって \((2k)^2=4k^2\) と変形している。最後の等号は \(4k^2\) から 2 をくくり出したものである。\(k\) が整数なら \(2k^2\) も整数なので、\(n^2\) は整数 \(2k^2\) の 2 倍になっている。これにより、任意の偶数の平方が偶数であることを証明できる。

ところが、証明の途中で \((2k)^2=2k^2\) と計算していた場合を考える。この等式は一般には成り立たない。\(k=2\) を代入すると、\(n=4\) であるから、左辺は \(4^2=16\)、右辺は \(2\times 2^2=8\) となる。同じ値になるはずの両辺が異なるため、等式が誤っていることが確認できる。\(k=0\) では偶然両辺が一致するが、任意の整数 \(k\) について成立する等式であることを示すには、すべての整数で一致しなければならない。一つの反例によって、この等式を一般的な計算規則として使用することは否定される。

誤った等式の右辺 \(2k^2\) も 2 の倍数なので、その計算を使った説明は、一見すると正しい結論へ到達しているように見える。しかし、\(n^2\) と \(2k^2\) が等しいという接続部分が成立していない以上、右辺が偶数であるという事実から左辺が偶数であるとは推論できない。ここでは、計算結果の性質自体が間違っているのではなく、その性質を元の平方へ移す根拠が失われている。誤った等式を含む推論が証明として成立しない理由は、この接続の欠落にある。

一方、最初に示した正しい計算では \(n^2=4k^2=2(2k^2)\) が成立する。誤った等式を使った証明を退けても、この別の計算によって元の命題は証明されている。反例が示したのは \((2k)^2=2k^2\) という等式の誤りであり、「偶数の平方は偶数である」という命題への反例ではない。両者を区別することで、同じ証明の中に現れる中間的な主張と最終的な主張を、それぞれ別の対象として評価できる。

この例では、確認する対象によって必要な根拠が異なる。誤った等式を見つけた段階で証明の一部が無効になったと判断できるが、命題そのものを偽と判断するには、偶数であるのに平方が奇数になる整数を示す必要がある。実際にはそのような整数は存在せず、正しい証明がすべての偶数に対して成立する。証明上の欠陥を発見する作業と、命題の真偽を判断する作業が異なることを、この単純な例から確認できる。

確認対象 直接確認できること それだけでは確定しないこと 追加で必要な確認
中間の等式への反例 \((2k)^2=2k^2\) が任意の整数 \(k\) について成立するという主張は偽である。 偶数の平方が偶数であるという最終命題の真偽は、この反例だけでは確定しない。 最終命題自体への反例、または別の正しい証明の有無を確認する。
誤った等式を利用した証明 左辺と右辺を等しいものとして扱った推論には欠陥があり、そのままでは証明が成立しない。 同じ命題を証明する別の推論が存在するかどうかは確定しない。 誤った等式への依存を取り除き、前提から結論まで正しい推論が接続するか確認する。
修正後の計算 \(n^2=4k^2=2(2k^2)\) が成立し、偶数の平方が 2 の倍数であることを示せる。 別の命題や、異なる仮定を持つ証明の正しさまでは保証しない。 証明したい命題の前提と結論が、修正後の推論に対応していることを確認する。

初等的な計算では、一つの等式を修正するだけで証明が回復する場合がある。しかし、複数の補題が連鎖する証明では、修正した箇所が後続の推論に与える影響も確認する必要がある。例えば、ある補題が特定の値への一致を保証していたのに、修正後は値の上限しか保証できなくなったとする。後続の証明がその一致を利用して場合分けを排除していたなら、上限だけでは同じ排除を正当化できない可能性がある。補題の修正自体が正しくても、後続の証明が修正後の補題から必要な結論を導けるかは別に検査しなければならない。

証明の誤りが最終結論に与える影響は、誤りの大きさや修正した行数だけでは判断できない。誤った等式が他の推論に使われていなければ影響は限定されるが、多数の補題がその等式に依存していれば、それぞれの使用箇所で推論の成立条件を確認する必要がある。さらに、別の証明経路が同じ結論を導いている場合には、一つの経路が無効になっても結論の証明は維持される。最終結論の成立を判断するには、誤った命題の特定に加えて、その命題に依存する推論と、依存せずに成立する証明を区別することが必要になる。

2. 反例が否定するのは、どの命題なのか

「すべての整数は偶数である」という命題を考える。この命題は、整数をどれでも一つ選べば、その整数が必ず偶数であると主張している。しかし、整数 3 は偶数ではないため、反例になる。一つでも条件を満たさない対象が存在すれば、「すべての整数」という範囲に対して述べられた命題は偽である。この判断に必要なのは、反例が主張の対象範囲に含まれていることと、主張された性質を満たさないことの確認である。

一方、整数 3 が反例になっても、「偶数が存在する」という命題は成立する。実際に整数 2 は偶数なので、少なくとも一つの偶数が存在することを示せる。「すべての整数が偶数である」という命題と、「偶数である整数が少なくとも一つ存在する」という命題では、要求される条件が異なる。前者を否定するには一つの反例があれば足りるが、後者を否定するには、どの整数も偶数ではないことを示す必要がある。同じ整数の性質について述べていても、「すべて」と「少なくとも一つ」の違いによって、反例が否定する命題の範囲は変わる。

条件付きの定理では、対象の範囲に加えて、定理を適用するための仮定を確認する必要がある。「条件 \(P\) が成立すれば、性質 \(A\) が成立する」という定理は、\(P\) を満たす対象について \(A\) を保証する。ここで \(P\) は定理を適用するための条件、\(A\) はその条件から導かれる結論である。ある対象について \(P\) が成立することを確認できれば、定理を利用して \(A\) を導ける。しかし、\(P\) の成立が確認されていない場合には、その定理を根拠として \(A\) を導くことは正当化されない。

具体的には、「4 の倍数である整数は偶数である」という定理が該当する。整数が 4 の倍数なら、ある整数 \(k\) を使って \(n=4k=2(2k)\) と表せるため、必ず偶数になる。この定理を整数 6 に適用しようとしても、6 は 4 の倍数ではないため、適用条件を満たしていない。しかし、6 自体は偶数である。反対に、整数 5 も 4 の倍数ではないが、こちらは奇数である。4 の倍数という条件を満たさない対象については、偶数になる場合も奇数になる場合もある。条件が成立しないことだけから、結論の真偽を決定することはできない。

この例は、定理の適用条件が欠けている場合と、定理そのものに反例が存在する場合の違いも示している。「4 の倍数なら偶数である」という定理を否定するには、4 の倍数でありながら偶数ではない整数を示す必要がある。整数 5 や 6 は 4 の倍数という条件を満たしていないため、この定理への反例にはならない。定理の仮定を満たしていない対象から結論を導こうとすることは適用上の誤りだが、それによって定理自体が偽になるわけではない。

数学の証明で補題を利用する場合にも、同じ確認が必要になる。補題が特定の条件を満たす対象について成立するなら、その補題を使用する側は、対象が必要な条件を満たしていることを証明しなければならない。仮定の一つが確認されていなければ、補題の結論を後続の推論へ引き渡す根拠が不足する。さらに、補題に反例が見つかって仮定を追加する必要が生じた場合には、その補題を利用していたすべての箇所で、新しい仮定を満たせるかを確認する必要がある。補題自体を修正できても、修正後の適用条件が後続の証明で成立するとは限らないためである。

発見された誤りの種類によって、直接確定する内容と、追加で検証すべき内容は異なる。

発見された問題 直接確定すること 追加の検証が必要なこと
全称命題への反例 反例が対象範囲に含まれ、主張された性質を満たさないため、提示された範囲の全称命題は偽である。 対象範囲や条件を変更した命題、または別の結論が成立するかを確認する。
補題の適用条件の欠落 必要な仮定の成立が確認されておらず、その補題を利用した推論の正当化が不足している。 欠けた仮定を証明できるか、別の補題によって同じ結論を導けるかを確認する。
証明途中の計算の誤り 誤った等式や変形を利用した推論が成立せず、その計算に依存する証明経路に欠陥がある。 計算を訂正したうえで、後続の推論が修正後の結果から同じ結論へ到達できるかを確認する。
最終命題そのものへの反例 反例が最終命題の条件を満たしている場合、その命題は主張された範囲で偽である。 対象範囲や仮定を変更した別の命題が成立するかを確認する。

表の上三つでは、問題が発見された時点でも、元の最終結論が真である可能性は残る。全称命題への反例が中間的な補題を否定しても、その補題を使わない別の証明経路が成立する場合がある。適用条件の欠落についても、必要な条件を別途証明できれば、元の補題をそのまま利用できる。計算の誤りなら、正しい計算へ置き換えた後も必要な結論が得られるかを確認する。一方、最終命題そのものに反例が存在する場合は、元の命題を主張された条件のまま維持することはできない。途中の推論に対する反例と、最終命題への反例では、修復の対象が異なる。

反例が見つかった際に、補題の仮定を追加したり、対象範囲を狭めたりすれば、修正後の命題が成立する場合もある。しかし、修正によって成立する命題は、元の命題と同じとは限らない。例えば、「すべての整数は偶数である」という偽の命題を「すべての 4 の倍数は偶数である」へ変更すれば正しい命題になるが、主張する対象の範囲は大きく異なる。元の証明がすべての整数について結論を必要としていたなら、4 の倍数に限定した命題だけでは、その証明を回復できない。修正後の命題が正しいことと、修正後の命題で元の証明に必要な役割を果たせることは、それぞれ確認する必要がある。

反例の影響範囲を判断する基準は、反例が否定した命題の内容、その命題に課されていた仮定、後続の推論がその命題のどの部分を利用していたかという三つの関係にある。補題の結論を弱めても後続の推論が成立する場合には、限定的な修正で証明を回復できる。一方、後続の推論が失われた条件や結論を必要としていれば、別の補題や証明経路が必要になる。誤りの発見から最終結論の成立状態を判断するには、反例によって否定された範囲を確定し、その範囲に依存する推論を個別に検証することが必要である。

3. 誤った前提は証明のどこまで影響するのか

数学の証明では、一つの定理を導くために複数の補題を利用することがある。例えば、定理 C を証明するために補題 B を使い、B の証明では補題 A を使ったとする。このとき、A、B、C の間には、A の成立を根拠として B を導き、B の成立を根拠として C を導くという依存関係がある。A に反例が見つかれば、A を前提とした B の証明は、そのままでは B の成立を保証できなくなる。さらに、B の有効な証明を確認できなければ、B を利用した C の証明についても、結論までの推論が成立しているかを再確認する必要がある。

この影響は、A が偽になったことで B や C まで偽になるという意味ではない。A から B を導く推論が論理的に正しくても、前提である A が成立していなければ、その推論によって B が真であることを確立できない。同様に、B の成立が確認できない状態では、B を根拠として C を導く証明も確立したとは言えない。後続の命題の真偽と、後続の命題を支える証明の有効性は、ここでも区別される。誤りの影響が連鎖する直接の理由は、先行する命題の成立を後続の推論が必要としているためである。

ただし、C に到達する証明経路が一つとは限らない。補題 A と B を経由する証明とは別に、補題 D から C を導く正しい証明が存在するとする。D の証明が A や B に依存しておらず、D から C への推論も成立していれば、A に反例が見つかっても、D を経由する C の証明は維持できる。反対に、D の証明にも A が使用されていたなら、見かけ上は別の経路でも同じ問題を抱えることになる。代替証明の有効性は、異なる補題を使用しているという外形だけでなく、問題になった前提への依存が残っているかによって判断される。

証明の依存関係は、ある文献が別の文献を引用しているという関係とも区別する必要がある。同じ論文に含まれる二つの定理でも、一方が他方を使用していなければ、片方の証明の誤りがもう片方の証明へ直接影響するとは限らない。一方、異なる論文で発表された定理であっても、後の定理が先の定理を前提としていれば、その依存関係を確認する必要がある。影響範囲を決めるのは文献の数や配置ではなく、実際の推論においてどの命題がどの条件で利用されているかという関係である。

既稿「フェルマーの最終定理の形式化で、AI が生成した証明を Lean がどう検証したか」では、多数の形式化された命題を接続し、最終定理まで証明経路を成立させる工程を扱った[1]。形式証明では、定理を使用するときに必要な仮定が明示され、それらを満たす証明が要求される。ある補題の成立条件を変更した場合、その補題を利用する証明でも変更後の条件を満たす必要がある。依存関係を誤りの発見という方向から調べることで、どの証明が無効になった前提を使用しているか、どの箇所で新しい根拠が必要になるかを特定できる。

特に影響が大きくなるのは、中間命題の結論を弱める修正である。例えば、ある補題が二つの数 \(x\) と \(y\) について \(x=y\) を保証していたとする。後続の証明では、別の条件 \(x\leq z\) と組み合わせることで、\(y\leq z\) を導いていた。この推論は、\(x\) と \(y\) が等しいため、\(x\) に関する上限をそのまま \(y\) に適用できることによって成立している。

ところが、元の等式に反例が見つかり、補題を \(x\leq y\) へ修正する必要が生じたとする。修正後の不等式と \(x\leq z\) がどちらも成立していても、\(y\leq z\) は保証されない。例えば、\(x=1\)、\(y=3\)、\(z=2\) なら、\(1\leq3\) と \(1\leq2\) は成立するが、\(3\leq2\) は成立しない。元の等式では二つの値を相互に置き換えられたのに対し、不等式では大小関係の一方向しか保証されない。この違いによって、後続の証明が必要としていた結論を導けなくなる。

ここでは、補題を修正した後の \(x\leq y\) が正しいとしても、後続の証明が求める \(y\leq z\) まで確立されたことにはならない。後続の証明を回復するには、例えば \(y\leq z\) を別の条件から直接導くか、元の等式に相当する関係が必要な場面でだけ成立することを証明する必要がある。補題の修正に成功した段階と、その補題に依存する最終定理までの証明が回復した段階には、明確な違いがある。

誤りの発見後に必要となる検証は、依存関係と修正内容によって次のように分かれる。

状況 証明への直接的な影響 必要な検証 最終結論への帰結
補題 A に反例が見つかった場合 A を前提として B を導いた証明は、そのままでは B の成立を保証できない。 B を別の前提から証明できるか、A の条件を修正して同じ推論を成立させられるかを確認する。 B の有効な証明が回復されるまでは、その B を利用した C の証明も確立したとは言えない。
別の補題 D から C を証明できる場合 A を経由する証明が失敗しても、D を経由する証明は別途成立する可能性がある。 D の証明と D から C への推論が有効であり、無効になった前提に依存していないことを確認する。 代替証明が成立すれば、A を経由する証明を修復できなくても C の証明を維持できる。
補題の結論を弱めた場合 修正後の補題が正しくても、後続の証明が必要とする性質を保証できなくなる場合がある。 後続の推論が修正後の結論だけで成立するか、不足する性質を別の根拠から導けるかを確認する。 必要な性質を回復できれば証明を維持できるが、回復できなければその証明経路は未確立となる。
誤った補題を使用していない証明がある場合 当該補題を利用していない証明経路には、その誤りによる直接的な影響は生じない。 別経路の前提と推論が有効であり、間接的にも問題のある補題へ依存していないことを確認する。 独立した証明経路が成立していれば、最終結論を導く根拠は残る。

この区別は、形式証明の規模が大きい場合にも適用される。多数の補題が存在していても、誤った補題を実際に利用している証明と、別の前提によって成立している証明を区別できれば、再検証が必要な範囲を特定できる。ただし、ある補題から直接参照されている定理だけを確認すれば十分とは限らない。その定理をさらに利用する後続の証明にも影響が及ぶため、依存関係を最終結論までたどる必要がある。

さらに、修正によって補題の仮定が追加された場合も、結論を弱めた場合と同様に後続の証明へ影響する。例えば、従来は任意の対象について成立するとされていた補題が、特定の条件を満たす対象についてだけ成立することになれば、補題を利用する各箇所でその条件を証明しなければならない。追加条件を満たせる箇所では従来の推論を維持できるが、満たせない箇所では別の補題や場合分けが必要になる。修正した命題の正しさだけでなく、修正後の条件を使用先へ適用できることが、証明全体の回復を左右する。

証明の誤りが最終結論まで影響するかは、無効になった命題の数や修正した行数では決まらない。一つの補題に多数の証明が依存していれば、修正が一行であっても広い範囲の再検証が必要になる。反対に、多くの計算を修正しても、それらが最終結論への有効な証明経路に含まれていなければ、結論の成立には直接影響しない。修復の完了を判断する基準は、問題のある前提を取り除いた後も、必要な仮定から最終結論まで正しい推論が成立していることである。

4. 別の証明で同じ結論を維持できる条件

証明の途中で使用していた補題が成立しないと判明した場合、最終結論を維持するには、その補題に依存していた推論を修復する必要がある。修復には、元の推論に不足していた条件を証明する方法と、問題のある補題を使わずに別の推論経路を構築する方法がある。いずれの場合も、修正された中間命題が正しいという確認だけでは完了しない。最初に与えられた前提から元の結論まで、必要な条件をすべて満たす推論が成立していることを確認する必要がある。

条件を追加する修正には、証明できる命題の範囲が変わるという問題がある。例えば、すべての対象について性質 \(A\) が成立すると主張していた命題に、条件 \(P\) を満たす場合に限るという制約を追加したとする。修正後の命題が正しくても、それによって保証されるのは \(P\) を満たす対象についての \(A\) の成立だけである。元の命題は対象全体について \(A\) を保証する必要があるため、条件を追加した段階では元の結論まで証明したことにならない。

この違いは、整数の倍数関係を使うと具体的に確認できる。「6 の倍数は偶数である」という命題を証明しようとして、途中で「12 の倍数は偶数である」という補題だけを得た場合を考える。12 の倍数は確かに偶数である。しかし、6 は 6 の倍数でありながら 12 の倍数ではないため、この補題だけでは元の命題が要求するすべての対象を扱えない。元の命題を証明するには、6 の倍数を \(n=6k=2(3k)\) と表し、任意の整数 \(k\) について偶数になることを示すなど、対象範囲全体を覆う推論が必要になる。

条件を追加した補題から元の結論を回復できるのは、追加条件が必要なすべての対象について成立することを別途示せる場合である。例えば、元の証明が対象に条件 \(Q\) を要求し、修正後の補題が条件 \(P\) のもとでだけ成立するなら、\(Q\) を満たすすべての対象が \(P\) も満たすことを証明できれば、その補題を利用できる。反対に、\(Q\) を満たすが \(P\) を満たさない対象が存在する場合、その対象については別の推論が必要になる。追加した仮定が正しいかどうかだけでなく、元の証明が対象とする範囲でその仮定を満たせるかが、修復の成否を決める。

別の補題へ置き換える場合も、結論と適用条件の対応を確認する必要がある。元の補題が性質 \(A\) を保証していたとして、新しい補題が性質 \(B\) を保証する場合、\(B\) から \(A\) を導けることが必要になる。例えば、ある値が 0 に等しいという結論を必要とする証明で、新しい補題がその値は 0 以上であるとしか保証しなければ、必要な結論には到達していない。値が 0 以下でもあることを別途証明できれば、二つの不等式を組み合わせて 0 との等式を導ける。補題の置換によって失われた性質を、どの推論で回復するかまで確認して初めて、後続の証明を維持できる。

代替証明では、依存関係の循環にも注意が必要になる。定理 C を証明するために補題 D を使い、その D の証明で C を前提としていた場合、C の成立を根拠に C を導く構造になってしまう。D が別の名前で定義され、C とは異なるファイルや文献に記載されていても、証明上の依存関係が循環していることに変わりはない。C を仮定すれば D が成立し、D を仮定すれば C が成立するという相互の条件付き主張だけでは、C が実際に成立することを証明したことにはならない。循環を解消するには、C の成立を前提とせずに必要な補題を導くか、別の独立した根拠から C を直接証明する必要がある。

既稿「AI の『正しい』を決める検証契約」では、検証条件を満たしたという事実と、そこから保証できる範囲を区別した[2]。数学の形式証明でも、検査されるのは明示された公理と仮定のもとで形式化された命題が導出できるかという関係である。追加仮定を含む命題の証明が検査を通過した場合、その追加仮定の成立が自動的に確定するわけではない。元の定理を無条件に証明する必要があるなら、追加仮定を導く証明も必要になる。検査に成功した命題の内容と、実際に必要としている最終結論が一致しているかを確認することが、形式証明においても欠かせない。

証明の修復方法ごとに、維持できる内容と追加で確認すべき条件を整理すると、次のようになる。

修復方法 修正によって成立すること 元の結論を維持する条件 条件を満たせない場合の帰結
不足した仮定を証明する 補題が成立するために必要な条件を、使用する対象について確認できる。 元の証明で補題を使用するすべての箇所について、追加された仮定を導ける必要がある。 仮定を満たせない箇所では補題を適用できず、別の推論が必要になる。
補題の結論を修正する 修正後の条件のもとで正しい中間命題を得られる。 修正後の結論から、後続の証明が必要とする性質を導ける必要がある。 必要な性質を導けなければ、元の証明経路は回復しない。
別の補題へ置き換える 問題のある補題を使用せず、別の根拠から中間的な結論を導ける。 新しい補題の仮定が成立し、その結論から元の最終結論まで推論できる必要がある。 新しい補題が必要な性質を保証しなければ、追加の証明または別経路が必要になる。
証明経路を再構成する 元の推論とは異なる補題や定理を組み合わせ、結論への経路を構築できる。 各補題の前提が成立し、最終結論や未証明の命題への循環依存が存在しないことを確認する必要がある。 循環依存や未証明の前提が残れば、代替証明としては未確立となる。
最終命題の適用範囲を制限する 追加条件を満たす対象について、修正後の命題を証明できる場合がある。 元の最終命題を維持するには、元の対象範囲全体について追加条件を証明するか、別の根拠を示す必要がある。 元の対象範囲を保証できなければ、成立するのは適用範囲を制限した別の命題である。

これらの方法は、一つだけを選択して適用するとは限らない。例えば、誤った補題の仮定を修正した結果、一部の対象には修正後の補題を適用できるが、残りの対象には適用できない場合がある。このとき、適用できる対象には元の推論を利用し、それ以外の対象には別の補題を使うという場合分けによって証明を再構成できる可能性がある。ただし、場合分けした対象が元の定理の対象範囲をすべて覆っていることと、それぞれの場合で必要な結論が成立することを確認しなければならない。一つでも扱われていない場合が残れば、最終定理の証明は完成していない。

また、代替証明が存在するという主張と、その代替証明が実際に成立することも区別する必要がある。別の文献に同じ結論が記載されていても、その証明が問題のある補題を再利用している可能性がある。異なる論文や異なる形式化ファイルに分かれているというだけでは、独立した証明経路であることを保証できない。代替証明に含まれる前提をたどり、問題になった命題への依存が残っていないことを確認する必要がある。証明の独立性は、資料の配置や補題の名称ではなく、推論上の依存関係によって決まる。

最終結論を維持できるかどうかは、修正された補題が正しいかという局所的な判断と、その補題を使って元の定理まで到達できるかという全体的な判断の両方によって決まる。追加した仮定を証明できても、その仮定が元の対象範囲を覆っていなければ、結論の適用範囲は変わる。別の補題が成立しても、必要な性質を導けなければ証明は回復しない。さらに、新しい経路が元の結論を前提としていれば、循環依存によって証明の根拠が失われる。修復が完了したと判断できるのは、元の前提から最終結論までの各推論が正当化され、問題のある命題への未解消の依存が残っていない場合である。

5. 巨大な数学的証明で実際に起きたこと

5.1 有限単純群の分類定理と既存証明の構造

有限単純群の分類定理（Classification of Finite Simple Groups、CFSG）は、有限群を構成する基本的な因子となる単純群を分類する定理である。群とは、一定の演算規則に従って元を組み合わせることができる数学的構造であり、図形の対称性や物体の回転などを記述する際にも利用される。有限群は元の個数が有限である群を指す。単純群は、自明なものを除いて正規部分群を持たない群であり、より大きな群の構造を調べる際の基本的な構成要素になる。正規部分群とは、群の元による共役という操作で保たれる部分群であり、群を商群へ分解する際に必要となる構造である。

有限群は、正規部分群を使って段階的に分解することで、単純群を組成因子として取り出せる。ジョルダン・ヘルダーの定理によれば、この分解で現れる単純群の種類と重複度は、分解の順序が異なっても一致する。そのため、どのような有限単純群が存在するかを確定することは、有限群全体の構造を理解するための基礎になる。ただし、組成因子が同じでも元の群が同型になるとは限らず、分類定理が有限群の構造をすべて決定するわけではない。

CFSG の結論は、すべての有限単純群が、素数位数の巡回群、5 以上の次数を持つ交代群、リー型の有限単純群、26 個の散在型単純群のいずれかに属するというものである。素数位数の巡回群は、素数個の元を持つ繰り返しの演算から構成される。交代群は偶置換と呼ばれる並べ替えの操作から成り、リー型の有限単純群は有限体上の代数的構造から構成される。散在型単純群は、これらの一般的な系列に含まれない例外的な群である。分類を完成させるには、各系列に属する群の性質を確認するだけでなく、その一覧に含まれない有限単純群が存在しないことを証明しなければならない。

この最後の条件が、分類定理の証明を困難にしている。既知の群をいくつ列挙しても、未知の単純群が別に存在する可能性は残る。すべての有限単純群が指定された分類に含まれると示すには、任意の有限単純群を対象として、その内部構造に応じた場合分けを行い、各場合が既知の群のいずれかに帰着することを証明する必要がある。個々の群の構成や単純性を示す結果と、分類一覧がすべての可能性を尽くすという結果は、異なる役割を持つ。

Ronald Solomon の分類史は、この成果が長期間にわたり多数の数学者の研究を組み合わせて成立した過程を整理している[3]。Michael Aschbacher も、分類定理の成立状況と、膨大な文献に分散した証明を理解し直す困難を説明している[4]。証明全体は、一つの論文に記載された連続的な計算ではなく、異なる研究者が示した補題、構造定理、群の認識定理などを組み合わせて構成されている。ある論文が証明した結果を別の論文が前提として利用し、その結果がさらに後続の分類に使用されるため、各定理の成立条件が一致していることが必要になる。

1983 年には CFSG の完成が発表されたものの、準薄群と呼ばれる一群に関する大きな未完部分が残っていた。準薄群とは、分類証明に現れる特定の局所構造によって特徴づけられる群であり、その場合を処理するためには独立した大規模な議論が必要だった。Aschbacher と Stephen D. Smith は、2004 年に刊行した研究によって、この未完部分を補った[5]。それまでの証明で扱いきれていなかった場合を解決することで、第一世代と呼ばれる分類証明の主要な欠落が埋められた。

さらに、Gorenstein、Lyons、Solomon らによる分類体系には、既存の記述や推論を修正する訂正資料が公開されている[6]。証明が完成したとされる時点と、各部分の記述について訂正や補足が不要になる時点は一致しない。長大な証明では、最終結論を支える中間定理の一つに問題が見つかった場合、その定理を利用していた箇所まで確認する必要がある。訂正によって中間定理の仮定や結論が変われば、後続の推論が必要とする性質を引き続き保証できるかも再検証の対象になる。

CFSG の証明が多数の文献に分散しているという事実は、単に文章量が多いこととは異なる困難を生む。ある補題が成立する条件を別の論文が暗黙に利用していた場合、両者を接続する際に条件の不足が生じる可能性がある。さらに、その補題が修正されたときには、依存先の論文で使用されている推論を追跡しなければならない。巨大な証明の正当性は、各補題が個別に正しいことに加え、それらを使用する条件が最終結論まで整合していることによって成立する。

5.2 数値の等式に見つかった反例

2026 年 10 月 26 日、Axiom Math は、CFSG の形式証明を Lean で構築したと発表した。Lean は数学的な定義、命題、証明を形式言語で記述し、定められた論理体系のもとで推論の成立を機械的に検査するための仕組みである。Axiom Math は、既存の文献にある数学的な議論を形式化する過程で、誤植、表の誤り、仮定の欠落などを発見し、そのうち注目すべき相違は 34 件に及んだと報告している[7]。この件数は発表元が整理した相違の数であり、34 件すべてが独立した数学的定理の誤りを意味するわけではない。

既存の証明を形式化する際には、人間の読者が文脈から補っていた仮定も明示しなければならない。例えば、ある補題が特定の条件のもとで成立するなら、その補題を使用する側で条件の成立を示す必要がある。形式化できない箇所が見つかった場合には、元の数学的主張が誤っている可能性に加えて、記述の省略や、形式化を行う側の解釈が間違っている可能性もある。そのため、形式化の失敗だけで既存文献の誤りを確定することはできず、具体的な反例や欠落した推論を調べる必要がある。

数学的な修正が必要になった事例の一つは、Aschbacher と Smith の準薄群に関する研究で見つかった。ある補題では、二つの数値が等しいと主張されていた。しかし、\(\mathrm{SL}_2(5)\) という群を用いた具体例では、一方の値が 1、もう一方の値が 2 となり、主張された等式が成立しなかった。\(\mathrm{SL}_2(5)\) は、5 個の元を持つ有限体上で定義される、行列式が 1 の 2 行 2 列の行列からなる群である。反例に用いられた群が具体的に定まっているため、主張された等式がその群について成立するかを検査できる[7]。

二つの数値が 1 と 2 になるという結果は、元の等式に対する直接の反例である。補題が両者の一致を一般的に保証していたなら、一つの具体例で値が異なることによって、その補題の主張は否定される。Axiom Math の報告では、等式を不等式へ置き換えることで補題の内容を修正できた。しかし、等式と不等式では後続の証明へ引き渡せる情報が異なる。等式では二つの値を相互に置き換えられるのに対し、不等式では指定された方向の大小関係だけが保証される。

この違いは、後続の証明に影響した。元の議論には、二つの数値が等しいことを利用して特定の場合を排除していた箇所があった。補題を不等式へ修正すると、以前は等式によって排除できた場合が残る可能性が生じる。つまり、補題の訂正によって中間命題自体を正しくできても、その補題を根拠に行われた場合分けの正当性は自動的には回復しない。

Axiom Math は、影響を受けた部分について、先行する議論で扱う場合を広げ、後続の議論を適用する対象を改めて区切ることで、必要な結論へ到達したと報告している[7]。元の証明が排除していた場合を別の段階で処理し、残りの対象に対して後続の定理を適用するという修復である。この方法では、修正後の各場合を正しく扱えることに加え、場合分けが元の証明で対象としていた範囲をすべて覆っていることが必要になる。

この事例で発見された誤りは、中間的な数値の等式にあった。しかし、その修復は等式を一箇所書き換えるだけでは完了せず、等式を利用していた場合分けの再構成に及んだ。反例が直接否定した命題と、その命題に依存していた推論の範囲が異なっていたためである。最終結論までの証明を回復できたかどうかは、訂正後の補題から必要な場合を処理し、残されたすべての条件について結論を導けるかによって判断される。

5.3 Walter の証明経路に対する反例

より大きな証明経路の再構成が必要になった事例は、不均衡群定理（Unbalanced Group Theorem、UGT）に関するものである。この定理は、有限単純群の内部に現れる特定の部分群の構造を利用し、群全体がどの分類に属するかを絞り込むための結果である。その議論では、対合と呼ばれる元と、その元に関する中心化群が重要な役割を果たす。対合とは、単位元とは異なり、2 乗すると単位元になる元である。中心化群とは、ある元との演算の順序を入れ替えても結果が変わらない元を集めた部分群である。

有限単純群の分類では、未知の単純群が存在すると仮定し、その中で位数が最小のものを調べる方法が使われる。この場合、より小さい単純群については既に分類できているという前提を利用できる。元の群に含まれる部分群や、その部分群から得られる単純群の情報を調べることで、元の群が既知のどの分類に属するかを判断する。その際、対合の中心化群に特定の奇数位数の構造が現れる場合を処理するために、UGT が使用される。局所的な部分群の情報から群全体の分類へ進むための接続を担っている。

Axiom Math が公開したプレプリントは、UGT の既存の証明経路に使われていた閉包性の主張に反例があることと、その問題を回避する代替証明を提示している[8]。閉包性とは、ある集合に含まれる対象へ指定された操作を行っても、結果が同じ集合に含まれるという性質である。例えば、整数の集合は加法について閉じている。二つの整数を足しても結果は整数になるためである。群論で扱う閉包性はこれより複雑だが、指定された操作の前後で対象が同じ分類の中に残ることを保証するという役割は共通している。

John Walter の 1986 年の研究では、特定の群の族に属する群から、関連する単純群を取り出す操作を考えていた。その議論には、操作後に得られる単純群も元の族に属するという推論が含まれていた[9]。この推論が成立すれば、操作後の群に対しても、元の族を対象として証明済みの結果を適用できる。反対に、操作後の群が族の外へ出る場合には、適用対象を限定していた前提が失われる。既存の定理自体が正しくても、その定理を利用するための条件が成立しなくなるのである。

反例として示されたのは、\(\mathrm{PSL}_2(49)\) という有限単純群である。\(\mathrm{PSL}_2(q)\) は、\(q\) 個の元を持つ有限体上の行列から構成される群に由来する記号であり、括弧内の数は元の群の要素数を示しているわけではない。ここで用いる有限体は 49 個の元を持ち、7 個の元を持つ有限体の拡大として構成できる。この関係から、元の有限体の構造を保つ位数 2 の自己同型が生じる。自己同型とは、群の演算を保存しながら、その群の元を別の元へ対応させる変換である。

\(\mathrm{PSL}_2(49)\) は Walter の議論で指定された群の族に含まれる。しかし、この群に体の自己同型から生じる対合を作用させると、その対合によって固定される元からなる中心化群は \(\mathrm{PGL}_2(7)\) と同型になる。さらに、そこに現れる関連する単純群は \(\mathrm{PSL}_2(7)\) である。ところが、7 は \(2^3-1\) と表せるメルセンヌ素数であり、\(\mathrm{PSL}_2(7)\) は問題の群の族から明示的に除外されている。元の群が指定された族に属していても、操作後の関連する単純群はその族に属さないという具体例が成立する[8]。

この反例では、二種類の対合を混同しないことも必要になる。UGT の条件で問題になる対合は、対象とする群の内部に存在する元である。一方、\(\mathrm{PSL}_2(49)\) の反例で用いられる対合は、有限体の構造に由来する自己同型であり、元の単純群の内部の元ではない。この区別を省くと、UGT の仮定そのものへの反例が見つかったかのように解釈される可能性がある。実際に否定されたのは、Walter の証明で使用された、関連する単純群が指定の族に残るという閉包性の主張である。

反例の影響は、Walter の議論において閉包性を必要としていた推論へ及ぶ。操作後の群が元の族に属することを前提に、既存の分類結果を適用していたなら、その適用は正当化されなくなる。しかし、反例によって \(\mathrm{PSL}_2(49)\) が有限単純群であることや、UGT の最終結論が偽であることまで示されたわけではない。Axiom Math は、問題の反例が UGT の結論だけでなく、Walter の Proposition II.5.9(ii) の結論そのものも否定するものではないと説明している[7]。

ここでは、命題が成立するかという判断と、特定の推論経路によって命題を証明できるかという判断が分かれる。Walter の証明経路では、操作後の群が同じ族に属するという条件を使えなくなったため、別の根拠が必要になった。UGT の結論を維持するには、その条件を必要としない推論を示すか、問題となった場合について別途正しい議論を構築しなければならない。反例の発見によって確定したのは、既存経路の一部がそのままでは成立しないという事実である。

5.4 代替証明が成立した理由

UGT には Walter の経路とは異なる証明も存在していた。Axiom Math が採用した修復では、Ronald Solomon が 1976 年に示した極大 2-成分に関する理論が基礎になっている[10]。2-成分とは、対合の中心化群などに現れる局所的な群構造を調べるために用いられる、特定の部分群である。極大 2-成分の理論は、こうした部分群の包含関係や相互作用に制約を与える。UGT の証明では、異なる対合に対応して現れる部分群を比較し、その比較によって関連する単純群の情報がどのように保たれるかが問題になる。

既存の経路では、ある操作を行っても関連する単純群が指定された族に残るという性質を利用していた。しかし、\(\mathrm{PSL}_2(49)\) の反例によって、その閉包性を一般的な前提として使用できないことが判明した。代替経路では、群の族全体について同じ閉包性を要求する代わりに、分類証明の該当箇所で必要となる仮定のもとで、比較対象となる部分群が持つ単純群の情報を保存できることを示す。必要な結論を導く条件を特定し、その条件に対応する別の数学的結果を構築する方法である。

公開プレプリントの Theorem 2.3「Preservation of simple tops」は、この比較に関する保存性を示す新しい群論上の結果として提示されている[8]。ここで保存されるのは、関連する部分群から取り出される単純群の構造に関する情報である。分類証明では、局所的な部分群から得た情報を別の局所構造へ移す際、その情報が同じ単純群を指していることを保証する必要がある。異なる部分群の間で対応が成立しているだけでは、そこから得られる単純群の種類まで一致するとは限らないためである。

Theorem 2.3 は、必要な仮定のもとでこの保存性を証明する役割を持つ。したがって、従来の閉包性の主張を無条件に復活させる結果ではなく、別の条件と推論によって必要な情報を確保するための補題である。この違いによって、反例のある閉包性を再び仮定することなく、分類に必要な単純群の情報を引き継ぐことが可能になる。新しい補題が正しいだけでなく、その仮定が分類証明の該当箇所で満たされることが、代替証明の成立条件になる。

代替証明には、この保存性を示す結果に加えて、既存の群論上の結果も利用されている。Gilman と Solomon による研究は、UGT の証明を特定の群を認識する問題へ縮約する役割を持つ[11]。群の認識定理とは、ある群が満たす構造的な条件から、その群がどの既知の群に対応するかを確定するための定理である。Foote による認識定理と Harris の関連研究は、縮約後に現れる場合を処理するための数学的根拠として利用される[12][13]。

これらの結果を組み合わせる際には、各定理が要求する仮定の対応を確認する必要がある。ある定理によって部分群の構造を制限できても、その結果が別の認識定理の仮定を満たすとは限らない。必要な情報を保存する Theorem 2.3 が成立しても、その情報から最終的な分類上の結論へ進むためには、Gilman と Solomon の縮約や、Foote と Harris の認識結果を適用できることを示さなければならない。Axiom Math は、これらの関係を接続することで、CFSG の分類に必要な単純群についての UGT の結論へ到達したと報告している[7]。

この修復では、Walter の証明経路に含まれた閉包性の問題を、そのまま正しい主張として扱う必要がなくなった。代わりに、Solomon の理論を基礎とした保存性の証明と、既存の縮約・認識定理を利用して必要な場合を処理している。反例が否定した推論を取り除き、別の前提から同じ結論へ到達する経路を構成したことが、修復の中心である。新しい経路に必要な数学的前提が増える場合には、それらも証明上の依存関係として解決する必要があるため、単に別の文献の定理を引用するだけでは修復が完了しない。

さらに、プレプリントの Remark 9.5 には、Theorem 2.3 を経由せずに必要な結論へ到達する、より短い導出も記載されている[8]。Axiom Math の説明によれば、この短い経路は形式化作業の完了後に数学者が見いだしたものであり、第一世代の証明で使用されてきた方法の範囲で構成されている。プレプリントには、AI によって構築・形式化された保存定理を含む経路と、その保存定理を使用しない短い経路の両方が残されている。前者には Theorem 2.3 という追加の数学的成果があり、後者は必要な結論への依存関係を短縮する役割を持つ。

二つの経路が同じ結論へ到達するということは、最終結論を導くための中間命題が一意ではないことを示している。保存定理を利用する経路では、比較対象となる部分群の情報を保存する性質を証明し、その結果を既存の認識定理へ接続する。一方、短い経路では、その保存定理を必要とせず、別の組み合わせによって結論を導く。それぞれの証明が異なる前提を利用していても、必要な仮定が満たされ、最終結論までの推論が成立していれば、同じ命題を証明できる。

今回の修復で問題になった対象と、その解決に必要だった条件を整理すると、次のようになる。

対象 発見された問題・必要な性質 修復に用いられた方法 最終結論との関係
Aschbacher と Smith の補題 二つの数値が等しいという主張に反例があり、後続の証明ではその等式を利用して場合を排除していた。 等式を不等式へ修正し、先行する議論と後続の議論が扱う場合の範囲を再構成した。 誤った等式に依存せず、必要な場合をすべて処理することで分類証明の該当部分を回復した。
Walter の閉包性の主張 \(\mathrm{PSL}_2(49)\) に関する操作から、指定された族に属さない \(\mathrm{PSL}_2(7)\) が現れた。 閉包性を前提とする推論に代えて、別の群論上の結果から必要な結論を導く経路を構築した。 反例が否定したのは既存経路の中間的な主張であり、UGT 自体の結論ではなかった。
Theorem 2.3 異なる部分群の比較において、関連する単純群の情報が保存されることを示す必要があった。 分類証明で必要な仮定のもとで保存性を証明し、既存の縮約・認識定理へ接続した。 問題のある閉包性を使用せずに、分類に必要な UGT の結論へ到達する経路を構成した。
Remark 9.5 保存定理を経由する証明とは別に、必要な結論へ到達する経路が存在した。 第一世代の証明で使用される方法から、Theorem 2.3 を使用しない短い導出を示した。 同じ結論に対して、異なる中間命題を使用する証明経路が成立することを示した。

Aschbacher と Smith の補題では、中間命題の訂正に伴って後続の議論の適用範囲を修正した。一方、Walter の証明経路では、問題のある閉包性を利用する推論を別の数学的結果へ置き換えた。両者は修復方法が異なるが、元の結論を導くために必要な条件を改めて確立したという点で共通する。誤った中間命題を訂正することと、その訂正を含む証明が最終結論まで成立することは、別々に確認する必要があった。

UGT の事例が示しているのは、一つの証明経路が破綻した場合でも、別の正しい推論によって同じ結論を維持できるという具体的な可能性である。ここで UGT の結論が維持された根拠は、反例の影響が限定的だったという判断だけではなく、Solomon の理論と既存の認識定理を組み合わせた代替証明が提示されたことにある。さらに Theorem 2.3 を使用しない経路も示されたことで、結論へ到達する方法が一つに限定されないことが明確になった。証明の誤りが最終結論まで及ぶかどうかは、失われた推論の範囲と、残された正しい証明経路の成立条件によって判断される。

6. 形式証明は何を保証し、何を保証しないのか

証明の誤りを修復したとき、最終的に確認すべきことは、修正後の前提から結論まで正しい推論が成立しているかという点である。人間が書いた数学的証明では、論文に記された仮定や補題を読み取り、各推論の正当性を確認する必要がある。形式証明では、命題と推論を形式言語で記述し、証明検査器によって論理的な接続を確認できる。ただし、形式化された命題が本来の数学的主張と一致していること、証明が指定された公理の範囲で成立していること、公開された成果を第三者が再現できることは、それぞれ確認する対象が異なる。

Axiom Math は、有限単純群の分類定理（CFSG）の形式化成果と、その証明を構成する依存関係を公開している[14]。公開された GitHub リポジトリの README によれば、形式化には Lean 4.35.0-rc3 を使用し、既存の数学ライブラリーである Mathlib と、有限単純群の分類に関する形式化を進めてきた TauCeti を基礎としている。README は、未証明の部分を一時的に残すための sorry を使用せず、標準的な公理だけに依存する証明であると説明している。また、プロジェクト全体を構築する手順として lake build を示している[15]。

Lean における sorry は、まだ証明できていない命題を一時的に受け入れて開発を進めるための仕組みである。これを残したままでも、周囲の定義や証明の記述を構築できる場合がある。しかし、その状態では未証明の命題を根拠として利用していることになる。sorry を残さないという条件は、未証明の穴をその仕組みで埋めていないことを意味する。ただし、形式証明の保証範囲を判断するには、sorry の有無に加えて、証明が依存する公理や定義を確認する必要がある。任意の命題を新たな公理として導入すれば、その公理を前提にした証明を構築できるため、使用した公理の範囲が証明の意味を左右する。

公開された最終定理 CFSGComparator.classification は、TauCeti.ClassificationStatement という命題を証明対象としている[16]。この命題は、任意の有限単純群について、分類一覧に登録された群のいずれかと同型になることを主張する。同型とは、二つの群の元を一対一に対応させ、その対応によって群の演算構造が保存されることである。元の表現や構成方法が異なっていても、群として同じ構造を持つことを意味する。したがって、分類一覧に記載された群と同型であることを示せれば、元の有限単純群をその分類に位置づけられる。

TauCeti 側の定義では、分類対象となる群を CFSGIndex という索引によって指定している。索引は、素数位数の巡回群、交代群、リー型の群、散在型群に対応する具体的な群を選択する。TauCeti.ClassificationStatement は、任意の有限単純群に対して、この索引のいずれかを選べば対応する群との同型が存在するという内容である[17]。この定義によって、分類一覧の完全性が具体的な論理命題として表現される。分類一覧にどの群を含めるかという定義と、すべての有限単純群がその一覧に含まれることを証明する作業は、ここでも区別されている。

最終定理の Lean コードでは、既に形式化された有限単純群の分類結果を利用し、TauCeti.ClassificationStatement の証明を構成している。つまり、最終定理そのものに数千万行の推論が直接記述されているわけではなく、多数の補題や定理を依存関係に沿って利用し、その結果を分類命題へ接続する構造になっている。最終定理の証明を検査するには、そこで参照される定理が証明済みであることに加え、それらの定理がさらに依存する命題についても、必要な前提が正当化されていることが求められる。形式証明の規模が大きくなっても、各推論が有効な根拠に依存しているという条件は変わらない。

プロジェクトの形式化管理情報である formalization.yaml には、sorry_count が 0 と記載され、使用公理として propext、Classical.choice、Quot.sound が指定されている[18]。propext は論理的に同値な命題を等しいものとして扱うための公理、Classical.choice は古典論理で選択を扱うための公理、Quot.sound は商構造において同値関係から等しさを導くための公理である。これらは Lean の標準的な論理体系で使用されるものであり、CFSG の分類結果そのものを仮定する公理とは役割が異なる。使用公理を明示することで、最終定理がどの論理的前提のもとで成立すると主張されているかを確認できる。

一方、同じ管理情報ではレビュー状態が self-assessed と記載されている。これは、公開された形式化の状態について、開発元が自己評価していることを意味する。README に証明の完成が記載され、最終定理のソースコードが公開されていることは確認できるが、それだけで第三者による独立した全体の再検証が完了したとは判断できない。独立再検証には、指定された Lean のバージョンと依存ライブラリーを用意し、公開された成果物を再構築したうえで、最終定理までの検査結果と実際の依存公理を確認する作業が必要になる。

ここで、Lean のカーネルが何を検査しているかを区別する必要がある。Lean では、命題を型として表現し、その命題の証明を対応する型の項として表現する。証明が与えられると、カーネルはその項が指定された命題の型を持つことを検査する。型の検査が成功すれば、定められた論理体系と使用公理のもとで、その形式命題を導く証明が成立していることを確認できる。Lean の公式仕様は、こうした型と証明項の関係、およびカーネルによる検査の仕組みを定めている[19]。

ただし、形式言語で記述された命題が、人間の意図した数学的主張を正確に表しているかという判断は、証明項の型検査とは別の作業になる。例えば、すべての有限単純群を分類するつもりで、形式化の対象を特定の種類の有限単純群に限定していたとする。その限定された命題に対する証明が正しくても、元の数学的主張が要求するすべての有限単純群について証明したことにはならない。カーネルは与えられた命題に対する証明を検査するため、定義の対象範囲が研究者の意図と一致しているかは、定義そのものを数学的に検討して確認する必要がある。

CFSG の形式化では、この対応関係が具体的な確認対象になる。TauCeti.ClassificationStatement は、任意の有限単純群が索引付きの群のいずれかと同型になることを表している。そのため、形式化された分類の数学的な意味を評価するには、索引に含まれる群が本来の分類一覧と対応しているか、それぞれの群が意図した数学的構造として定義されているか、最終定理が必要な対象範囲を覆っているかを確認する必要がある。形式証明の受理は、定義された命題を証明したことの検査結果であり、その定義が元の数学的分類と一致していることは、別途確認すべき対応関係である。

さらに、数学的な代替証明の成立と、形式化された証明全体の再現も区別される。UGT の代替証明について、数学的に必要な仮定から結論を導く議論が提示されていても、その議論が形式化された最終定理のどの依存関係に組み込まれているかは、公開された証明構成から確認する必要がある。逆に、形式証明の全体が検査を通過したとしても、それだけで新しい補題の数学的な重要性や、従来の証明と比較した理解の容易さまで決まるわけではない。証明の成立、形式化された命題の意味、研究成果の評価は、それぞれ異なる根拠によって判断される。

これらの確認対象を整理すると、次のようになる。

確認対象 確認によって確定する範囲 別途必要な判断
数学的な代替証明 提示された仮定から結論まで、数学的に正当な推論が成立していることを確認できる。 各仮定が実際の適用対象で満たされるか、元の最終結論が要求する範囲を覆っているかを確認する。
Lean の形式証明 形式化された命題について、指定された定義と公理のもとで証明項がカーネルに受理されることを確認できる。 使用公理の範囲と、形式化された定義や命題が意図した数学的主張に対応しているかを確認する。
独立した再検証 第三者が指定された環境と依存関係を用いて成果物を再構築し、証明の検査結果を再現できることを確認できる。 形式化された数学的主張の妥当性や、証明方法の新規性、数学的な理解への貢献は別途評価する。

三つの確認は相互に関係しているが、代替できるものではない。数学的な代替証明が正しいことを確認できても、公開された Lean プロジェクトが独立環境で正常に構築できるとは限らない。Lean のカーネルが証明を受理しても、形式化された命題が数学的な意図と一致しているかは定義の確認を要する。また、第三者がビルドを再現できた場合でも、その事実だけで証明の新規性や数学的な説明としての価値が確定するわけではない。何を確認した結果なのかを明示することで、それぞれの検証結果が保証する範囲を特定できる。

既稿「証明はいつ数学的知識になるのか」では、証明が生成され、検証され、研究者によって評価され、既存の数学へ位置づけられるまでの状態を区別した[20]。CFSG の形式化では、これに加えて、以前から使用されていた証明経路の一部に反例が見つかり、別の経路によって必要な結論を回復する作業が発生した。UGT の代替証明では、問題のある閉包性の主張を使用せず、別の群論上の結果を組み合わせることで分類に必要な結論へ到達している。形式証明は、そうして組み立てられた推論が形式体系のもとで成立するかを検査するための根拠になる。

この事例で検証対象となるのは、既存の証明に誤りがあったという事実だけではない。誤りのある推論を取り除いた後も、CFSG の分類命題まで有効な証明経路が接続していることを確認する必要がある。公開リポジトリには最終定理の実装とその依存関係が示され、開発元は未証明の穴を残さない形式化を報告している。一方、その成果を独立に再構築したか、形式化された分類対象が本来の数学的分類と一致するかという判断には、それぞれ対応する検証が必要になる。証明の修復が最終結論を維持する根拠となるのは、問題のある中間命題に依存せず、必要な前提から元の結論まで正しい推論が成立している場合である。

7. 証明の誤りが結論まで届く条件

証明の途中に誤りが見つかった場合、その誤りを修正する作業と、最終結論の成立を確認する作業は区別する必要がある。誤った等式を正しい等式へ置き換えるだけで済む場合もあれば、後続の推論を組み替えたり、別の数学的結果を使って証明経路を再構成したりする場合もある。修復の規模が異なるのは、誤った中間命題が後続の証明でどのような役割を果たしていたかによる。修正後の命題が正しくても、以前の推論が必要としていた性質を保証できなければ、最終結論までの証明は回復しない。

最初に扱った偶数の平方の例では、\((2k)^2=2k^2\) という誤った等式を、\((2k)^2=4k^2\) へ修正することで証明が成立した。修正後の式から \(4k^2=2(2k^2)\) と変形できるため、偶数の平方が偶数であるという結論まで正しい推論を接続できる。この場合、誤りは一つの計算に限定され、訂正した等式が後続の推論で必要とする性質を満たしていた。そのため、証明全体の構造を変更せずに結論を回復できた。

一方、CFSG の形式化で報告された Aschbacher と Smith の補題では、等式を不等式へ修正するだけでは後続の証明が成立しなかった。元の証明では、二つの数値が等しいことを利用して特定の場合を排除していたためである。不等式への修正によって補題そのものを正しくできても、等式を前提とした場合分けの正当性は失われる。Axiom Math は、先行する議論で扱う場合を広げ、後続の議論を適用する範囲を再構成することで、必要な結論へ到達したと報告している。ここでは、中間命題の訂正が後続の推論の変更を必要とし、証明の修復範囲が補題の記述を超えて広がった。

不均衡群定理（UGT）の事例では、さらに異なる修復が行われた。Walter の証明経路で使用されていた閉包性の主張は、\(\mathrm{PSL}_2(49)\) に関する反例によって成立しないことが示された。この場合、問題になったのは数値の計算や場合分けだけではなく、ある操作を行った後の群にも既存の定理を適用できるという前提である。その閉包性が失われたため、元の経路で必要としていた定理の適用条件を保証できなくなった。Axiom Math は Solomon の理論などに基づく代替経路を構築し、問題のある閉包性を使用せずに、分類に必要な結論を導く方法を提示した。

三つの事例を比較すると、誤りが発見された箇所と、証明を修復するために変更が必要となる範囲は必ずしも一致しないことが分かる。

事例 反例によって判明したこと 証明の修復に必要だったこと 最終結論との関係
偶数の平方 平方の計算に用いた中間の等式が誤っていた。 等式を訂正し、偶数の平方が 2 の倍数になることを正しい計算から示した。 元の命題を同じ前提のもとで証明できた。
Aschbacher と Smith の補題 二つの数値が等しいという主張に反例があり、後続の証明で使用した性質が保証されなくなった。 補題を修正し、等式を用いていた場合分けの対象範囲を再構成した。 修正後の条件から必要な場合を処理し、分類証明の該当部分を回復したと報告された。
UGT の証明経路 Walter の推論で使用されていた群の族の閉包性が、具体的な反例によって否定された。 Solomon の理論などを利用し、問題のある閉包性に依存しない代替証明を構築した。 既存経路の欠陥とは別に、必要な UGT の結論を導く経路が提示された。

偶数の平方では、誤った計算を取り除いた後も、必要な性質を同じ計算の中で直接示せた。Aschbacher と Smith の補題では、等式から不等式への修正によって失われた情報を、場合分けの再構成によって補う必要があった。UGT では、既存の証明経路が必要としていた閉包性を維持できなかったため、別の数学的結果を組み合わせる経路が採用された。いずれも最終結論を維持する方向で修復が行われたが、修復の成否を決める条件は、訂正後の前提から同じ結論まで有効な推論が成立するかという点にあった。

証明の誤りを発見した後の判断は、三つの状態に分けられる。第一に、問題のある証明を修正するか別の有効な証明を確認できた場合、最終結論は証明された状態にある。第二に、検討した証明が無効になり、別の有効な証明も確認できていない場合、その証明による結論の確立は認められない。この状態では、命題が真である可能性も偽である可能性も残る。第三に、最終命題が要求する条件を実際に満たしながら、その結論に反する対象が見つかった場合、命題そのものが偽であると確定する。

この三つを区別する理由は、反例が否定する対象と、証明が保証する対象が異なるためである。中間命題への反例は、その中間命題を主張された条件のままで利用することを否定する。そこから導かれていた最終結論については、問題のある経路による証明が成立しているかを再確認する必要がある。一方、最終命題そのものへの反例が成立すれば、証明経路を変更しても元の命題を真にすることはできない。その場合に可能なのは、反例を除外する新しい条件を設定するなど、証明対象の命題自体を変更することである。

代替証明が存在する場合にも、その証明が何を前提としているかを確認する必要がある。新しい補題が元の問題を別の名前で再利用していれば、証明経路を変更しただけでは欠陥を解消できない。また、新しい補題が追加の仮定を要求する場合、その仮定を元の証明が対象としていたすべての場合で満たせるかを確認しなければならない。必要な条件を満たす対象についてだけ結論を導けても、元の定理が要求する範囲全体を覆っていなければ、元の結論を証明したことにはならない。証明経路の修復には、推論の正しさと適用範囲の両方の確認が必要である。

UGT の修復では、Walter の閉包性に対する反例が、UGT の最終結論への反例とは区別された。代替経路では、異なる対合の中心化群に現れる構造を比較し、必要な単純群の情報を保存する結果と既存の認識定理を組み合わせている。さらに、Theorem 2.3 を経由しない短い導出も提示された。これらは、最終結論を導くために必要な中間命題が一つの組み合わせに限定されないことを具体的に示している。Walter の経路に誤りが見つかったという事実だけで UGT の結論を維持できたのではなく、別の根拠から必要な結論を導く推論が示されたことに修復の根拠がある。

今回の CFSG の形式化が示すもう一つの点は、証明の規模が増大しても、修復の成立条件そのものは変わらないことである。数千万行の形式証明でも、最終定理の成立は、そこで使用される中間命題と、それらを適用するための条件によって支えられている。形式化によって各依存関係を明示し、証明検査器によって推論の成立を確認できるようになる一方、何を証明対象として定義したか、その定義が本来の数学的主張と一致しているかという確認も残る。公開された形式証明の完成報告と第三者による独立再検証の状況を区別する必要があるのも、どの範囲の正当性が確認されたかを明確にするためである。

証明の途中に誤りが見つかったとき、最終結論まで否定されるかどうかは、その誤りの位置や修正した行数によって決まるわけではない。反例が直接否定する命題を特定し、その命題に依存する推論を確認し、残された証明経路が必要な前提から最終結論まで成立しているかを判断する必要がある。CFSG の形式化で発見された等式の反例と、UGT の証明経路に対する反例は、いずれも中間的な推論の欠陥を示したが、修復には異なる数学的作業が必要だった。誤った証明を退けることと、証明対象の命題を退けることは同じではない。結論を維持する根拠は、問題のある推論を取り除いた後にも成立する、正しい証明そのものにある。

参考文献

  1. id774, フェルマーの最終定理の形式化で、AI が生成した証明を Lean がどう検証したか（2026-09-07）. https://blog.id774.net/entry/2026/09/07/5616/
  2. id774, AI の「正しい」を決める検証契約（2026-09-24）. https://blog.id774.net/entry/2026/09/24/5642/
  3. Ronald Solomon, A Brief History of the Classification of the Finite Simple Groups (2001-03-27). https://doi.org/10.1090/S0273-0979-01-00909-0
  4. Michael Aschbacher, The Status of the Classification of the Finite Simple Groups (2004-08). https://authors.library.caltech.edu/records/5b4mm-frv50
  5. Michael Aschbacher, Stephen D. Smith, The Classification of Quasithin Groups: I. Structure of Strongly Quasithin -groups (2004). https://www.ams.org/books/surv/111
  6. Inna Capdeboscq, Daniel Gorenstein, Richard Lyons, Ronald Solomon, Errata for The Classification of the Finite Simple Groups. https://sites.math.rutgers.edu/~lyons/cfsg/er220303.pdf
  7. Axiom, Formalizing the Enormous Theorem (2026-10-26). https://axiommath.ai/research/the-enormous-theorem-formalized/
  8. Axiom Math, The Unbalanced Group Theorem (2026-10-27). https://hexagonmath.org/2610.00575
  9. John H. Walter, The B-conjecture; characterization of Chevalley groups (1986). https://doi.org/10.1090/memo/0345
  10. Ronald Solomon, Maximal 2-components in finite groups (1976). https://doi.org/10.1080/00927877608822121
  11. Robert Gilman, Ronald Solomon, Finite groups with small unbalancing 2-components (1979). https://msp.org/pjm/1979/83-1/pjm-v83-n1-p05-s.pdf
  12. Richard Foote, Finite Groups with Maximal 2-Components of Type L₂(q), q Odd (1978-11-01). https://doi.org/10.1112/plms/s3-37.3.422
  13. Morton E. Harris, PSL(2,q) type 2-components and the unbalanced group conjecture (1981-01). https://doi.org/10.1016/0021-8693(81)90294-5
  14. Axiom Math, CFSG in Lean. https://cfsg.axiommath.ai/
  15. AxiomMath, Classification of Finite Simple Groups in Lean, README.md. https://github.com/AxiomMath/CFSG/blob/main/README.md
  16. AxiomMath, Comparator/Solution.lean. https://github.com/AxiomMath/CFSG/blob/main/Comparator/Solution.lean
  17. Tau Ceti contributors, The statement of the classification of finite simple groups, Classification.lean. https://github.com/TauCetiProject/TauCeti/blob/6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380/TauCeti/GroupTheory/SpecificGroups/CFSG/Classification.lean
  18. AxiomMath, formalization.yaml. https://github.com/AxiomMath/CFSG/blob/main/formalization.yaml
  19. Lean Project, The Lean Language Reference. https://lean-lang.org/doc/reference/latest/
  20. id774, 証明はいつ数学的知識になるのか（2026-10-09）. https://blog.id774.net/entry/2026/10/09/5760/