---
name: Paper 132 公開 — 10/11 platform 完了 (Zenodo 遅延)
description: Paper 132 (5 Rei candidates roadmap) を 10 platform に公開。Zenodo は 2026-04-23 に infra outage (503) で retry 待ち。Part F で Paper 130 ingestion bug を公式告白した初 roadmap paper。
type: project
originSessionId: 2812f631-04af-4dd8-a8cd-4f872e1e1383
---
# Paper 132 公開記録

## 基本情報
- **Title**: Five Classical Open Problems as Rei-AIOS's Next Lean 4 Deep-Dive Candidates: Sunflower, Hadwiger-Nelson, Happy Ending, Herzog-Schönheim, Wolstenholme
- **Type**: reconnaissance (roadmap) paper — 新定理証明なし
- **File**: `papers/paper-132-five-rei-candidates.md` (311 行, 11 Parts A-K)
- **公開日**: 2026-04-23
- **commits**: `78f28c2` (draft) + `d8d1af6` (publish state) + `239087a` (metadata fix 前提)

## 公開プラットフォーム (10/11 成功)

| # | Platform | URL |
|---|----------|-----|
| 1 | Internet Archive | archive.org/details/rei-aios-paper-132-1776926783022 |
| 2 | Harvard Dataverse | doi.org/10.7910/DVN/KC56RY |
| 3 | dev.to | dev.to/fc0web/five-classical-open-problems-...-paper-132-4dp4 |
| 4 | Hatena Blog | fcwebfujimoto.hatenablog.com/entry/2026/04/23/155112 |
| 5 | HackMD | hackmd.io/@zCUv2P2UQHGmAOJFPLL_-A/rJyObHD6Ze |
| 6 | Notion | notion.so/Paper-132-... |
| 7 | Mastodon | mathstodon.xyz/@Fujimoto/116452695896220516 |
| 8 | livedoor | fcwebfujimoto.livedoor.blog/archives/12903953.html |
| 9 | Scrapbox | scrapbox.io/rei-aios/Paper 132 — ... |
| 10 | Zenn | zenn.dev/fujimoto/articles/paper-132-five-rei-candidates |
| 11 | ✅ Zenodo | doi.org/10.5281/zenodo.19704359 (retry 成功) |

**Zenodo retry note**: 2026-04-23 06:30 UTC から ~30 min の Zenodo 計画メンテで初回 FAIL。07:02 UTC に復旧確認後、`scripts/publish-paper-132-zenodo-only.ts` で retry 成功。DOI `10.5281/zenodo.19704359` 取得。

## Paper 132 の 5 候補 + 残 sorry

| 問題 | 実 sorry | Lean4 file | 近年進展 |
|------|---------:|-----------|---------|
| Erdős-Rado Sunflower | 2 | ErdosProblems/20.lean | Alweiss-Lovett-Wu-Zhang 2021 |
| Hadwiger-Nelson | 5 | ErdosProblems/508.lean | de Grey 2018 (χ≥5) |
| Happy Ending | 7 | ErdosProblems/107.lean | Suk 2017 / HMPT 2020 |
| Herzog-Schönheim | 4 | ErdosProblems/274.lean | Mirsky-Newman abelian |
| Wolstenholme 残 | 5 (was 6) | Wikipedia/WolstenholmePrime.lean | Linhares 2026-04-14 |
| **合計** | **23** | — | — |

## Paper 133 以降のターゲット (Tier 1-2 closure, 2026-05-15 target)

1. Hadwiger-Nelson χ ≥ 4 (Moser-Spindel 7-vertex graph, native_decide)
2. Happy Ending f(3) = 3 (基本 AffineIndependent + convex hull)
3. Wolstenholme specific primes 16843 / 2124679 (Nat.ModEq + Nat.choose)
4. (延伸) Herzog-Schönheim abelian case Mirsky-Newman

## 4+7 要素構造 v2 遵守の特記事項

- **Part A VERIFIED 欄は意図的に空** (roadmap paper なので新定理無し honesty)
- **Part F で Paper 130 ingestion bug を公式告白** (defaulted-zero ≠ counted-zero)
- **Part J**: NEITHER-tag 項目を明示 parking (Herzog-Schönheim 一般 / Linhares engine 内部)
- **Part K**: "counted-zero vs defaulted-zero" distinction を D-FUMT₈ ZERO vs NEITHER にマッピング

## 関連 commit chain
- `239087a` (C) 4 Wikipedia JSON metadata 修正 (sorry 0→2/5/7/4, p 0.95→0.55-0.65)
- `78f28c2` Paper 132 draft 起草
- `d8d1af6` 10 platform publish

## Paper 127-131 cluster 延長
- 127 (Schur/EGZ) + 128 (Davenport) + 131 (Bipartite Ramsey) = 3 件 closed small-value 前進
- **132 = 5 件 open roadmap 宣言**
- 133+ = Tier 1-2 sorry closure