The board / graph theory / #613
Erdős Problem #613
DISPROVED LEANdatabase updated 2025-11-04
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
**Erdős Problem 613:** Let \(n \geq 3\) and \(G\) be a graph with \(\binom{2n+1}{2} - \binom{n}{2} - 1\) edges. Must \(G\) be the union of a bipartite graph and a graph with maximum degree less than \(n\)?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/613.Prizenone
Topicsgraph theory, ramsey
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/613
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.