Erdős Problems 552 and 85 — Reproducibility Archive

Erdős Problems 552 and 85 · October 7, 2026

Scope. A Lean 4 proof of Chen's bound (1997), an equivalence for Problem 85, and three record corrections. Problems 552 and 85 remain open.

Replay

python -m pip install networkx z3-solver
python battery_552.py
python f85_from_ramsey.py
python witness_f85.py 15 4

# Lean 4 proof (in lean/)
lake exe cache get
lake build

Files

File	Purpose
lean/Erdos/Erdos552.lean · Ramsey.lean	Lean 4 proof of Chen's bound; the project is in `lean/` and at agnt-gg/erdos-lean
battery_552.py · output	Brute force over all graphs on at most 7 vertices
f85_from_ramsey.py · output	f(n) for Problem 85 from OEIS A006672
witness_f85.py · graph · output	15-vertex C4-free graph of minimum degree 4
claim-ledger.json	Claim-by-claim evidence map
SHA256SUMS.txt	SHA-256 integrity ledger