数学的証明に関するsubjective vs objective

Vladimir Voevodskyが査読の通った自分の論文の証明の誤りに気づきcoq/unimathによる証明システムに取り組んだことや、Jacob Lurieが数学的証明を公言するのは誤りが100%ないことを保証する必要のある恐怖のあるアクションであると語っていることから、第一線の世界的数学者だとしてもその理論の証明ステップを100%保証することはとても精密な作業である。

証明とは「客観的な再構築性」の保証である

数学者が「証明した」と言うとき、それは「私(我々)は納得した」という意味ではなく、「誰が（あるいはどのマシンが）辿っても言語や記号に依存することなく同じ結論に辿り着く、欠落のない有向グラフを構築した」という意味である。

例え数学界の中核にいる人物だとしてもこの厳密性を取り違えて「証明した」と宣言してしまうのは禁じ手に近い。例えば、ABC予想の証明を2012年にIUT理論が証明したと発表されたが、一般的には数学ではこのような自己宣言はされることはない。数学的証明とは、論理的存在に関するトートロジーであり、選択された公理系において真であるものは真であるというホモトピー等価性を宣言するものである。そしてこの工程はNP-completeであることから3-SATやboolean algebraの形式に置き換えられて当然の主張である。ケプラー予想のトーマス・ヘイルズ証明はシステムによる厳密なconstructive stepが完了するまで「証明された」という宣言はなされていない。ペレルマンのポアンカレ予想の証明も静かにArxivにアップロードされただけであり、「証明された」と宣言できるのはあくまで第三者が論理ステップを客観的に再構築した場合に限るのである。例えばフェルマー最終定理のアンドリューワイルズ証明も、ワイルズは証明したとして論理のステップを公開した。しかし、論理のステップを説明しているうちに自分の論理に飛躍していることに気づき、その後１年間かけてその論理の飛躍を取り除くための既存定理への可換性検証を始めたのである。

つまり、数学的な証明とは時間や空間に依存することのない100%の堅牢性を保証するものなのであり、これは「証明が終わった」とsubjectiveに宣言できるようなものではなく、現実世界における再現が完了するというobjectiveなプロセスなのである。もちろん、subjectiveなconjectureやpostulate、frameworkもたくさんある。例えば、フェルマーの仮説はワイルズに証明されるまでは単なる予想、conjectureにしかすぎなかった。ホモトピー、トポロジー、数論、代数などの幾何化イニシアティブであるラングランズプログラムもobjectiveな数学的証明ではなく、subjectiveなムーブメントに過ぎない。

例えばZFCにおいてバナッハ＝タルスキのパラドックスのような、最小単位の無限小を扱うと集合が２つにコピーされてしまうという直観的矛盾も、それは無限の性質であると既存の公理系と矛盾のない形で論理的に解決、接続される。また、IP=PSPACEやArthur-Merlin protocol のように、2点問題でNPやEXPも検証できるのである。量子もつれを用いたMIP*= REはNEXPTIME（P ⊆ NP ⊆ EXPTIME ⊆ NEXPTIME）まで多項式で証明できるのである。数学における「証明」とは、宇宙のどこに持っていっても、あるいは1億年後のAIが検証しても、同じ公理系の下では同じ結論（ホモトピー等価性）に収束する堅牢な構造物のトポロジー連続性解析および離散的な記述である。数学的に選択された公理に基づく表現に矛盾がないかどうかはpolynomial equationによって検証できるというのが現代数学の発見の歴史であって、「私の説は斬新すぎるので既存の公理系と接続することはできない」というのはモノイダル圏だとしてもCohen forcingで積法合成できる以上、それは証明形式を充足していないことの言い訳に聞こえてしまうのである。