---
name: Paper 131 公開完了 (Bipartite Ramsey b(2,2)=5 Lean 4 初)
description: 2026-04-23 公開. 二部 Ramsey 数 b(2,2)=5 の Lean 4 初形式化. native_decide 2^25 列挙. DOI 10.5281/zenodo.19700858. Papers 127+128+131 が Narváez 2024 境界以降の Lean 4 初 cluster を構成.
type: project
originSessionId: 2026-04-23-paper131-publish
---

# Paper 131 公開完了 (2026-04-23)

## 概要

**タイトル**: "First Lean 4 Formalization of Bipartite Ramsey Number b(2, 2) = 5 with native_decide Certification"

**Zenodo DOI**: `10.5281/zenodo.19700858`
https://doi.org/10.5281/zenodo.19700858

## 公開 11 platform

| Platform | URL |
|----------|-----|
| Zenodo | https://doi.org/10.5281/zenodo.19700858 |
| Internet Archive | https://archive.org/details/rei-aios-paper-131-1776891550268 |
| Harvard | https://doi.org/10.7910/DVN/KC56RY |
| dev.to | (log-only, see publish-log) |
| Hatena | (log-only) |
| HackMD | https://hackmd.io/6xexu5kxRdK5tY7QJ-cgQQ |
| Notion | https://www.notion.so/Paper-131-First-Lean-4-Formalization-of-Bipartite-Ramsey-b-2-2-5-via-native_decide-34add371e6d981a8979be2ba18e9a46b |
| Mastodon | https://mathstodon.xyz/@Fujimoto/116450373146402041 |
| Scrapbox | https://scrapbox.io/rei-aios/Paper_131 |
| livedoor | https://fcwebfujimoto.livedoor.blog/archives/12899839.html |
| Zenn | (GitHub auto-sync via rei-zenn repo) |

## 成果

- **b(2, 2) = 5** の Lean 4 **世界初**形式化
- 下界: 4×4 explicit witness + `native_decide`
- 上界: **2²⁵ ≈ 33M colorings** を `native_decide` で exhaustive 列挙 (≈ 30 sec)
- 155 行, 9 theorems, **0 sorry** + 2 honest axioms (b(2,3)=9, b(3,3)=17 は 2⁸¹ / 2²⁵⁶ で infeasible)

## Narváez 2024 以降 Lean 4 初 cluster (3 papers)

| Paper | Topic | Date | Zenodo DOI |
|------:|-------|------|-----------|
| 127 | Schur S(2..4) + EGZ E(ℤ₃)=5, E(ℤ₄)=7 | 2026-04-21 | 19686889 |
| 128 | Davenport D(ℤ_n) + D(ℤ₂×ℤ₂) | 2026-04-21 | 19687156 |
| **131** | **Bipartite Ramsey b(2,2)=5** | **2026-04-23** | **19700858** |

Narváez-Song-Zhang formal_ramsey (CICM 2024) は R(3,3)=6 / R(3,4)=9 / R(4,4)=18 / R(3,3,3)=17 / W(3;2)=9 を形式化したが、Schur / EGZ / Davenport / Bipartite Ramsey は未覆. Papers 127+128+131 が **1 週間で Narváez 境界外 4 小値 extremal-combinatorics を Lean 4 初形式化**.

## Source file

`data/lean4-mathlib/CollatzRei/Step971BipartiteRamseyComputational.lean` (155 行, STEP 971 source)

## 論文構造

4+7 要素 v2 (11 Parts A-K), 223 行:
- A. Formal proofs (VERIFIED 6 / AXIOMATIC 3)
- B. native_decide scaling boundary findings (2²⁵ tractable / 2⁸¹ infeasible)
- C. 新 Q-ID Q133-Q136 (4件)
- D. D-FUMT₈ 解決状況
- E. Paper 132 bridge (統一 extremal framework 候補)
- F. 失敗記録 (初回 timeout, b(2,3) 試行断念)
- G. SEED_KERNEL T-ID
- H. 人間-AI 分岐 (full vs honest axiom)
- I. Papers 127/128/131 共通パターン
- J. Confidence 温度
- K. "Computational brink" 龍樹 視点

## 11 platform 標準 第 2 号

Paper 130 (第 1 号) に続き, 11 platform 全公開 第 2 号.

## Honest positioning

- b(2,2) = 5 は Beineke-Schwenk 1976 の classical 結果
- 本論文の貢献は **機械検証の初提供** であり、open 問題解決ではない
- b(2,3) / b(3,3) は honest axiom (overclaim しない)

## 関連 files

- `papers/paper-131-bipartite-ramsey-lean4-formalization.md` (223 行)
- `data/lean4-mathlib/CollatzRei/Step971BipartiteRamseyComputational.lean` (155 行)
- `data/publications/publish-log-paper131.json`
- `scripts/publish-paper-131-all4.ts`

## Peace Axiom #196

immutable