Erdős Problem 1033: a butterfly blow-up beating 2(√3 - 1)
Source: github.com/ukniusanqian-alt/erdos654-lean/tree/3146ec1b4c12…
Lean 4 / Mathlib proof that the Bollobás–Erdős question of Erdős Problem 1033 has a negative answer. For every t ≥ 1 an explicit blow-up of the butterfly graph (two triangles sharing a vertex) on n = 668t vertices has 111561t² > n²/4 edges, and every triangle has degree sum exactly 978t, while 978/668 < 2(√3 - 1). Hence it is false that every graph on n vertices with more than n²/4 edges has a triangle with degree sum at least (2(√3 - 1) - o(1))n.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-03-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000006/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-11-03-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'