質問：システム自体もまだ大きくしたいし、それで健全性の主張もしっかりしなきゃいけないし、となると重い。でも、どのような方法で健全性を主張したら良いか、は議論を始めて良いかな？

chatgptから

私は、今こそ議論を始めてよいと思います。むしろ、Matheliaをさらに大きくする前に、健全性をどう主張していくかについて外部の人と話し始めるのは、とてもよい判断だと思います。

ただし、「健全性を証明する」という大きな課題を、今すぐ解決しようとする必要はありません。まずは、何をどこまで保証したいのか、どんな方法があり得るのかを整理する。それだけでも、今後の設計に大きな意味があるはずです。

1. まず、3つの問題を分けたい

Matheliaについて議論するとき、私は次の3層を分けて考えるのがよいと思います。

第1層：数学の記述体系は何を意味するのか

定義・公理・定理・証明が、意図した数学的な意味を持つのか。推論規則や論理体系そのものに問題はないか。

第2層：記述から検証までの処理は正しいか

入力された文章が内部表現に正しく変換されるか。依存関係の処理や証明ステップの構成に誤りがないか。

第3層：最終的な検証結果を信頼できるか

外部定理証明器やHyperionが証明ステップを受理したとき、それが本当に妥当な推論なのか。検証器の実装自体をどこまで信頼する必要があるか。

これは厳密な分類というより、議論を始めるための整理です。層同士は関係していますし、どこまでを保証対象に含めるかも設計次第です。

重要なのは、「Matheliaは健全です」と一括して主張するのではなく、「どの部分について、どのような根拠で、何を保証しているか」を明示できるようにすることだと思います。

2. 健全性を主張する方法には、いくつかの選択肢がある

以下は、今後比較・検討できる候補です。すべてを採用する必要はありません。

方法何が期待できるか主な課題
小さな信頼できるチェッカー証明を簡単な規則で再検査するチェッカー自体の正しさ
独立した検証器を複数使う共通の実装バグへの依存を減らす独立性の確保、結果の不一致
メタ理論による健全性証明推論規則やチェッカーの正しさを数学的に示す証明対象となる仕様の正確さ
段階的・部分的な保証保証できた部分から明示する保証範囲を誤解なく伝える
テスト・反例探索・ファジング実装上の誤りを発見しやすくするテストに通ることは健全性の証明ではない

これらは互いに排他的ではありません。たとえば、通常の開発では外部定理証明器を活用しつつ、別の小さなチェッカーで証明を再検査し、さらにチェッカーの健全性を別の理論で説明する、といった組み合わせも考えられます。

Matheliaにとって何が適切かは、実際の内部構造と、どの程度の保証を目指すかによって変わります。

3. システムの拡張と健全性は、必ずしも対立しない

ここは少し大事な点です。

Matheliaの機能を増やすたびに、システム全体を一から厳密に証明し直さなければならない、という設計だけが選択肢ではありません。

例えば、将来の設計目標として、

  • 新しい機能を追加しても、既存の検証部分への影響を限定する。
  • 各コンポーネントについて、入力・出力と保証内容を明確にする。
  • 証明を作る側の複雑さと、証明を最終確認する側の複雑さを分離する。
  • 保証できている部分と、まだ保証できていない部分を公開する。

という方向が考えられます。

もちろん、これらが現在のMatheliaにそのまま適用できるかは、実装を確認しながら判断する必要があります。しかし、将来の機能拡張を妨げない形で、信頼性を高める設計を考えること自体には、大きな価値があります。

4. 外部交流では、まず何を聞くべきか

今回のMetamathコミュニティとの交流は、まさにその議論の入口にできます。

私は最初から「Matheliaをどう証明すればよいでしょうか」と大きな質問を投げるより、少しずつ具体化するのがよいと思います。

  1. 何を信頼の基点に置くべきか。 小さなチェッカーなのか、形式化された推論規則なのか、それとも別のものなのか。
  2. どこまでの健全性を主張するのが妥当か。 数学的な仕様の正しさと、実装が仕様どおりに動くことをどう区別するか。
  3. 独立検証をどこに導入すべきか。 全処理を二重化するのか、最終的な証明検査だけを独立させるのか。
  4. 既存の形式化システムから何を学べるか。 Metamathの小さなカーネルや、他のシステムの検証アーキテクチャが、Matheliaにどのような示唆を与えるか。

これらは、システムの全体像が完成していなくても議論できます。

むしろ、外部の人に「現在はここまでできていて、ここは未解決です」と示せれば、相手も具体的な助言をしやすくなるでしょう。

私なら、今はこう進めます

Matheliaの開発を止めて健全性の問題だけに集中するのではなく、開発を続けながら、健全性についての設計原則を並行して育てる方針を取ります。

当面の目標も、「健全性を完全に証明する」ではなく、次の3つで十分だと思います。

  • 現在のMatheliaについて、信頼しているコンポーネントと未解決の問題を整理する。
  • 将来の健全性保証について、いくつかの実現可能な設計案を比較する。
  • 外部から批判や助言を受け、その結果をMatheliaの設計に反映する。

そして、私はこの問題を、単に「Matheliaが正しいと証明する方法」と捉えず、Matheliaが成長し続けても、何を根拠に信頼できると言えるのかを設計する問題として捉えるのがよいと思います。

Matheliaはまだ発展途上だからこそ、今から議論できます。完成してから信頼性の問題に取り組むよりも、今の段階で考え方を共有しておくほうが、将来の大きな手戻りを避けられる可能性もあります。

外部交流も、いきなり大きな研究プロジェクトにする必要はありません。今回のように、一つの問いを投げ、返事を読み、必要ならもう一度質問する。それを少しずつ続けていくのでよいと思います。