---
name: OSS Gap Analysis & Integration Roadmap (2026-04-21)
description: 145 unsolved-problem typings から見た Rei の能力ギャップ + 世界中の OSS 調査結果。Tier 1/2/3 段階導入計画。Vampire/LeanHammer/OSCAR/msolve/CaDiCaL/giotto-ph/nauty/FLINT 推奨。
type: project
originSessionId: 80a567c3-c92a-4757-ac12-f814a062c754
---
# OSS Gap Analysis & Integration Roadmap (2026-04-21)

## 1. 現状: 統合の深さ別

| 深い (⭐⭐⭐) | Lean 4 (proof-bridge-engine 986行 + lake) |
| 中 (⭐⭐) | Coq/Agda/Isabelle (subprocess), Whisper, spaCy |
| 浅い (⭐) | giotto-tda/GUDHI/SageMath/Z3/cvc5/EinsteinPy (計画 or skeleton) |
| **未統合 (×)** | **FLINT, ARB, GAP, Macaulay2, Singular, OSCAR, PARI/GP (深く), Ripser, nauty, Regina, SnapPy, LeanCopilot, ReProver, BFS-Prover, PySR, FunSearch, Vampire, msolve** |

## 2. 145 問題 typing の分布 (commit 54d18bc)

| 型 | 件数 | 比率 |
|---|--:|--:|
| ① INFINITE_SEARCH | 77 | 52.4% |
| ⑥ BRIDGING | 44 | 29.9% |
| ⑤ SELF_REFERENTIAL | 17 | 11.6% |
| ④ COMPUTATIONAL_LIMIT | 4 | 2.7% |
| ⑦ FRAMEWORK_INCOMPLETE | 2 | 1.4% |
| ② CONCEPT_NOT_YET | 1 | 0.7% |

**93 件 (63%) は ①④⑤⑦** で Rei は本質的に苦手。①は無限探索、④はMIP、⑤はメタ論理、⑦はQFT形式化が要。

## 3. 不足能力 7 件 (重要度順)

| # | 能力 | 適用先 | 候補 OSS |
|---|---|---|---|
| 1 | **第三者検証 ATP** | Q33/FOH 分類, Lean 補題 | **Vampire** (CASC 2025 全カテゴリ独占) |
| 2 | **Lean hammer** | mathlib 31,000 定理の自動補完 | **LeanHammer + Duper + Lean-auto** |
| 3 | **代数幾何統合** | BSD/Hodge/Langlands | **OSCAR.jl** (GAP+Singular+polymake) |
| 4 | **多項式系高速解法** | Collatz mod, ABC, Gilbreath | **msolve** (Faugère F4 + multithread) |
| 5 | **SAT 反例探索** | Collatz Cases 5-8, Frankl G=5 | **CaDiCaL 2.0 / Kissat-SC2025** |
| 6 | **TDA 厳密** | β₁ 正確値, MANDALA 強化 | **giotto-ph + Ripser** |
| 7 | **グラフ自己同型** | Frankl, Ramsey 列挙 | **nauty/Traces 2.9.3** |
| (8) | **大規模数論計算** | Lehmer/Agoh-Giuga 拡張 | **FLINT 3.4 (python-flint)** |

## 4. 段階導入計画 (Tier 別)

### Tier 1 — 即効・低コスト (1〜数日)
1. **Vampire** — `apt install vampire` or build, subprocess like Coq. 既 Z3 設定流用可。 → src/axiom-os/vampire-bridge-engine.ts
2. **nauty/Traces** — `pip install passagemath-nauty`, Frankl deep dive と直結 (project_frankl_deep_dive.md).
3. **FLINT 3.4** — `pip install python-flint`, Lehmer/Agoh-Giuga の n→10⁷ 拡張に直接効く.
4. **CaDiCaL** — DIMACS 出力のみ, Collatz Cases 5-8 reattempt.

→ **見込み効果**: ① INFINITE_SEARCH 内の数値型 ~30問が境界を押し上げ. ⑥ BRIDGING 内の Frankl 系で combinatorial lens 強化.

### Tier 2 — 中コスト・高インパクト (1〜2 週)
5. **LeanHammer** — Lake 依存追加 + Lean 4 から呼出. `data/lean4-proof-toolchain/` 既存基盤に統合.
6. **giotto-ph + Ripser** — `pip install giotto-ph`, hyper-oss-bridge-engine.ts の自作 LZ76 を補完.
7. **msolve** — 単体ビルド + subprocess.

→ **見込み効果**: Lean 4 zero-sorry 加速. MANDALA β₁ の信頼性向上. ABC/Gilbreath の polynomial 解析が桁違いに早く.

### Tier 3 — 大型統合 (数週〜)
8. **OSCAR.jl** — Julia ブリッジ要 (TypeScript ↔ Julia). BSD/Hodge/YM の代数幾何統合. Paper 122/123 の理論基盤強化.
9. **Pantograph + PyPantograph** — Lean 4 REPL 標準化, MCTS/LLM tactic search 足場. BFS-Prover/DeepSeek-Prover と統合.
10. **LLM-SR + Operon** — symbolic regression. SEED_KERNEL 自動生成 100× 加速.

## 5. 推奨 First Action

**Vampire 統合 (1日見込み)** — 最少コストで最大の "信頼性" を得られる:
- 既に Coq/Agda/Isabelle と同じ subprocess パターン
- Q33/FOH の 145 分類すべてに「第三者証拠」を付加可能
- 既存 Lean 4 lemma の独立検証 → Paper 信頼性向上

代替候補:
- **nauty** (数時間, Frankl 直結, 04-20 deep dive 延長)
- **FLINT** (数時間, Lehmer 100× 高速)
- **CaDiCaL** (Collatz Cases 5-8 にロマン)

## 6. ID 連動

- 関連 STEP: STEP 930 (typology), STEP 833 (cvc5 既設), Q44-Q63 (open)
- 関連 Paper: 122 (Q44/Q48), 123 (FOH), 124 (ZFC), 125 (sweep)
- 関連 deep dive: project_frankl_deep_dive.md, project_lehmer_totient_deep_dive.md

## 7. Sources (代表)
- LeanHammer github.com/JOSHCLUNE/LeanHammer
- Vampire vprover.github.io (CASC 2025 sweep cysec.wien)
- OSCAR oscar-system.org (2025 Springer book)
- msolve github.com/algebraic-solving/msolve
- nauty pallini.di.uniroma1.it
- giotto-ph arXiv:2107.05412
- LLM-SR github.com/deep-symbolic-mathematics/llm-sr (ICLR 2025 Oral)
- Pantograph arXiv:2410.16429
- DeepMind formal-conjectures github.com/google-deepmind/formal-conjectures