Counterexamples to graph compactness and two-degenerate extremal bounds

Source: url:https://github.com/openai/ten-proofs Authors: OpenAI, Dean Cureton Status: verified Main declarations: CompactnessConjecture.quantitativeCompactnessCounterexample Tags: extremal-combinatorics, extremal-graph-theory, degenerate-graphs, counterexamples MSC: 05C35, 05C75

Counterexamples in extremal graph theory

This project proves quantitative counterexamples to the Erdős–Simonovits compactness conjecture and to the two-degenerate extremal-number conjecture.

The source is OpenAI's Apache-2.0 ten-proofs release at commit 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6. This import starts from Dean Cureton's semantics-preserving performance pass at commit 30c21d72a2ee3308d66c945387729d736e0cb305 and further adapts the development to Lean Pool.