AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

A linear cycle-and-edge decomposition of every graph

Can the mathematical statement in A linear cycle-and-edge decomposition of every graph be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 181)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A linear cycle-and-edge decomposition of every graph'. 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.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 181). The Lean development was not rebuilt locally.