Crab Research
研究ホーム/数学
主力研究プログラム / 数学

Proof Engine

Crab Research の主力数学研究プログラムです。正確な命題、読める論証、再現可能な証明の証拠を通じて、信頼できる AI 支援数学研究を進めます。

組合せ論 · 数論 · 幾何学17 件の数学的結果 · 4 件の方法論論文

信頼性と検証の基準

形式検証とは、定理と証明を証明支援系が検査できる厳密な形で記述することです。以下では、完了した検査と残っている前提を説明します。

内部レビュー済みの原稿（Paper Close）

内部レビューを終えて公開しています。主要結論の完全な形式化はまだ確立されておらず、誤りが残る可能性があります。

外部定理を前提とする検証（Reference-Gated）

引用する定理の一部を明示的な前提とし、証明支援系はその前提の下で残りの推論を検査します。前提とした定理の証明は、まだ公開パッケージに含まれていません。

基礎公理のみに基づく検証（Kernel-Only）

証明支援系は引用結果を含むすべての定理依存を検査し、未証明の定理を追加の前提にしません。許容するのは、推論の出発点となる以下の基礎公理のみです。形式化と論文の対応も確認しますが、説明の修正が必要な場合はあります。

propext (命題の外延性); Classical.choice (古典選択公理); Quot.sound (商型の健全性).

査読済み · 採択済み

独立した査読を経て、学術誌または査読付き会議に採択されています。外部の学術的な受容を示し、採択と正式な公刊は別々に記録します。

最終的な形式化として認める基準は Kernel-Only のみです。Reference-Gated は信頼性がそれより低く、工程規模が特に大きい場合に限って中間版として公開します。査読によって未証明の定理の前提が解消されるわけではありません。

検証方法と適用範囲の詳細を読む

正確な定理依存関係

引用する結果には、正確な定理文、出典、対応する検証済み形式的定理が必要です。Lean/mathlib の既存のカーネル検証済み証明は再利用できます。すべての依存は最終的に propext、Classical.choice、Quot.sound のみに帰着させ、追加の定理公理、sorry、カーネル未検証のネイティブ計算による省略は認めません。

Reference-Gated 版では、正確な命題・仮定・量化・出典箇所・形式的前提・依存する結論を記した関門一覧を公開する必要があります。Kernel-Only に到達するには、検証済み証明ですべての関門を解消し、最終定理と論文との対応を再確認します。

最終定理の公理レポートは、証明が実際に何に依存しているかを示します。その命題が意図した数学的定理に対応するかは別途確認が必要であり、公理レポートだけではその対応は確立しません。

数学的結果 17

SSRN のワーキングペーパーは、十分に展開された研究です。一部は意図的に独立したワーキングペーパーとして維持されます。研究の成熟度と公刊状況は別に記録します。

17 件の結果 · 学術的な公刊・採択を優先 · 記録更新 2026-09-06

初期段階のワーキングペーパー 7論文を表示論文を閉じる

初期のアイデア、草稿、さらなる展開や検証を要する研究を、進行中の成果として公開しています。

私たちは、AI 時代の数学における重要な変化は成果の量の増加にとどまらず、高速な生成によって、従来の数学体系で検証・解釈・再利用・保守を結ぶ工学的な層の不足が顕在化し、新しい研究の分業が開かれることにあると考えます。AI は論証の候補生成や証明経路の探索に参加し、数学エンジニアのような新たな役割は、それらを検査・再現・継続利用できる成果に整えます。数学者は、価値ある問いを立て、構造を発見し、概念を生み出し、結果を説明・一般化する中心的な役割を担います。これらの役割は重なり得るものであり、Proof Engine は公開された数学的事例を通じて、その基本的な実現可能性を探っています。 詳しい論証は方法論論文をご覧ください。

方法論

Proof Engine 1.0 と 2.0

数学研究における相互補完的な二つの層です。1.0 は証明開発を組織し、2.0 は数学的探究を統括し、その中で 1.0 を利用できます。

Proof Engine 1.0

証明開発

正確な命題・証拠・依存関係を組織し、未解決の証明義務を明示し、訂正を論証全体へ伝播させます。

論文を読む · SSRN 7237460
初回公開
2026-07-29
最新の公開改訂
2026-08-31

Proof Engine 2.0

研究ガバナンス

数学的探究の問い、意図する貢献、必要な証拠を統括します。自律的な実行は、人間が承認した範囲内に留まります。

論文を読む · Zenodo ワーキングペーパー
初回公開
2026-09-05
最新の公開改訂
2026-09-05

方法論の論文 4

SSRN のワーキングペーパーは、十分に展開された研究です。一部は意図的に独立したワーキングペーパーとして維持されます。研究の成熟度と公刊状況は別に記録します。

4 件の論文 · 学術的な公刊・採択を優先 · 記録更新 2026-09-06

研究ホームに戻る