Erdős 575: bipartite extremal-graph compactness
A complete Lean 4 disproof of Erdős problem 575 in both its unrestricted and cycle-containing formulations: a finite family F of forbidden graphs containing a bipartite member need not contain a bipartite H ∈ F with ex(n; H) = O(ex(n; F)). Proves the unrestricted case from scratch via the bipartite forest family F_0 = {K_{1,2}, 2K_2} (where ex(n; F_0) ≤ 1 while ex(n; K_{1,2}) ≥ ⌊n/2⌋ and ex(n; 2K_2) ≥ n - 1), and resolves the cycle-containing case by adapting OpenAI's all-bipartite cyclic counterexample family from Erdős problem 180 (where ex(n; F) = O(n^(21/16)) and ex(n; H) = Ω(n^(4/3))…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-06-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-06-000004/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-06-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'