---
name: reference-alphaproof-nature-2025-open-adoptable-techniques
description: "AlphaProof (Nature 2025-11-12, s41586-025-09833-y) から solo Lean 4 researcher が採用可能な 4 core technique"
metadata: 
  node_type: memory
  type: reference
  originSessionId: bf3ef5b0-e925-41af-95a6-5ab728a320be
  modified: 2026-07-19T14:32:43.288Z
---

# AlphaProof (Nature 2025-11-12) — Open-adoptable techniques for solo Lean 4

**Source**: "Olympiad-level formal mathematical reasoning with reinforcement learning" (Nature 2025-11-12, DOI s41586-025-09833-y). IMO 2024 silver (4/6 problems P1+P2+P6+ AlphaGeometry) / IMO 2025 gold pipeline.

**Rei 2026-07-19 audit**: 実装非対象 (情報のみ) だが、既存 Rei stack と符合する core insight が 4 件あり、部分的に既実装。

## 4 core adoptable techniques

### 1. Auto-formalization pipeline (両ステージ LLM + stochastic)

- 段 1: natural language → Lean, 段 2: Lean statement → proof
- **stochastic prompt**: 1 statement から 80+ 変種を意図的生成
- 「意味誤 formalization も training value あり」 = Lean type system で自動 validate
- Solo 適用: 任意 LLM API で prompt vary → 合成 training data

**Rei との符合**: STEP 1257 (Semantic Scholar + arXiv prior-art audit hook) は formalization ではなく radar 側で類似 stochastic search を既導入。formalization 側は未実装 (現状 手作業 mathlib port)。

### 2. Test-Time Reinforcement Learning (TTRL)

- 訓練時 RL でなく **推論時** RL に集中
- 対象 theorem を LLM prompt で 5-10 variant 生成 → 逐次 proof search → 早い variant で easy sub-problem を露出 → curriculum learning
- Solo 適用: 分散不要、sequential search で run 可

**Rei との符合**: STEP 622-624 Collatz Cases 5-8 変種列挙は概念的に類似 (問題を分解 → sub-lemma 逐次 attack) だが、LLM prompt vary 経由でなく手作業。TTRL 型自動化は future candidate (Priority 3+ の中期 candidate)。

### 3. Product-node MCTS (goal-splitting handling)

- 通常 MCTS: goal-split は "or" node (どれか proved で ok)
- AlphaProof: **product node** = 全 child 必要 (∧ 型)
- Backprop: **最難 branch の difficulty** で価値伝搬 (平均でなく)
- Solved sub-goal を marker で skip → wasted search 削減

**Rei との符合**: Lean 4 の tactic tree (`⟨_,_⟩` intro / `constructor` / `refine`) は既に product 構造。Rei は MCTS 使わず tactic 直書き + `decide` / `omega` / `duper` に依存で、product-node search infrastructure は未実装。small Rei 個別 lemma (STEP 1264 refinement 等 <20 theorem/file) では overkill 判定可。

### 4. Encoder-decoder single-embed + parallel tactic sampling

- 大 Lean state を **1 度だけ embed** → 多 tactic を並列 sample
- Single-GPU memory 内で完結
- Pretraining (12 trillion token, 50 epoch) は skip 可 = 既存 Lean-Copilot / DeepSeek-Prover-V2 / duper で代替

**Rei との符合**: Lean-Copilot + duper + LeanHammer は既 Radar watch (Layer 2 証明補助)、実運用は Lean Copilot + duper (前 session memory Layer 2 記載)。encoder-decoder embedding infra は未導入。

## Rei 現時点の判定

**Priority 3 「情報のみ」 結論** (藤本さん指示通り実装非対象):

- 既存の Layer 2 (証明補助 tool: Lean-Copilot + duper 実運用) が AlphaProof の (4) 相当を軽量 substitute
- (1) auto-formalization stochastic + (2) TTRL は Rei にとって将来 candidate だが、solo 現状は手作業 mathlib port + Chang paradigm retrofit (12/29 = 41.4%) の方が yield 高い
- (3) product-node MCTS は Rei scale (individual lemma file ≤20 theorem) では overkill
- 「Distributed RL 不要 + search-time optimization > raw model scale」 という核 insight は既 Rei が体現 (単一 machine + tactic-native search + honest coverage tracking)

**next candidate** (別 STEP 化推奨):
- AlphaProof の "randomized prompt formalization" を Rei radar (STEP 1257 hook) と合成 → Chang 17 gap paradigm の Lean 4 skeleton auto-generation prototype
- ただし急がずゆっくり ([[feedback-no-rush-publication]])

## 関連

- [[project-session-2026-07-19-priority-1-2-arc]] (本 audit は D 項目)
- [[feedback-zero-sorry-floor-not-ceiling]] (AlphaProof 「100% correct via Lean」 = zero-axiom floor と同 stance)
- [[feedback-external-community-outreach-premature]] (AlphaProof チームへの outreach 対象外)
- [[feedback-evaluation-symmetry-principle]] (AlphaProof を inflate せず deflate せず: 既 (4) は Lean-Copilot で substitute 済、(1)(2) は future candidate、(3) は scale mismatch)
- [[reference-llm-driven-code-evolution-frameworks-2026]] (AlphaEvolve etc. と系統的位置付け)

## Sources

- Nature 2025-11-12 s41586-025-09833-y
- julian.ac blog 2025-11-13 (open-adoptable technique summary source)