The board / graph theory / #583
Erdős Problem #583
FALSIFIABLEdatabase updated 2025-08-31
Still open — but if it is false, a finite counterexample exists, so a computer search could in principle disprove it. A search can't prove it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A subgraph `H` of `G` is a path subgraph if it is the subgraph traced out by a path in `G`, i.e. a walk with no repeated vertices.
Every connected graph on \(n\) vertices can be partitioned into at most \(\lceil n/2\rceil\) edge-disjoint paths. A problem of Erdős and Gallai.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open. The authoritative wording is on erdosproblems.com/583.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/583
Attempts
submit one →Read our working report →
Exact exhaustive path-number distributions and the stronger odd-semi-clique classification are verified for every connected simple graph on at most 8 vertices; no uniform proof or counterexample is ob
PARTIAL