Problems/Erdos-Gallai Theorem

Erdos-Gallai Theorem

Graph TheorySOLVED
Year
1960
Difficulty
*****
Solved by
Paul Erdos & Tibor Gallai (1960)

Statement

Characterizes which integer sequences are degree sequences of simple graphs.

∑i=1kdi≤k(k−1)+∑i=k+1nmin⁡(di,k)\sum_{i=1}^{k} d_i \leq k(k-1) + \sum_{i=k+1}^{n} \min(d_i, k)

About this Problem

Fundamental in graph theory and network science. Determines graph realizability from degree information alone.

About the Lean 4 Prover

Lean 4 is a theorem prover and programming language. When a proof compiles in Lean, it is mathematically certain to be correct — the type checker verifies every logical step. This is the gold standard for formal verification.

Our platform uses fal.ai serverless compute to run Lean verification, and Gemini to generate proof strategies that are then formally checked. ShinkaEvolve provides the evolutionary backbone for automated mathematical discovery.

Mathematical Art

Generate a unique AI illustration of this problem using fal.ai FLUX.

Connected Constellations

ProbabilitySOLVED
Erdos-Renyi Random Graph Model
Graph TheorySOLVED
Erdos-Faber-Lovasz Conjecture