2. Mathelia本体の信頼性を主張するためにすべきこと

来年の商用化において、研究者やエンジニアから「Matheliaの 〇（OK/PASSED）は本当に信頼できるのか？」と問われた際、どう答えるかは極めて重要なブランディングになります。

「今は手が回らない」とのことですので、「今すぐできる最小コストの施策」から「将来的に実装すべき本格機能」まで段階的に整理しました。

Phase 1: 今すぐ（低コスト・文章や運用でカバー）

  1. 「偽の 〇（反例集）」の公開とCIテスト（回帰テスト）の明記
    • チュートリアルにあった「偽の〇（通ってはいけない記述が通ってしまうバグ）を反例集に蓄積し、修正後も自動テストで弾かれているか検証している」という運用方針は、信頼性向上において最大の強みです。
    • これを「About Mathelia」やドキュメントで前面に出し、「バグを隠さず、回帰テストで健全性を担保している」ことを宣言するだけで、専門家からの信頼度が大きく上がります。
  2. 前提（Γ）の完全開示アピール
    • 「ブラックボックスなライブラリに依存せず、その定理が依存している公理・前提・定義がすべて A ◀ Γ に明示される」という設計自体が強力な信頼性の根拠になります。

Phase 2: リリース前後（システム的補助）

  1. 証明カーネル（Checker）の分離・独立
    • 現在のHyperion（つなぎ）や各種Proverの出力を、「最小限のルールだけを持つ小さな検査器（Independent Micro-kernel）」で再検証できるようにする構想（3.1節の目標）です。
    • 「本体エンジンが複雑でも、最後に数文字のルールチェックを通しているため偽の〇は出ない」と言える状態にすることが、形式検証ツールにおける究極の信頼性担保になります。
  2. 査読結果の機械可読化（JSON出力）
    • 3.2節にある「依存関係・使用した公理・翻訳後の式・実行時間をJSONで書き出す機能」です。これにより、第三者がMatheliaの検証結果を外部ツールで二次検証・分析できるようになります。