We derived three cases of Erdős #776, then found someone had already proved all of them

On 5 September 2026 we worked out three exact thresholds for Erdős–Trotter problem #776: n₀(5) = 14, n₀(6) = 16, n₀(11) = 27, with the boundary values g(14,5) = 10, g(16,6) = 12, g(27,11) = 23. The argument is the classical one: the cascade form of Kruskal–Katona turns "does an antichain with r sets on every level 2..n−2 exist?" into a downward integer recurrence, and at these three parameter pairs the rank-2 requirement exceeds the pair capacity by exactly one (92 > 91, 121 > 120, 352 > 351). Colex constructions cover every larger ground set up to He and Tang's cutoff, and their Proposition 4.1 covers the rest.

Then we did the literature check properly. The Erdős problems catalogue still says "open". Its proof-claims tab does not: M. Thiim posted claim #78 on 17 July 2026, proving n₀(r) = 2r+4 for 4 ≤ r ≤ 10 and 2r+5 for r ≥ 11 for every r ≥ 4, with a full Lean 4 formalization. Same method. His paper even contains our (27, 11) trace line for line. Our three values are special cases, seven weeks late.

Why publish

Three reasons, none of them priority:

  • It is an independent replication. Two groups, working without contact, produced the same obstruction
    • traces and the same 253-set family on 27 points. Claim #78 had no published independent check.
  • We built Thiim's Lean package from source. 1,064 targets, exit 0, on Lean 4.30.0; its axiom audit
    • reproduces exactly as documented (standard axioms plus three native_decide certificates, no sorry). As far as we know this is the first external build of that formalization.
  • Our three cases now compile as corollaries of its endpoint theorem, with the exact boundary values
    • added through explicit witnesses and a proved soundness lemma. 3.4 seconds, no sorry.

    Everything is in github.com/OV3RK177/erdos776-three-cases and mirrored on our proofs page. The release manifest is timestamped with OpenTimestamps, the same rail that anchors our DePIN data batches to Bitcoin every night.

    What we would tell anyone doing this

    Check the proof-claims tab, not the status badge. A problem stays "open" until a moderator reviews a claim; "open" is not "unclaimed". We got this wrong for about an hour and would have gotten it wrong for good if the check had stopped at the README.

    Credit where it belongs: the theorem is Thiim's; the bounds and the r = 2, 3 cases are He and Tang's (arXiv:2602.09803). Ours is the replication and the build.