なぜすべてカーネルにあるのか？

Machine Logic計算、論理、数学の交差点でなぜすべてカーネルにあるのか？2026年7月30日[一般Lean Isabelle HOLシステム哲学記憶]センセーショナルなニュース！Collatz予想が反証されました。Ramana Kumarがその否定を証明しました。証明はLeanでチェックされ、独立したNanoda型チェッカーを使用して二重チェックされました。残念ながら、証明は間違っていました。それはLeanカーネルのバグを利用していました。Nanodaもエラーを検出できませんでした。さて、私はこれを自慢するために書いているのではありません。Isabelleを含む多くの証明支援システムで健全性バグが発見されています。私の知る限り、明日も新しくて恐ろしいバグが発見されるかもしれません。それにもかかわらず、ここにはいくつかの教訓があります。さあ、始めましょう！Collatz予想この有名な予想は、約1世紀前から、真面目な数学者と変わり者の両方の注意を引いてきました。それは次の手順に関係しています。数Nから始めます。次にこのステップを繰り返します。Nが偶数なら2で割ります。奇数ならNを3N+1に設定します。Collatzは、この手順がどのようなNの値から始めても必ず1に到達すると予想しました。広範なテストでも、単一の反例は見つかっていません。最近の研究では、言語モデルが予想の反例を見つけるのに非常に優れていることが示されていますが、Collatzはどうでしょうか？それを解決することは、確かにセンセーションを引き起こすでしょう。 証明オブジェクトのデッドウェイト我々が半世紀前から知っているように、証明オブジェクトは不要です。Robin Milnerは、証明支援システムをサポートする目的でML言語を設計しました。抽象型の概念を通じて、証明カーネルはプログラムの残りの部分から安全に保つことができました。推論規則は、抽象型内に限定され、定理を作成するためのAPIとなるでしょう。それにもかかわらず、私たちのコミュニティの多くは証明オブジェクトの保存に固執しています。特に、証明オブジェクトは独立してチェックできる証明書であると指摘しました。しかし、私は独立した証明チェッカーが証明支援システムのカーネルを通過した健全性エラーを検出した単一のインスタンスを知りません。Collatzの場合、見たように、Nanodaも騙されました。 証明オブジェクトが表すメモリの負担を考えると、これは、故障した場合に備えてトレーラーに予備の車を牽引して、どこへ行くにも運転するのと似ています。そしてあなたの車は故障しますが、見てみると、予備の車も機能しません。そして、あなたの車が故障した正確な理由は、予備の車を牽引する負担でした。証明オブジェクトを持つ証明計算だけが、すべてをカーネルに入れる必要があるように見えるからです。 盗み対誠実な労働20世紀のほとんどの間、論理学者は、そこから数学の残りを導き出すために、可能な限り少ない公理を仮定しました。おそらく彼らはRussellのパラドックスや他のパラドックスを心配していたのでしょう。おそらく彼らは単に倹約家だったのでしょう。この見解は、おそらくRussell自身が最もよく述べています。「欲しいものを『公理として設定する』方法は多くの利点があります。それは盗みが誠実な労働よりも優れているのと同じ利点です。それらを他人に任せ、私たちの誠実な労働を続けましょう。」（Russell、1919年） したがって、噂によれば、Leanのバグはカーネル内のネストされた帰納型によって引き起こされたことは注目に値します。Rocqの健全性バグの多くは、カーネル内の再帰関数を含むパターンマッチングによって引き起こされました。従属型理論が、より基本的な計算から再帰のようなものを表現するのに十分な表現力を持っていない理由を正確には知りません。理由は技術的なものでしょう。しかし、はっきりさせておきましょう。集合論と単純型理論では、非常に少ないことを仮定する必要があります。集合論は、集合を導入するためのいくつかの原則を提供します。和集合、分離、ペアリング、置換。単純型理論は、論理とλ計算の少しを提供し、それは型付き集合論を提供し、そこで集合はブール値関数です。次に、誠実な労働によって、帰納的定義、レコード、再帰的データ構造、および帰納的関数を、パターンマッチングや部分関数を含む非常に一般的な設定で取得できます。シンボリックバイナリ算術を使用して数値計算を実行できます。これらすべてが原始公理に基づいて定義されており、公理として設定されているわけではないため、カーネルの外にあり、矛盾につながることはありません。 1980年代に戻り、Martin-Löf型理論を扱っていた頃、再帰関数を表現することについての質問が生じました。理論は原始帰納の形式しか認識しませんでした。しかし、理論は高階型も許容し、より強力な形式の帰納の可能性を与えました。誠実な労働の伝統で数学を学んだ私は、Martin-Löf型理論内に、広大な終端帰納関数の空間を表現できるコンビネータシステムを定義するために（そしてそれは本当に骨の折れる仕事でした）働きました。しかし、私はこのゲームの遊び方を理解していませんでした。質問に対する正しい答えは、MLTTに一般的な帰納の概念を拡張することでした。そして、それはシンプルかつエレガントに行うことができたと認めなければなりません。私がやったことを誰かが理解したかどうかはわかりません。数年後、私はこの論文が「PaulsonはMLTTに帰納を拡張した」というコメントとともに引用されているのを見ました。彼らは、誠実な労働によって帰納を得た人を想像できませんでした。 誠実な労働とはどのようなものか？証明支援システムの開発者が盗みの選択肢を選ぶ理由がわかります。なぜなら、誠実な労働は本当に岩を砕くようなものだからです。多くの目標の中で最も簡単なのは、再帰的データ構造です。帰納的定義は、集合上の単調演算子に変換できます。最小不動点が帰納的定義を与え、共帰納的定義を好む場合は、最大不動点を取ります。Isabelleでは、これらの構成を型にリンクすることはめったにありませんが、再帰的データ型は重要な特殊ケースであり、現在では有界自然関手を通じて一般的かつ洗練された方法で処理されています。 最初の原理からの帰納関数の構築は特に面倒です。まず、よく確立された関係から始め、よく確立された帰納法によって目的の帰納関数の存在を証明します。MLTTでの帰納に関する私の仕事はいくらか役立ったので、それは完全に無駄ではありませんでした。Isabelle/HOLは現在、パターンマッチングや終了チェックを含む、非常に一般的な再帰関数定義をサポートしています。そして、これらすべてはカーネルの外に安全に配置されています。 証明オブジェクトが、より大きな健全性保証につながると謳われることがあるという皮肉があります。逆が明らかに真です。健全性があなたの主な懸念であるなら、HOL LightまたはHOL4に行くべきです。Isabelleはそれらよりも多くのバグがありますが、数は少なく、確かに他のいくつかのシステムよりもはるかに少ないです。あるいは究極はCandle、HOL Lightの検証済みバージョンです。↩