∑math20

Combinatorics · Result 181

The Erdős–Gallai cycle-decomposition conjecture

1 paperLean

Proves that the edges of every finite simple undirected graph on n vertices can be partitioned into at most \(Cn\) simple cycles and single edges, for an absolute constant C. This resolves the Erdős–Gallai cycle-decomposition conjecture, bounding the number of pieces linearly even for dense graphs.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of A linear cycle-and-edge decomposition of every graph

A linear cycle-and-edge decomposition of every graph

OpenAI · September 24, 2026

We prove that every finite simple undirected graph on n vertices has an edge partition into at most \(Cn\) simple cycles and single edges, for an absolute constant C. This resolves the Erdős–Gallai cycle decomposition conjecture positively.

Read PDF Download Source

Cite
@misc{OAI:A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026,
  author = {{OpenAI}},
  title = {{A linear cycle-and-edge decomposition of every graph}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026/main.pdf}{OAI:A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The Erdős–Gallai cycle-decomposition conjecture asks for a linear bound on the number of cycles and single edges needed to partition a graph's edges. The formalized result gives one absolute constant \(C>0\) such that every finite simple graph on \(n\) vertices has an edge-disjoint decomposition into at most \(Cn\) cycles or singleton edges. Edgeless and small graphs are included. The optimal value of \(C\) is not determined.

Comparator links

ResultComparator statement
Linear cycle-and-edge decompositionCycleDecomposition.lean

Scope note on GitHub →