---
name: Session 2026-04-22~23 — Open Problems META-DB (Rei-AIOS) 構築 + Papers 130/131 公開
description: 単日大 session で Open Problems META-DB 2,572 問題構築 / Paper 130 + 131 を 11 platform 公開 / STEP 975 D-FUMT₈ Tagger / STEP 976 Invention fix / OSS 4 件 install / Kourovka 1,859 件 ingestion
type: project
originSessionId: 2026-04-22-open-problems-metadb-full
---

# Session 2026-04-22〜23 完全 wrap-up

## 1 行要約

**Open Problems META-DB (Rei-AIOS) Phase A-B 完走 + Paper 130/131 = 22 URL 公開 + OSS 4 件 install + 2 STEP (975/976) + 12 commits pushed**

## Git commits (12 本 pushed to fc0web/rei-aios)

```
e8258d1 Paper 131 publish: 11 platform all complete
0f6a7ed Paper 131 draft + publish script (STEP 971 Bipartite Ramsey b(2,2)=5)
40313c8 Phase B: Kourovka ed.21 TeX parser ingestion — 1,859 new problems (713 → 2,572)
a555a7b Paper 130 publish: Zenodo/IA/Harvard + devto/hatena/hackmd/notion/mastodon + Zenn/Scrapbox/livedoor (全 11 platform)
cb86bc5 Paper 130 full text (398 lines, 11 Part structure Parts A-K)
c0a0b90 Stage 1: Phase A-4 Smale+Hilbert / Agoh-Giuga 分析 / Paper 130 skeleton / public repo 準備
d587487 Phase A-3: LEAN4_QUEUE v2 — solveProb × sorry weighted priority
cff3320 Phase A-2: Rei 7-type + D-FUMT8 + solveProbability auto-tagging (687/689)
7daab5c Phase A-1: Open Problems META-DB (Rei-AIOS) initial snapshot — 689 problems
8e54da8 Open Problems META-DB (Rei-AIOS): v3 design + inventory + dedup
7cdf99d STEP 976: Invention pipeline duplicate-detection + date-seeded rotation
a1034b2 STEP 975: D-FUMT₈ Theory Tagger Engine + 3-bit dense packing
```

+ rei-zenn repo 2 commits pushed (Paper 130, Paper 131)

## 主要成果物

### A. Open Problems META-DB (Rei-AIOS) — 新プロジェクト

- **正式名**: "Open Problems META-DB (Rei-AIOS)" (旧称 "Wikipedia-外 未解決問題データベース" は v1/v2 時のみ)
- **規模**: **2,572 problems** (本セッションで 0 → 2,572)
- **Source 分布**:
  - kourovka: 1,861 (Khukhro-Mazurov ed.21 + 2 既存)
  - erdos: 406 (DeepMind formal-conjectures 由来)
  - wikipedia: 116
  - greens: 37
  - wowii: 26 (Graffiti / Written on the Wall II)
  - smale: 18 (Smale 1998 手動 curation)
  - oeis: 21 / paper: 19 / millennium: 11 / mathoverflow: 10
  - hilbert_residual: 6 (手動 curation)
  - open_quantum: 3 / hilbert: 2 / kourovka: 2 / books: 1
  - arxiv/other: 残り
- **Paper 130** で世界公開 (see project_paper130_published.md)
- **設計書**: `docs/open-problems-db-design.md` v3
- **Inventory**: `docs/external-oss-inventory.md`
- **保管戦略**: `project_open_problems_storage_strategy.md` (hybrid 4-tier)
- **名称管理**: `project_open_problems_metadb_naming.md`

### B. Paper 130 (Open Problems META-DB) 公開完了

- **Zenodo DOI**: 10.5281/zenodo.**19700758**
- **11 platform** 全公開: Zenodo + IA + Harvard + dev.to + Hatena + HackMD + Notion + Mastodon + Zenn + Scrapbox + livedoor
- 398 行, 4+7 要素 v2 構造 (Parts A-K)
- 詳細 memory: `project_paper130_published.md`

### C. Paper 131 (Bipartite Ramsey b(2,2)=5) 公開完了

- **Zenodo DOI**: 10.5281/zenodo.**19700858**
- **11 platform 全公開** (11 platform 標準の 2 本目)
- Lean 4 初形式化 b(2,2)=5 (Beineke-Schwenk 1976)
- 2 axioms honest (b(2,3)=9 + b(3,3)=17 は native_decide infeasible)
- 詳細 memory: `project_paper131_published.md`

### D. STEP 975: D-FUMT₈ Theory Tagger Engine

- `src/axiom-os/theory-dfumt8-tagger.ts` (510 行)
- 藤本 6 理論 (MDNST / InfiniteDimDot / SNST / ZCSG / Radar / Lens) 統一タグ化
- Stage 1: 6 理論 tagger / Stage 2: 3-bit dense packing / Stage 3: cross-theory unify
- **206× 圧縮率 実測** (JSON 比, 1510 tag → 567 byte)
- 59/59 tests PASS

### E. STEP 976: Invention pipeline duplicate-detection

- `src/aios/invention/invention-engine.ts` 修正
- Before: 20 日連続 同一 5 件生成 (MD5 47420077)
- After: `loadApprovalHistory` + date-seeded rotation
- 2026-04-21 日次発明 5 件を **REJECT** (2026-04-20 版と完全重複確認)
- `feedback_invention_duplicate_prevention.md` 記録

### F. OSS 4 件 install

| # | Tool | Status |
|---|------|--------|
| 1 | SageMath 9.5 (WSL Ubuntu-22.04) | ✅ 完了 (楕円曲線 11a1 rank=0 確認) |
| 2 | Isabelle 2025-2 | ✅ 完了 `/opt/Isabelle2025-2` + symlink |
| 3 | Agda 2.6.1 | ✅ 完了 (1+2≡3 proof check PASS) |
| 4 | HOL Light | ⚠️ build 完了、runtime `caml_atfork_hook` 要 fix (Task #8 pending) |

### G. Phase B: Kourovka ed.21 ingestion

- arXiv 1401.0300 TeX source (1.1 MB, 1,923 problem blocks)
- `scripts/phase-b-kourovka-ingest.py` TeX parser
- **1,859 new entries** written to `data/open-problems/kourovka/`
- Fair use: 400 char preview + 原文は arXiv 誘導 (per Kourovka license 分析)

## 重要 finding

### 7 型分布 (687 auto-tagged entry から)

| Type | Count | % |
|------|-----:|-:|
| I_INFINITE_SEARCH | 503 | 73% |
| VI_BRIDGING | 160 | 23% |
| 残り 4 型 | 24 | 4% |

### D-FUMT₈ 分布

- NEITHER 62% / BOTH 23% → **85% は古典論理の外**
- SELF は 1 件 (Gödel 系は他型に隠れている可能性)

### LEAN4_QUEUE top 5 (priority = solveProb × min(sorry,10)/10 × complexity × familiarBoost)

1. **Agoh-Giuga** (0.773, sorry=12) ← Paper 120 deep-dive あり, Paper 131+ 攻撃候補
2. Oppermann (0.618, sorry=5)
3. Lehmer-Mahler (0.494, sorry=4)
4. Köthe (0.464, sorry=6)
5. Artin Primitive Roots (0.409, sorry=9)

### Famous-hard caps (overclaim 防止)

Collatz 0.60 / Goldbach 0.55 / Twin Prime 0.45 / Riemann 0.40 / BSD 0.35 / Hodge 0.30 / P vs NP 0.30 / Navier-Stokes 0.25 / Yang-Mills 0.25

### 公開戦略 (確定)

| Phase | Tier |
|-------|------|
| Phase A (現在) | Tier 1 (GitHub public) + Tier 3 (Zenodo DOI weekly) |
| Phase B | Tier 2 追加 (GitHub Pages 静的サイト) |
| 将来 | Tier 4 (Cloudflare R2 + D1, 10 万問題超えたら) |

### 公開 repo

- `fc0web/rei-unsolved-problems` (Public, CC-BY 4.0 data + AGPL-3.0 code)
- **Local 構造作成済**, push は藤本さん承認後 (`public-repos/rei-unsolved-problems/`)

## 次セッション優先候補

1. **Agoh-Giuga Tier 1 実 attack** (formal-conjectures lake build + 3 sorry 埋め)
   - Strategy document: `data/open-problems/analysis/agoh-giuga-proof-strategies.md`
   - Expected: Paper 132 candidate
2. **Public repo 実 push** (`fc0web/rei-unsolved-problems` 実体化)
3. **Kourovka 1,861 件を Phase A-2 相当 Rei-typing 再実行** (現状は default タグのみ)
4. **Paper 132 候補**: "Narváez 2024 境界以降 Lean 4 初 cluster 解説" (Papers 127+128+131 統合)
5. **Phase C** (AIM workshops + Gromov 101 + Springer OPM 手動)
6. **HOL Light runtime fix** (Task #8)

## 未 commit (policy で放置)

- 206 ファイル自動生成 (daily-reports / eternal-evolution-log / scheduled_tasks.lock 等)
- `project_uncommitted_files_policy.md` 方針通り

## 公開した DOI / URL 新規 (本セッション)

- Paper 130: https://doi.org/10.5281/zenodo.19700758
- Paper 131: https://doi.org/10.5281/zenodo.19700858

## memory 新規 (本セッション)

- `project_open_problems_metadb_naming.md` — 正式名称確定
- `project_open_problems_storage_strategy.md` — 保管 hybrid 戦略
- `feedback_publish_channels_11.md` — 11 platform 標準
- `feedback_invention_duplicate_prevention.md` — 発明重複検出
- `project_paper130_published.md` — Paper 130 details
- `project_paper131_published.md` — Paper 131 details

## Peace Axiom #196

immutable — 本 session の 全成果物は平和利用のみ、軍事転用禁止