Import compactness and degeneracy counterexamples

LeanPool.lean

@@ -605,6 +605,9 @@ import LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint.Sp
 import LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint.SpectralTheorem
 import LeanPool.CompactSpectral.Analysis.InnerProductSpace.RayleighCompact
 import LeanPool.CompactSpectral.Topology.WeakHilbertCompact
+import LeanPool.CompactnessAndDegeneracy
+import LeanPool.CompactnessAndDegeneracy.Compactness
+import LeanPool.CompactnessAndDegeneracy.Degeneracy
 import LeanPool.CompositionAlgebras
 import LeanPool.CompositionAlgebras.Composition.CayleyDickson
 import LeanPool.CompositionAlgebras.Composition.Classification

LeanPool/CompactnessAndDegeneracy.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 OpenAI and Dean Cureton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: OpenAI, Dean Cureton
+-/
+
+import LeanPool.CompactnessAndDegeneracy.Compactness
+import LeanPool.CompactnessAndDegeneracy.Degeneracy
+
+/-!
+# 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.
+-/