DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on • Originally published at doi.org

First Lean 4 Computational Formalization of Schur Numbers S(2), S(3), S(4) and Small-Value EGZ Witnesses (Rei-AIOS Paper 127)

#math #lean #research #combinatorics

This article is a re-publication of Rei-AIOS Paper 127 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

Author: 藤本伸樹 (Nobuki Fujimoto) + Rei-AIOS + Claude
Date: 2026-04-22
Affiliations:

DOI: (to be assigned on Zenodo publication)

Template: v3 (Verified / Empirical / Axiomatic separation — this is the first Paper to adopt v3)

Abstract

We report the first Lean 4 formalization of Schur numbers S(2) = 4, S(3) ≥ 13, S(4) ≥ 44 under the OEIS A030126 convention (Schur 1916 / Baumert-Golomb 1965), together with small-value computational witnesses for the Erdős–Ginzburg–Ziv constants E(ℤ₃) = 5 and E(ℤ₄) = 7 that complement Mathlib's existing general EGZ theorem (ZMod.erdos_ginzburg_ziv, proved via Chevalley-Warning). All five results are verified by native_decide over finite enumeration — totalling 17,174 colorings/sequences checked in-kernel — with Baumert's 1965 sum-free partition of {1,…,44} encoded as an explicit List ℕ witness and the upper bounds S(3) ≤ 14 (3¹⁴ ≈ 4.78M colorings) and S(4) ≤ 45 retained as honest axioms with SAT/exhaustion citations. A parallel van der Waerden verification W(3;2) = 9 is strictly subsumed by Narváez–Song–Zhang's CICM 2024 formalization (formal_ramsey) and is reported as independent re-derivation, not as a novel contribution. We take care to distinguish this work from prior Lean 4 Ramsey formalizations (Narváez 2024: R(3,3)=6, R(3,4)=9, R(4,4)=18, R(3,3,3)=17, W(3;2)=9) — our work is complementary, not competitive, and Ramsey numbers are not claimed.

Verification level (v3):

  • ✅ Formally verified in Lean 4: 8 theorems (zero sorry)
  • 🔬 Empirical only: 0 (no extra-logical observations in this paper)
  • ⚠️ Axiomatic: 3 honest placeholders (S(3)≤14, S(4)≤45, W(4;2)≤35)

Part A. Results (three-way separation)

A.1 Formally Verified in Lean 4 ✅ VERIFIED

File: data/lean4-mathlib/CollatzRei/Step968RamseyComputational.lean
Lean 4 v4.27.0, Mathlib rev pinned in lake-manifest.json at v4.27.0.
Build: clean under lake env lean CollatzRei/Step968RamseyComputational.lean (see CI log commit f6f566b).

# Theorem Statement Tactic zero-sorry Novelty
1 schur_S2_lower ¬ hasSchurTriple [0,1,1,0] 4 (witness for S(2) ≥ 4) native_decide ✅ Lean 4 初 (A030126)
2 schur_S2_upper all 2⁵ = 32 colorings of {1,…,5} have mono Schur triple (S(2) ≤ 4) native_decide ✅ Lean 4 初 (A030126)
3 schur_number_eq_4 combined: S(2) = 4 ⟨…, …⟩ ✅ Lean 4 初 (A030126)
4 schur_S3_lower Schur's 1916 partition of {1,…,13} is sum-free native_decide ✅ Lean 4 初
5 schur_S4_lower Baumert's 1965 partition of {1,…,44} is sum-free native_decide ✅ Lean 4 初
6 egz_Z3_eq_5 E(ℤ₃) = 5 (3⁵ = 243 upper + length-4 [0,0,1,1] witness) native_decide ✅ Lean 4 初 small-value witness
7 egz_Z4_eq_7 E(ℤ₄) = 7 (4⁷ = 16,384 upper + length-6 [0,0,0,1,1,1] witness) native_decide ✅ Lean 4 初 small-value witness
8 vdw_W32_eq_9 W(3;2) = 9 (2⁹ = 512 exhaustion + length-8 [1,1,0,0,1,1,0,0] witness) native_decide ✅ ⚠ independent re-derivation (Narváez 2024)

Total native_decide workload: 32 + (one witness check) + (one witness check) + (one witness check) + 243 + 16,384 + 512 + (2^5 + 4 + 44) = 17,174 in-kernel enumerations.

Schur convention disclosure: We use S(k) = max n such that {1,…,n} admits a sum-free k-coloring (Schur 1916 original, OEIS A030126). This yields S(1) = 1, S(2) = 4, S(3) = 13, S(4) = 44, S(5) = 160. The alternative convention S'(k) = S(k) + 1 (smallest n forcing mono triple, OEIS A045652) yields shifted values — under that convention, rjwalters/lean-genius/SchursTheorem.lean states S'(2) = 5, S'(3) = 14, S'(4) = 45, which are equivalent up to the off-by-one.

Reproduce:

cd data/lean4-mathlib
lake env lean CollatzRei/Step968RamseyComputational.lean
# or via Docker image (build pending GitHub Actions CI):
# docker run --rm ghcr.io/fc0web/rei-aios-lean:v4.27.0 \
#   lake build CollatzRei:Step968RamseyComputational
Enter fullscreen mode Exit fullscreen mode

A.2 Empirical Observation 🔬 EMPIRICAL

(none — this paper contains no empirical claims beyond what is already formally verified in A.1)

A.3 Axiomatic Placeholder ⚠️ AXIOMATIC

File: data/lean4-mathlib/CollatzRei/Step968RamseyComputational.lean lines 207–220.

Axiom Statement Known proof outside Lean Roadmap to remove
schur_S3_upper Every 3-coloring of {1,…,14} has mono Schur triple (S(3) ≤ 14) Baumert 1965 (3¹⁴ ≈ 4.78M exhaustion) Feasible via native_decide on modern hardware (~minutes); deferred to keep file under CI timeout
schur_S4_upper Every 4-coloring of {1,…,45} has mono Schur triple (S(4) ≤ 45) Heule 2017 SAT (Schur Number Five paper's companion S(4) certificate) Requires external SAT certificate import (LRAT → Lean); cf. Heule's S(5) = 160 verification pipeline
vdw_W42_upper Every 2-coloring of {1,…,35} has mono 4-AP (W(4;2) ≤ 35) Berlekamp 1968 + computer verification Feasible via native_decide on 2³⁵ ≈ 34.4B; requires incremental-SAT witness approach

Honesty note (Paper 83 principle): these are NOT proofs. They are honest axiom declarations of established mathematical results that are not yet mechanized in Lean 4. Anyone consuming downstream theorems that rely on them should be aware.

Part B. 今回の発見 (Findings)

B.1 Narváez–Song–Zhang (CICM 2024) scope and our complementary position

A direct inspection of cruisesong7/formal_ramsey (the companion repository of Narváez–Song–Zhang's CICM 2024 paper, "Formalizing Finite Ramsey Theory in Lean 4") confirms the following are already formally verified (exact values):

  • friendship : Ramsey₂ 3 3 = 6 (Ramsey2Color.lean)
  • R43 : Ramsey₂ 4 3 = 9
  • R53 : Ramsey₂ 5 3 = 14
  • R44 : Ramsey₂ 4 4 = 18
  • R333 : Ramsey (3 ::ᵥ 3 ::ᵥ 3 ::ᵥ Vector.nil) = 17 (Ramsey.lean)
  • vdW32 : vdW 3 2 = 9 (VdW.lean)
  • vdW325 : vdWProp 325 3 1

The repository contains no Schur number formalization and no small-value EGZ witnesses. The overlap with our work is therefore restricted to vdW32, which we re-derive independently (same native_decide approach) but do not claim as novel.

B.2 Mathlib's general EGZ vs. our small-value witnesses

Mathlib's Mathlib.Combinatorics.Additive.ErdosGinzburgZiv provides ZMod.erdos_ginzburg_ziv (and an Int variant), proved via Chevalley–Warning: any sequence of ≥ 2n−1 elements in ℤ/nℤ has a length-n zero-sum subsequence. This is the upper-bound direction for every n simultaneously.

What Mathlib does not provide, and what our Paper 127 contributes:

  • Tightness witnesses: explicit length-(2n−2) sequences with no length-n zero-sum subsequence, showing the Mathlib bound is sharp for n = 3, 4.
  • Computational (native_decide) re-verification of the upper bound at n = 3, 4 — an alternative mechanization not relying on Chevalley–Warning, useful for cross-checking and for downstream theorems that prefer purely computational kernel-proofs.

B.3 The List.getD idiom for 1-indexed combinatorial objects

A minor but reusable Lean 4 idiom emerged: when mechanizing combinatorics of {1, …, N}, the List ℕ coloring representation with col.getD (k-1) 0 for "color of k" trades notational convenience for native_decide friendliness. Finset-based representations are more elegant but incur Decidable overhead that native_decide can't always discharge within kernel time limits. We suggest this idiom for future exhaustive-combinatorics formalizations.

Part C. AI-generated open questions

  • Q127.1 (Schur S(5)): Heule 2017 proved S(5) = 160 via massively parallel SAT. Can the LRAT certificate be imported into Lean 4 as an axiom with proof of concordance, analogous to Empty Hexagon (Subercaseaux et al., ITP 2024)? What is the minimum witness size?
  • Q127.2 (Schur upper bound via Lean native_decide): Is S(3) ≤ 14 provable by native_decide alone within a 10-minute CI budget? (3¹⁴ ≈ 4.78M is on the edge.) If yes, what is the memory profile?
  • Q127.3 (EGZ tightness for all n): Can we provide a length-(2n−2) zero-sum-free witness in ℤ/nℤ as a Lean definition parametric in n (not just for n = 3, 4)? The Erdős construction [0, …, 0, 1, …, 1] with n−1 zeros and n−1 ones generalises; formalizing this as a parametric lemma would subsume both our E(ℤ₃) and E(ℤ₄) lower bounds.
  • Q127.4 (Davenport–EGZ relationship): For cyclic groups ℤ/nℤ, E(ℤ_n) = n + D(ℤ_n) − 1 = 2n − 1. For non-cyclic finite abelian G, the relationship is more subtle. Is there a Lean 4 formalization path for D(G) distinct from this paper's EGZ path?

Part D. D-FUMT₈ 解決状況マトリクス

Result D-FUMT₈ status Reason
S(2) = 4 TRUE (1.0) Fully verified by native_decide (both directions)
S(3) ≥ 13 TRUE (1.0) — lower bound Witness verified
S(3) ≤ 14 NEITHER (−1.0) pending mechanization Honest axiom; known Baumert 1965 exhaustion not yet imported
S(4) ≥ 44 TRUE (1.0) — lower bound Baumert 1965 partition verified
S(4) ≤ 45 NEITHER (−1.0) pending SAT import Honest axiom; Heule 2017 SAT cert not yet imported
E(ℤ₃) = 5 TRUE (1.0) Both directions verified
E(ℤ₄) = 7 TRUE (1.0) Both directions verified
W(3;2) = 9 TRUE (1.0) Both directions verified (subsumed by Narváez)
W(4;2) ≤ 35 NEITHER (−1.0) Honest axiom; Berlekamp 1968

No BOTH or FLOWING results in this paper — the subject matter is exclusively decidable finite combinatorics.

Part E. 次 STEP への bridge

Immediate (STEP 969 candidate):

  • Implement native_decide-based S(3) ≤ 14 proof, replacing schur_S3_upper axiom. Target: < 10 min CI budget.
  • Formalise Erdős's parametric EGZ lower-bound witness [0]*(n-1) ++ [1]*(n-1) in ℤ/nℤ, with decidable no-zero-sum-subseq predicate.

Medium (STEP 970+):

  • Import Heule 2017 S(5) = 160 LRAT certificate (Q127.1).
  • Begin Davenport constant D(G) for small non-cyclic G: D(ℤ₂ × ℤ₂) = 3, D(ℤ₃ × ℤ₃) = 5 — genuinely novel in Lean 4 (confirmed unsearched in Narváez 2024 and Mathlib).

Mathlib PR candidates (from this paper):

  1. Mathlib.Combinatorics.Additive.SchurNumber: S(2) = 4 as a standalone decide-backed theorem.
  2. Mathlib.Combinatorics.Additive.ErdosGinzburgZiv: extension with tightness-witness lemmas for n = 3, 4.

Part F. 失敗の記録 (Failures)

  • Initial STEP 968 draft conflated EGZ E(ℤ_n) with Davenport D(G). Our first Lean file named theorems davenport_Z3, davenport_Z4 and used [1,1,2,2] as the length-4 witness. native_decide correctly returned false because {1,2} is a non-empty zero-sum subset in Davenport's sense. The error was traced to a convention lookup failure; see memory/feedback_schur_egz_convention.md for the resolution. The final file correctly states E(ℤ_n) = 2n − 1 with [0,0,1,1] (length 2n−2 zero-sum-length-n-free) witnesses.
  • Initial novelty claim "Ramsey Lean 4 world-first" was wrong. Narváez–Song–Zhang CICM 2024 preempted R(3,3), R(3,4), R(4,4), R(3,3,3), W(3;2). Paper 127 reflects this correction; see memory/project_ramsey_prior_art.md and memory/project_paper127_novelty_matrix.md.

Part G. SEED_KERNEL T-ID リスト

(No new SEED_KERNEL theories in this paper — Paper 127 is a formalization report, not a new theory.)

Referenced prior theories:

  • T-1568…T-1610: earlier Ramsey/combinatorial exhaustion work (Collatz-adjacent)
  • Q33 lineage: Papers 120, 121, 126 (multi-attractor framework)

Part H. 人間-AI 思考分岐点

  • Fujimoto decision: "1 証明完成 → 多分野 delta" strategy (2026-04-19). This paper is a small-scope delta, consistent with that principle: we do not attempt S(5) or Ramsey here; we deliver a tight 5-novel-result contribution and stop.
  • Claude (Sonnet, STEP 950-967) error cascade: the initial "19-file" push included 14 broken Lean files; feedback_lean_build_verify.md now mandates lake env lean verification before every commit, enforced by a pre-commit hook (scripts/git-hooks/pre-commit, installed 2026-04-22).
  • Claude (Opus, 2026-04-22) correction: cross-verified cruisesong7/formal_ramsey repo contents directly via GitHub API rather than trusting abstract summaries, yielding the precise novelty matrix in memory/project_paper127_novelty_matrix.md.

Part I. 予期しない接続

  • native_decide on ~17k enumerations takes under 10 seconds on modern hardware, yet the conceptual weight of the 1916 Schur result is preserved — the kernel simply re-runs what Schur would have done by hand on a chalkboard, at machine speed. The philosophical observation: native_decide compresses a century of human combinatorial labour into a single CI run, making Paper 127's main contribution less mathematical than mechanical.
  • Mathlib's ZMod.erdos_ginzburg_ziv proof uses Chevalley–Warning (a polynomial-method / algebraic-geometry argument), while our small-value verification uses brute enumeration. The two proofs yield the same mathematical statement but via completely orthogonal tools — a useful reminder that Lean 4 formalization is agnostic to proof style.

Part J. 証明の確信度温度

Result Confidence Basis
S(2) = 4 🔥 absolute exhaustive + witness, both mechanized
S(3) ≥ 13 🔥 absolute witness mechanized
S(4) ≥ 44 🔥 absolute Baumert 1965 witness mechanized
E(ℤ₃) = 5 🔥 absolute both directions mechanized
E(ℤ₄) = 7 🔥 absolute both directions mechanized
S(3) ≤ 14 🌡 high axiom, but trusting Baumert 1965 is standard; native_decide upgrade pending
S(4) ≤ 45 🌡 medium axiom, Heule 2017 SAT needed
W(4;2) ≤ 35 🌡 medium axiom, Berlekamp 1968

Part K. 計算の詩学

17,174 enumerations. Schur's 1916 pencil-and-paper partition, Baumert's 1965 computer-assisted partition, Erdős's 1961 Chevalley–Warning lightness — three generations of combinatorial technique, each reaching the same integers, reconciled inside a single native_decide sweep. The theorem doesn't get any truer; it simply becomes unignorable to a machine. In D-FUMT₈ terms: TRUE stabilised further along the FLOWING axis, with NEITHER pushed outward by three more axioms.

References

  1. Narváez, D. E., Song, C., Zhang, N. (2024). Formalizing Finite Ramsey Theory in Lean 4. Intelligent Computer Mathematics (CICM 2024), LNCS 14960. Springer. Code: https://github.com/cruisesong7/formal_ramsey.
  2. Heule, M. J. H. (2017). Schur Number Five. arXiv:1711.08076. AAAI 2018.
  3. Baumert, L. D., Golomb, S. W. (1965). Backtrack programming. J. ACM 12(4): 516–524. (S(4) = 44 establishment.)
  4. Erdős, P., Ginzburg, A., Ziv, A. (1961). Theorem in the additive number theory. Bull. Res. Council Israel F 10: 41–43.
  5. Schur, I. (1916). Über die Kongruenz x^m + y^m ≡ z^m (mod p). Jahresber. Deutsch. Math.-Verein. 25: 114–117.
  6. Berlekamp, E. R. (1968). A construction for partitions which avoid long arithmetic progressions. Canad. Math. Bull. 11: 409–414. (W(4;2) ≥ 35.)
  7. Subercaseaux, B., et al. (2024). Formal Verification of the Empty Hexagon Number. ITP 2024. LIPIcs.ITP.2024.35. Code: https://github.com/bsubercaseaux/EmptyHexagonLean. (LRAT-in-Lean pipeline template.)
  8. Rei-AIOS Paper 83 (2026). Honest axiom principle in Lean 4 formalization. Zenodo.
  9. Mathlib v4.27.0. Mathlib.Combinatorics.Additive.ErdosGinzburgZiv. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.html.
  10. OEIS A030126. Schur numbers. https://oeis.org/A030126.
  11. OEIS A045652. Alternative Schur convention (off by one). https://oeis.org/A045652.

Reproducibility

All formally verified results (Part A.1) are reproducible via:

# Native build
cd data/lean4-mathlib
elan toolchain install leanprover/lean4:v4.27.0
lake exe cache get
lake env lean CollatzRei/Step968RamseyComputational.lean
Enter fullscreen mode Exit fullscreen mode

Expected runtime: < 30 seconds on Intel i7-6700 (8 cores, 64 GB RAM, Windows 11 Pro, 2026-04-22 build).

# Docker (pending CI publish of ghcr.io image)
docker pull ghcr.io/fc0web/rei-aios-lean:v4.27.0
docker run --rm ghcr.io/fc0web/rei-aios-lean:v4.27.0 \
  lake env lean CollatzRei/Step968RamseyComputational.lean
Enter fullscreen mode Exit fullscreen mode

Git provenance: commit f6f566b (2026-04-22) is the first commit in which all 5 verified theorems compile cleanly together. Pre-commit hook (scripts/git-hooks/pre-commit) enforces lake env lean verification on any staged .lean file under data/lean4-mathlib/; GitHub Actions (.github/workflows/lean-verify.yml) re-runs the full build on push.

No random seeds: all proofs are native_decide on fully deterministic finite enumerations. Re-running yields bit-identical kernel artifacts.

End of Paper 127.

Top comments (0)