---
name: Paper 127 Published
description: Paper 127 (Lean 4 Schur S(2..4) + EGZ E(Z3), E(Z4) formalization) published to all 11 platforms on 2026-04-21
type: project
originSessionId: ea0eb1f8-f659-4461-a674-df3f98cba941
---
**Paper 127 公開完了 (2026-04-21 JST 夜 / 2026-04-22 06:55)**

Zenodo DOI: **10.5281/zenodo.19686889**
Title: First Lean 4 Computational Formalization of Schur Numbers S(2), S(3), S(4) and Small-Value EGZ Witnesses E(ℤ₃), E(ℤ₄) — native_decide Certificates

**Why:** Template v3 (VERIFIED / EMPIRICAL / AXIOMATIC 三分離) の inaugural paper。Narváez CICM 2024 先行研究を回避し、Schur 5件 + EGZ 2件 = 合計 5 novel Lean 4 contribution (S(2)=4, S(3)≥13, S(4)≥44, E(ℤ₃)=5, E(ℤ₄)=7) に claim を絞った。

**How to apply:** 今後の Ramsey/Schur/EGZ 関連論文では Narváez 2024 (`cruisesong7/formal_ramsey`) 既存範囲を必ず除外。Mathlib の `Int.erdos_ginzburg_ziv` + `ZMod.erdos_ginzburg_ziv` は一般形のみで小値 witness なしのため、small-value EGZ は依然 novel。

## 11 platform URLs

| Ch | URL |
|----|-----|
| Zenodo | https://doi.org/10.5281/zenodo.19686889 |
| Internet Archive | https://archive.org/details/rei-aios-paper-127-1776808478996 |
| Harvard Dataverse | https://doi.org/10.7910/DVN/KC56RY |
| dev.to | https://dev.to/fc0web/first-lean-4-computational-formalization-of-schur-numbers-s2-s3-s4-and-small-value-egz-3pn9 |
| Hatena Blog | https://fcwebfujimoto.hatenablog.com/entry/2026/04/22/065514 |
| HackMD | https://hackmd.io/@zCUv2P2UQHGmAOJFPLL_-A/SkArzdSpbe |
| Notion | https://www.notion.so/Paper-127-First-Lean-4-Formalization-of-Schur-S-2-4-Small-Value-EGZ-349dd371e6d98184928ac1418f64360b |
| livedoor | https://fcwebfujimoto.livedoor.blog/archives/12887467.html |
| Scrapbox | https://scrapbox.io/rei-aios/Paper%20127%20—%20First%20Lean%204%20Computational%20Formalization%20of%20Schur%20Numbers%20S(2)%2C%20S(3)%2C%20S(4)%20and%20Small-Value%20EGZ%20Witnesses%20E(ℤ₃)%2C%20E(ℤ₄)%3A%20native_decide%20Certificates |
| Zenn | via rei-zenn repo commit 61e8951 (articles/paper-127-schur-egz-lean4-formalization.md) |
| Mastodon | https://mathstodon.xyz/@Fujimoto/116444929463214016 |

## Commits
- rei-aios 890d362 — Paper 127 artifacts (paper + 6 publish META)
- rei-aios 7f4cab3 — Zenn converter META for Paper 127
- rei-zenn 61e8951 — Paper 127 Zenn article

## Content summary
- Lean file: `data/lean4-mathlib/CollatzRei/Step968RamseyComputational.lean` (exit 0 verified)
- 11 theorems = 5 novel (Schur 3 + EGZ 2) + 6 auxiliary (R(3,3)=6 etc, re-derived — not claimed novel)
- 3 axioms (schur_S3_upper, schur_S4_upper, vdw_W42_upper) — honest axiom principle
- W(3;2)=9 explicitly acknowledged as "subsumed by Narváez 2024, included as independent re-derivation"