Four self-contained notes on problems from the Erdős problems database, with the code needed to check every computational claim. Nothing here solves an open problem. Two of the notes are corrections or verifications that the database can act on directly; two are partial structural results.
The computational checks have commands for a clean checkout with bun and
python (see Reproducing). The workflow template is held in
ci-pending/; automated CI is not currently enabled in this repository.
| Problem | What the note contains | Status of the problem | |
|---|---|---|---|
| 617 | Erdős–Gyárfás balanced colourings | A product bound for edge-disjoint graphs, a reduction of the open r = 5 case, an independent machine verification of r = 3, and 13 symmetry classes excluded for r = 5 | still open for r ≥ 5 |
| 1221 | de Bruijn–Erdős points on a circle | The published statement is missing a factor of r: as written one question is false and another trivial | statement correction |
| 835 | Erdős–Rosenfeld / Johnson graph colouring | A two-line reproof of the Ma–Tang theorem from design divisibility and Kummer's theorem | still open for k = 16, 18, 22, … |
| 550 | tree vs complete multipartite Ramsey | Independent rebuild and audit of E. Li's Lean proof; the database recorded formal_status: unformalized |
solved by E. Li; formalisation now verified independently |
A further note on problem 617 proves that
any balanced five-colouring of K₂₆ has a colour-preserving automorphism group
of order 2^a 3^b, and restricts the possible permutations of order three.
It includes a Lean-checked finite circulant lemma. This is a partial obstruction;
the open case remains unresolved.
For pairwise edge-disjoint graphs C₁,…,C_r on n vertices and any i ≠ j,
n ≤ χ̄_f(C_i) · χ̄_f(C_j),
where χ̄_f is the fractional clique cover number (the fractional chromatic number
of the complement). Sample a clique from each of two optimal fractional clique
covers; the intersection is a clique in both graphs, so it has at most one vertex,
while its expected size is at least n/(w₁w₂).
On novelty, plainly: the integral case n ≤ θ(C_i)θ(C_j) is an immediate
injection — map each vertex to its pair of block labels — and is surely folklore.
The fractional strengthening follows by a standard sampling argument. I have not
found either stated in this context, but I would not be surprised to be shown a
reference, and I would like to be. See
notes/617.
Applied to Erdős problem 617 it gives: in a balanced r-colouring of K_n with
n > r², at most one colour class can have χ̄_f ≤ r. It also identifies r²
as an MDS-code barrier via Singleton's bound, attained exactly when an affine plane
of order r exists — which explains both the known construction and why the
r = 2 counterexample K₅ = C₅ ⊔ C₅ escapes.
Requires bun (no npm dependencies) and Python with pyyaml.
cd code/617
bun validate.js # machinery checks: AG(2,3) → K₉ and AG(2,5) → K₂₅ are balanced
bun claims.js # every structural claim in notes/617, machine-checked
bun drive_sym.js # symmetry-restricted complete searches on K₂₆ (with a K₂₅ control)
bun drive_prime.js # prime-order symmetries on K₂₆
N=10 R=3 bun exhaust.js # complete search: no balanced 3-colouring of K₁₀ (~3 min)
N=9 R=3 bun exhaust.js # the same code finds one on K₉
SEED=1 ITERS=30000000 RESTARTS=6 bun sa.js # annealing on K₂₆
N=25 R=5 ITERS=3000000 RESTARTS=6 bun sa.js # the control, on K₂₅Every colouring the code reports as balanced is independently rechecked by brute
force over all C(n,6) six-subsets, so a bug in the clever counting cannot
manufacture a false positive.
For problem 550 (needs Lean 4.28.0 and a few GB for Mathlib):
git clone https://github.com/ericlisg/erdos550-lean && cd erdos550-lean
git checkout 6624ede70821f095eaee49865448af4e4f8c421c
lake exe cache get && lake build # 8160 jobs
lake env lean MainAudit.lean # axioms: propext, Classical.choice, Quot.sound
cp ../erdos-notes/code/550/IndependentAudit.lean . && lake env lean IndependentAudit.lean
python ../erdos-notes/code/550/audit.py --json source-audit.json
python ../erdos-notes/code/550/test_audit.pyIf any of this is known, wrong, or badly attributed, please open an issue — that is more useful to me than silence. The claims are stated so that each is individually checkable.
This work was carried out with Claude (Anthropic). The proofs are short and self-contained and are meant to be read and checked; every numerical claim comes from a run recorded here, and the positive ones are confirmed by an independent brute force. Any error is mine.
MIT for the code, CC BY 4.0 for the notes.