Import compactness and degeneracy counterexamples

[Vilin97]

Summary

Imports both extremal-graph-theory counterexamples from OpenAI's ten-proofs release as one Lean Pool project:

• CompactnessConjecture.quantitativeCompactnessCounterexample, disproving the Erdős--Simonovits compactness conjecture quantitatively;
• TwoDegenerateGraphs.twoDegenerateExtremalCounterexample, disproving the proposed universal n^(3/2) extremal upper bound for the stated class of connected bipartite two-degenerate graphs.

The project is split into two focused leaf modules (8,882 and 8,834 non-comment code lines) plus a two-line entry module. Both exact source theorem names remain public and are recorded in main_results. The compactness theorem alone is in main_declarations so the generated card remains within the style invariant; the second theorem received the separate signature, closure, and axiom audit below.

Provenance

• Canonical source: OpenAI ten-proofs at 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6
• Optimization baseline: Dean Cureton's semantics-preserving pass at 30c21d72a2ee3308d66c945387729d736e0cb305
• License: Apache-2.0
• Proof provenance: mix (OpenAI source proofs plus Dean Cureton's and this import's optimization/adaptation work)

Both commit IDs are also preserved in the entry-module documentation.

Dependency closure and public surface

A source-declaration dependency pass was run before making implementation declarations module-private. After deleting the first two output-only declarations, 935 of the remaining 937 source declarations were reachable from the two headline results. The two residual unreachable declarations were then deleted as well. The four removed declarations are:

• CompactnessConjecture.compactnessCounterexample_bigO
• CompactnessConjecture.proposedFamily_familyExtremal_isBigO
• TwoDegenerateGraphs.DegeneracyConjectureStatement
• TwoDegenerateGraphs.not_erdos_146

Thus all 935 retained original declarations are in the union source closure of the two endpoints. Three small computable instances were added where the optimized construction needs them.

The compiled-environment closure was audited independently with opaque theorem values enabled. Of 1,918 project constants (including compiler-generated recursors, proof helpers, and simp auxiliaries):

• the compactness endpoint reaches 835, all in Compactness;
• the degeneracy endpoint reaches 705: 701 in Degeneracy and four in Compactness;
• their union reaches 1,536.

Only the statement vocabulary, the two cross-module extremal helpers, and the two endpoints are public; proof scaffolding is module-private. Exact-name search found no duplicate CompactnessConjecture or TwoDegenerateGraphs project namespaces elsewhere in Lean Pool. A mixed integration module importing this entry beside LeanPool.MulticolorTriangleRamsey elaborated successfully.

The separately audited second endpoint has the exact signature:

TwoDegenerateGraphs.twoDegenerateExtremalCounterexample :
  ∃ q H,
    H.Connected ∧
      H.IsBipartite ∧
        TwoDegenerateGraphs.IsTwoDegenerate H ∧
          (∀ (coloring : H.Coloring (Fin 2)) (side : Fin 2),
              2 < {vertex | coloring vertex = side}.sup fun vertex => H.degree vertex) ∧
            ∃ c ε, 0 < c ∧ 0 < ε ∧
              ∀ᶠ (n : ℕ) in Filter.atTop,
                c * ↑n ^ (3 / 2 + ε) ≤ ↑(SimpleGraph.extremalNumber n H)

#print axioms reports exactly [propext, Classical.choice, Quot.sound] for this theorem, and the same three permitted axioms for the compactness theorem.

Optimization and golf

• Replaced the exhaustive 8-by-8 finite case splits in the theta/gamma cycle homomorphisms with kernel-checked decide proofs.
• Reworked the subdivision-line center injectivity and directed-relation mapping arguments structurally.
• Narrowed accidental broad simp dependencies, including the quotient-copy and Boolean-word equivalence paths.
• Replaced the monolithic import Mathlib with focused public/private imports. lake shake --force --explain confirms every remaining import is required.
• Removed all 300 baseline warnings: 98 semantic/linter warnings and 202 long-line warnings.
• Removed every set_option; there are no waivers or forbidden constructs.

Measured on the same checkout with prebuilt Mathlib dependencies and forced source rebuilds:

Metric	Dean baseline	Imported project	Change
Wall time	65.79 s	25.21 s	-61.7%
Peak RSS	7.63 GiB	3.42 GiB	-55.2%
Warnings	300	0	-100%
Non-comment, non-whitespace characters	554,602	553,573	-1,029

Mandatory file splitting and 100-column formatting raise the physical non-comment line count from 17,536 to 17,718; the whitespace-insensitive character count above records the actual golf. Both leaf modules remain below the 10,000-code-line gate. There are zero proofs over 200 code lines (largest blocks: 180 and 161).

Absolute lean --profile runs measured 10.36 s / 2.48 GiB for Compactness and 7.81 s / 2.24 GiB for Degeneracy. The heartbeat linter's maxima are 9 and 2 units respectively, far below the 200,000 limit.

Verification

• lake build LeanPool.CompactnessAndDegeneracy — passed, warning-free
• lake exe runLinter LeanPool.CompactnessAndDegeneracy — passed
• lake exe lint-style LeanPool.CompactnessAndDegeneracy — passed
• lake exe mk_all --check — no update necessary
• focused lake shake --force --explain on both leaf modules — no removal suggestions
• targeted static quality suite — headers, reachability, forbidden text, lake options, style waivers, file/proof sizes, metadata uniqueness/imports/card/declaration checks all passed
• compiled option-manipulation/backdoor audit over LeanPool.CompactnessAndDegeneracy — zero findings
• manual #check and #print axioms for both headline declarations — passed with only the three permitted axioms
• mixed integration elaboration with the existing OpenAI multicolor Ramsey project — passed

[greptile-apps]

Greptile Summary

The PR imports two extremal graph theory counterexamples as a single Lean Pool project.

• Adds focused compactness and two-degeneracy proof modules.
• Registers both headline results and their provenance in the project catalog.
• Connects the new entry and leaf modules to the aggregate import.

Important Files Changed

Filename	Overview
LeanPool/CompactnessAndDegeneracy/Compactness.lean	Adds the quantitative compactness counterexample and its supporting finite-graph construction.
LeanPool/CompactnessAndDegeneracy/Degeneracy.lean	Adds the connected bipartite two-degenerate graph counterexample and its extremal lower bound.
LeanPool/CompactnessAndDegeneracy.lean	Defines the project entry module and records source and adaptation provenance.
LeanPool/projects.yml	Registers the project, its two main results, source revision, authorship, and license.
LeanPool.lean	Adds the entry and leaf modules to the repository-wide aggregate import.

_{Reviews (8): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile}

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 78.07 s (= 1.30 min) — user 191.55 s, sys 7.90 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 2,162 maxHeartbeats units across 3 files (18,909 added LOC).

Sum of lean --profile: 165163.3 ms (= 165.16 s). Import-excluded time: 161073.3 ms (= 161.07 s).

Count-heartbeats wall-clock total: 92.59 s. Repeated import cost inside lean --profile: 4090.0 ms (= 4.09 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/CompactnessAndDegeneracy/Compactness.lean	9,586	1,356	44.82	77.45	76.34	1.11	465	0
LeanPool/CompactnessAndDegeneracy/Degeneracy.lean	9,291	806	42.56	85.72	84.48	1.24	403	0
LeanPool/CompactnessAndDegeneracy.lean	32	0	5.21	2.00	0.26	1.74	0	0
Total	18,909	2,162	92.59	165.16	161.07	4.09	868	0

Aggregate phase totals

Phase	Time
interpretation	31517.0 ms (= 31.52 s)
typeclass inference	30600.0 ms (= 30.60 s)
tactic execution	27800.0 ms (= 27.80 s)
simp	20650.0 ms (= 20.65 s)
blocked (unaccounted)	14480.0 ms (= 14.48 s)
type checking	8630.0 ms (= 8.63 s)
elaboration	6320.3 ms (= 6.32 s)
import	4090.0 ms (= 4.09 s)
instantiate metavars	3392.0 ms (= 3.39 s)
norm_num	3311.0 ms (= 3.31 s)
ring	2850.0 ms (= 2.85 s)
tacticAnalysis	2821.6 ms (= 2.82 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.CompactnessAndDegeneracy.Compactness	32.00 s
LeanPool.CompactnessAndDegeneracy.Degeneracy	28.00 s
LeanPool.CompactnessAndDegeneracy	6.80 s

Per-file `lean --profile` output

LeanPool/CompactnessAndDegeneracy.lean

import took 1.74s
cumulative profiling times:
	elaboration 0.291ms
	import 1.74s
	initialization 35.2ms
	interpretation 217ms
	linting 0.482ms
	module linting 0.00125ms
	overlappingInstancesLinter 0.347ms
	parsing 0.0521ms
	tacticAnalysis 1.63ms
real 2.66
user 1.52
sys 1.15

LeanPool/CompactnessAndDegeneracy/Compactness.lean

import took 1.11s
tactic execution of Lean.Parser.Tactic.simpAll took 137ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 126ms
type checking took 154ms
instantiate metavars took 506ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 200ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 195ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 184ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 187ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 179ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 156ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 135ms
instantiate metavars took 2.44s
share common exprs took 325ms
process pre-definitions took 129ms
elaboration took 285ms
type checking took 301ms
linting took 214ms
simp took 140ms
simp took 120ms
simp took 113ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 239ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 251ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 119ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 227ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 279ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 126ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 251ms
simp took 115ms
simp took 111ms
simp took 116ms
simp took 116ms
simp took 101ms
tactic execution of Lean.Parser.Tactic.change took 207ms
typeclass inference of NonUnitalNonAssocSemiring took 121ms
typeclass inference of ZeroHomClass took 286ms
typeclass inference of NonUnitalNonAssocSemiring took 127ms
typeclass inference of NonUnitalSemiring took 102ms
typeclass inference of ZeroHomClass took 285ms
simp took 117ms
simp took 118ms
simp took 117ms
simp took 116ms
cumulative profiling times:
	aesop 68.5ms
	attribute application 13.7ms
	blocked (unaccounted) 6.86s
	compilation (IR) 5.84ms
	compilation (LCNF base) 93.1ms
	compilation (LCNF impure) 28ms
	compilation (LCNF mono) 60.6ms
	congr simp thm 161ms
	dsimp 35.9ms
	elaboration 4.1s
	fix level params 216ms
	import 1.11s
	initialization 41ms
	instantiate metavars 3.29s
	interpretation 12.2s
	let-to-have transformation 39.1ms
	linting 1.31s
	module linting 0.0013ms
	norm_num 501ms
	overlappingInstancesLinter 205ms
	parsing 587ms
	process pre-definitions 1.12s
	ring 1.11s
	share common exprs 1.03s
	simp 8.25s
	tactic execution 13.6s
	tacticAnalysis 1.5s
	type checking 4.81s
	typeclass inference 15.1s
real 24.49
user 69.33
sys 2.21

LeanPool/CompactnessAndDegeneracy/Degeneracy.lean

import took 1.24s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 130ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 333ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 110ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 114ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 101ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 105ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 129ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 232ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 120ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 487ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 151ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 133ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 207ms
tactic execution of Mathlib.Tactic.nlinarith took 258ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 220ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 216ms
tactic execution of Mathlib.Tactic.nlinarith took 888ms
tactic execution of Mathlib.Tactic.nlinarith took 910ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 110ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 104ms
tactic execution of Mathlib.Tactic.nlinarith took 737ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 177ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 239ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 215ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 638ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 129ms
tactic execution of Lean.Parser.Tactic.refine took 101ms
linting took 183ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 467ms
simp took 179ms
simp took 150ms
simp took 154ms
simp took 149ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 137ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 561ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 805ms
simp took 167ms
simp took 159ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 128ms
tactic execution of Mathlib.Tactic.nlinarith took 135ms
simp took 192ms
simp took 520ms
tactic execution of Lean.Parser.Tactic.change took 1.2s
tactic execution of Lean.Parser.Tactic.exact took 115ms
linting took 134ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 146ms
simp took 2.78s
simp took 1.69s
tactic execution of Lean.Parser.Tactic.congr took 1.22s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 435ms
cumulative profiling times:
	aesop 63.6ms
	attribute application 5.66ms
	blocked (unaccounted) 7.62s
	compilation (IR) 1.23ms
	compilation (LCNF base) 17.6ms
	compilation (LCNF impure) 4.92ms
	compilation (LCNF mono) 7.98ms
	congr simp thm 157ms
	dsimp 137ms
	elaboration 2.22s
	fix level params 50.5ms
	import 1.24s
	initialization 28.8ms
	instantiate metavars 102ms
	interpretation 19.1s
	let-to-have transformation 7.03ms
	linting 1.3s
	module linting 0.00131ms
	norm_num 2.81s
	overlappingInstancesLinter 98.2ms
	parsing 517ms
	process pre-definitions 594ms
	ring 1.74s
	share common exprs 660ms
	simp 12.4s
	tactic execution 14.2s
	tacticAnalysis 1.32s
	type checking 3.82s
	typeclass inference 15.5s
real 23.55
user 77.14
sys 1.37

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[github-actions]

🤖 LLM review (gpt-5.6-sol, 5 rubrics)

Reviewed head: 4f02883d0eccb6f5ef054b97cc9a5073dcd7cf40

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	Both headline declarations match the card’s quantified claims and are unconditional.
Novelty	✅ pass	Neither headline result is already formalized by the supplied Mathlib hits or any listed pool project.
Significance	✅ pass	This is a completed research-level extremal graph theory project with two substantial counterexamples, including a quantitative disproof of the Erdős–Simonovits compactness conjecture.
Sources	✅ pass	The canonical formalization and the optimization baseline are explicitly credited with exact commits, but the cited repository contents cannot be independently checked from the diff.
Code quality (advisory)	✅ pass	The development is coherently sectioned, keeps proof scaffolding private, and exposes a small cross-module API with no material maintainability defect evident in the diff.

Aspect	Value
Proves the claim	✅ proves_it
Matches cited source	🟡 unverifiable
Fit	✅ good_fit
Level	research
Branch	extremal graph theory
Mode	theory_building
Code quality	4 / 5

Statement check: The first endpoint constructs the stated finite family with uniform member lower bounds, quantitative family-free host bounds, noncompactness, and failure of the compactness conjecture; the second constructs the stated connected bipartite two-degenerate graph with the bipartition degree condition and an eventual c n^(3/2+ε) extremal lower bound.

The project proves CompactnessConjecture.quantitativeCompactnessCounterexample, which concludes ¬ CompactnessConjectureStatement, and constructs in TwoDegenerateGraphs.twoDegenerateExtremalCounterexample a connected bipartite two-degenerate graph with extremal growth of order at least n^(3/2+ε) for some positive ε.

---

Tokens: 1,262,253 in / 6,399 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $3.2516
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

/review

[github-actions]

LLM review skipped: Lean Action CI conclusion was in_progress. Push a fix or comment /review after CI is green.

[Vilin97]

Automation disposition: needs-maintainer

Reviewed exact head 608b865 after a verified repair pass. The duplicate constant was removed and one broad private import was narrowed; both leaf modules build. The remaining full Compactness-to-Degeneracy coupling, final conjunction repackaging, and unavoidable private BinaryEntropy dependency keep quality below 4/5 and need an architectural maintainer decision.