---
name: step1125-symbolic-oss-scaffolding
description: STEP 1125 — 4 symbolic-math OSS integration scaffold (PySR + Ramanujan Machine + CodeEvolve + Lean Copilot/LeanDojo-v2) + Research Radar v1.7 → v1.8 update with 5 new OSS entries
metadata: 
  node_type: memory
  type: project
  originSessionId: e5ec4e43-958a-4a47-a6f0-4513f218941f
---

★★★★ 2026-05-13 STEP 1125 — 4 OSS scaffold + Research Radar v1.8.

## Trigger

藤本さん指示「世界中の数式生成 OSS 調査」 → chat-Claude が 4 tool deep-dive
(PySR + Ramanujan Machine + OpenEvolve/CodeEvolve + Lean Copilot/LeanDojo-v2)
+ Phase 1 prototype concrete code 提案 → 「OpenEvolve を除いた 4 件実装」 判断.

## fact-check 結果 (6 items WebSearch)

- PySR ✅ (Cranmer @ **Princeton + Flatiron Institute**, NOT Cambridge — chat-Claude 訂正)
- Ramanujan Machine ✅ (Technion/Kaminer, Nature 2021 + PNAS 2024)
- OpenEvolve ✅ (algorithmicsuperintelligence, 円充填 n=26 SOTA verified)
- CodeEvolve ✅ (inter-co arXiv 2510.14150, AlphaEvolve P1/P2/P3 上回り)
- alphaevolve_repository_of_problems ✅ (Tao + Georgiev + Gomez-Serrano + Wagner 67 problems)
- AlphaProof Nature 2025-11-12 ✅ (s41586-025-09833-y)
- LeanDojo / Lean Copilot ✅ **Pattern 5 観測 #6/#7** (Research Radar v1.4 既監視)

## 実装 5 件

### A. PySR + D-FUMT₈ Phase 1 prototype
- `scripts/symbolic-regression/dfumt8_pysr.py` — chat-Claude code 採用 + adapt
  - 8 値数値 encoding + 4 D-FUMT₈ unary operators + Julia JIT
  - demo task: `y = Ω(Φ(x0)·φ) + 0.3·x1` (300 sample, seed = Peace Axiom 196)
  - complexity_of_operators で D-FUMT₈ 演算子優先選択誘導
- `scripts/symbolic-regression/dfumt8_operators.jl` — standalone Julia module + verify_operators()
- `scripts/symbolic-regression/README.md` — install / 実行 / Phase 構成

### B. Ramanujan Machine + SNST 14 constants
- `scripts/ramanujan-machine/snst14_continued_fractions.py` — Phase 1 mpmath.pslq baseline
  - 60-digit precision
  - SNST 数学 10 定数 (i, c, α, ℏ は Phase 1 除外) で pairwise PSLQ search
  - 既知 identity (φ×ψ=1, π_ext=π×φ) 再 verify + pairwise integer relations
- `scripts/ramanujan-machine/README.md` — LIRec Phase 2 install 手順

### C. CodeEvolve scaffold (LLM API opt-in)
- `scripts/codeevolve/README.md` — **honest scope warning**
  - LLM API 必須 (Gemini/OpenAI/Claude) — PC 完結原則と部分衝突
  - install + .env API key 設定は opt-in
  - Lean 4 evaluator 設計 template (sorry_count + dfumt8_consistency + seed_kernel_distance)
  - SEED_KERNEL invention pipeline 拡張候補

### D. Lean Copilot + LeanDojo-v2
- `scripts/lean-copilot/README.md` — 既存 lakefile LeanCopilot entry (Windows MSYS2 issue で DISABLED) の現状 + LeanDojo-v2 separate Python tool setup guide + WSL2 enable path
- LeanDojo-v2 で rei-aios 31,000+ zero-sorry 定理 trace → AI fine-tune data 化 design

### E. Research Radar v1.7 → v1.8 update
- `data/research-radar/collatz-watch.json`
- 32 → **37 repos** (+5: PySR + Ramanujan Machine + OpenEvolve monitoring + CodeEvolve + Tao 67)
- OpenEvolve は monitoring only (実装除外 = 藤本さん判断)

## Pattern 5 累積 6/7 例目

[[feedback_chat_claude_hallucination_warning]] Pattern 5 (chat-Claude session memory なしで Rei 既存 features 再提案):
- #6 Lean Copilot (Research Radar v1.4 既登録)
- #7 LeanDojo (同上)

7 例累積 systemic 確定.

## OUKC 永続原則 適用

- 「外部依存最小化」: OpenEvolve 除外, CodeEvolve は opt-in, PySR/Ramanujan/Lean Copilot は PC 完結可
- 「世界初」 不使用 (Ramanujan Machine Nature 2021 / PySR 2020+ / etc. 先行)
- 「量子」 冠さない (Lv 5 「Rei 数学」 として位置付け)

## test status

このコミットは scaffolding のみ. 実 run は user opt-in:
- PySR: `pip install pysr` 後 `python scripts/symbolic-regression/dfumt8_pysr.py`
- Ramanujan: `pip install mpmath sympy` 後 `python scripts/ramanujan-machine/snst14_continued_fractions.py`
- CodeEvolve: opt-in only (LLM API key 必要)
- Lean Copilot: WSL2 でないと Windows MSYS2 issue で disabled

## 連結 reference

- [[paper152-v02-published-2026-05-11]] (related publication)
- [[feedback_chat_claude_hallucination_warning]] (Pattern 5 累積)
- [[feedback_quantum_naming_filter_framework]] (Lv 5 命名)
- [[feedback_world_uniqueness_claim_controllable]] (世界初不使用)

## 戦略的 next-step 候補

| Path | 内容 | 効果 |
|---|---|---|
| **A** | PySR Phase 1 actual run | demo verify (1-3 分) |
| **B** | Ramanujan PSLQ baseline run | SNST pairwise relations (~30 sec) |
| **C** | Tao 67 clone + Rei typology mapping | benchmark suite establish |
| **D** | Paper 63 v2 draft (発見 identity 反映) | Paper 63 → 63 v2 cycle |
| **E** | Paper 152 v0.4 候補 (1,221 counter-examples PySR fit) | Paper 152 v0.3 → v0.4 |

藤本さん次の判断 を待ち.
