From 7a4b61929d9c953d2ce75e0f5ea4b0ecb902fc58 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 9 Aug 2026 20:42:52 +0800 Subject: [PATCH 1/8] feat(Combinatorics): designs exist --- LeanEval/Combinatorics/DesignsExist | 86 +++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 LeanEval/Combinatorics/DesignsExist diff --git a/LeanEval/Combinatorics/DesignsExist b/LeanEval/Combinatorics/DesignsExist new file mode 100644 index 000000000..d1447239d --- /dev/null +++ b/LeanEval/Combinatorics/DesignsExist @@ -0,0 +1,86 @@ +import Mathlib +import EvalTools.Markers + +/-! +# Existence of designs + +Peter Keevash showed in 2014 that designs of parameters (n, q, r, λ) exist provided +n is sufficiently large (given fixed q, r, λ). + +We include multiple related results with similar methods of proof in this challenge +to encourage production of reusable code. + +## References + +* Peter Keevash. The existence of designs. https://arxiv.org/abs/1401.3665 + +* Peter Keevash. The existence of designs II. https://people.maths.ox.ac.uk/keevash/papers/designsII.pdf + +* Peter Keevash, Ashwin Sah, Mehtaab Sawhney. The existence of subspace designs. https://arxiv.org/abs/2212.00870 + +* Gil Kalai. Designs Exist! [after Peter Keevash] http://www.bourbaki.ens.fr/TEXTES/1100.pdf + +* https://aperiodical.com/2014/01/proof-news-designs-exist/ includes links to multiple blog posts. +-/ +namespace LeanEval.Combinatorics.DesignsExist + +/-- The type of designs with parameter (#X, q, r, lam). -/ +structure Design (X : Type*) (q r lam : ℕ) where + blocks : Set (Set X) + card_blocks : ∀ s ∈ blocks, s.encard = q + card_subset : ∀ s : Set X, s.encard = r → {b ∈ blocks | s ⊆ b}.encard = lam + +/-- The obvious necessary condition for a design of given parameters to exist. -/ +def DivisibilityCondition (n q r lam : ℕ) : Prop := + ∀ i ∈ Finset.range r, (q - i).choose (r - i) ∣ lam * (n - i).choose (r - i) + +/-- Existence of designs. Theorem 0.1 in Kalai's Bourbaki notes. -/ +@[eval_problem] theorem keevash (q r lam : ℕ+) (hrq : r ≤ q) : + ∃ N : ℕ, ∀ n > N, DivisibilityCondition n q r lam → Nonempty (Design (Fin n) q r lam) := by + sorry + +/-- Existence of resolvable designs (for which the set of blocks can be partitioned into partitions. +Theorem 1.1 in *The existence of designs II*. -/ +@[eval_problem] theorem keevash_resolvable (q r lam : ℕ+) (hrq : r ≤ q) : + ∃ N : ℕ, ∀ n > N, DivisibilityCondition n q r lam → (q : ℕ) ∣ n → + ∃ d : Design (Fin n) q r lam, ∃ p : Partition d.blocks, + ∀ s ∈ p, ∃ p' : Partition (.univ : Set (Fin n)), p' = s := by + sorry + +/-- Existence of a large set of designs. Theorem 1.2 in *The existence of designs II*. -/ +@[eval_problem] theorem keevash_large_set (q r : ℕ+) (hrq : r ≤ q) : + ∃ N : ℕ, ∀ n > N, ∀ lam : ℕ+, DivisibilityCondition n q r lam → + (lam : ℕ) ∣ (n - r : ℕ).choose (q - r) → + ∃ p : Partition {s : Set (Fin n) | s.encard = q}, + ↑p ⊆ Set.range fun d : Design (Fin n) q r lam ↦ d.blocks := by + sorry + +/-- Existence of a complete resolution of Kₙ^q. Theorem 1.3 in *The existence of designs II*. -/ +@[eval_problem] theorem keevash_complete_resolution (q : ℕ+) : + ∃ N : ℕ, ∀ n > N, (∀ i ≤ q, (i : ℕ) ∣ (n - q)) → + ∃ s : Π i : Fin q, Set (Design (Fin n) q (i + 1) 1), + (s (.rev 0)).encard = 1 ∧ ∀ i j : Fin q, i ≤ j → + ∀ d ∈ s j, ∃ p : Partition d.blocks, ↑p ⊆ Design.blocks '' s i := by + sorry + +/-- The type of subspace designs with parameter (dim V, s, r, lam). -/ +structure SubspaceDesign (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V] + (s r lam : ℕ) where + subspaces : Set (Subspace K V) + rank_subspaces : ∀ W ∈ subspaces, Module.rank K W = s + card_subset : ∀ U : Subspace K V, Module.rank K U = r → {W ∈ subspaces | U ≤ W}.encard = lam + +/-- q-binomial coefficients. -/ +def qChoose (q n k : ℕ) := + let prod (n : ℕ) := ∏ i ∈ Finset.Icc 1 n, (q ^ i - 1) + prod n / (prod k * prod (n - k)) + +/-- Existence of subspace designs: Theorem 1.4 in the paper by Keevash, Sah and Sawhney. -/ +@[eval_problem] +theorem keevash_sah_sawhney (K : Type*) [Finite K] [Field K] (s r : ℕ) (lt : r < s) (lam : ℕ+) : + ∃ N, ∀ n > N, let q := Nat.card K + (∀ i ∈ Finset.range r, qChoose q (s - i) (r - i) ∣ lam * qChoose q (n - i) (r - i)) → + Nonempty (SubspaceDesign K (Fin n → K) s r lam) := by + sorry + +end LeanEval.Combinatorics.DesignsExist From 89cbbbac0238a5a3d1549918b77003ae884c3fcd Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 9 Aug 2026 20:43:40 +0800 Subject: [PATCH 2/8] .lean suffix --- LeanEval/Combinatorics/{DesignsExist => DesignsExist.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename LeanEval/Combinatorics/{DesignsExist => DesignsExist.lean} (100%) diff --git a/LeanEval/Combinatorics/DesignsExist b/LeanEval/Combinatorics/DesignsExist.lean similarity index 100% rename from LeanEval/Combinatorics/DesignsExist rename to LeanEval/Combinatorics/DesignsExist.lean From 2f17a0b478e0ca87552ff8e6f1366d7e29d41550 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 9 Aug 2026 20:48:24 +0800 Subject: [PATCH 3/8] toml --- manifests/problems/designs_exist.toml | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 manifests/problems/designs_exist.toml diff --git a/manifests/problems/designs_exist.toml b/manifests/problems/designs_exist.toml new file mode 100644 index 000000000..8963e937d --- /dev/null +++ b/manifests/problems/designs_exist.toml @@ -0,0 +1,7 @@ +id = "designs_exist" +title = "The existence of designs" +test = false +module = "LeanEval.Combinatorics.DesignsExist" +holes = ["keevash", "keevash_resolvable", "keevash_large_set", "keevash_complete_resolution", "keevash_sah_sawhney"] +notes = "Keywords: probabilistic method, randomized algebraic constructions, absorption." +submitter = "Junyan Xu" From f9fc15508de132fdedc6a0e200564b2c3bc2acc8 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 10 Aug 2026 03:07:35 +0800 Subject: [PATCH 4/8] more refs + 1 more problem --- LeanEval/Combinatorics/DesignsExist.lean | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/LeanEval/Combinatorics/DesignsExist.lean b/LeanEval/Combinatorics/DesignsExist.lean index d1447239d..971211488 100644 --- a/LeanEval/Combinatorics/DesignsExist.lean +++ b/LeanEval/Combinatorics/DesignsExist.lean @@ -13,13 +13,12 @@ to encourage production of reusable code. ## References * Peter Keevash. The existence of designs. https://arxiv.org/abs/1401.3665 - * Peter Keevash. The existence of designs II. https://people.maths.ox.ac.uk/keevash/papers/designsII.pdf - +* Peter Keevash. Counting designs. https://arxiv.org/abs/1504.02909 * Peter Keevash, Ashwin Sah, Mehtaab Sawhney. The existence of subspace designs. https://arxiv.org/abs/2212.00870 - +* Stefan Glock, Daniela Kühn, Allan Lo, Deryk Osthus. The existence of designs via iterative absorption: hypergraph F-designs for arbitrary F. https://arxiv.org/abs/1611.06827 +* W. T. Gowers. Probabilistic combinatorics and the recent work of Peter Keevash. https://www.ams.org/journals/bull/2017-54-01/S0273-0979-2016-01553-9/S0273-0979-2016-01553-9.pdf * Gil Kalai. Designs Exist! [after Peter Keevash] http://www.bourbaki.ens.fr/TEXTES/1100.pdf - * https://aperiodical.com/2014/01/proof-news-designs-exist/ includes links to multiple blog posts. -/ namespace LeanEval.Combinatorics.DesignsExist @@ -39,6 +38,14 @@ def DivisibilityCondition (n q r lam : ℕ) : Prop := ∃ N : ℕ, ∀ n > N, DivisibilityCondition n q r lam → Nonempty (Design (Fin n) q r lam) := by sorry +/-- Asymptotics on the number of Steiner triple systems: if n is 1 or 3 mod 6, then +the number of Steiner triple systems on n vertices is (n/e² + o(n)) ^ (n²/6). +Theorem 2.2 of *Counting designs*. -/ +@[eval_problem] theorem steiner_triple_asymptotics : + (fun n : ℕ ↦ Nat.card (Design (Fin n) 3 2 1) ^ (6 / n ^ 2 : ℝ) - + if 6 ∣ (n + 5) ∨ 6 ∣ (n + 3) then n / Real.exp 2 else 0) =o[Filter.atTop] ((↑) : ℕ → ℝ) := by + sorry + /-- Existence of resolvable designs (for which the set of blocks can be partitioned into partitions. Theorem 1.1 in *The existence of designs II*. -/ @[eval_problem] theorem keevash_resolvable (q r lam : ℕ+) (hrq : r ≤ q) : From 5de4392ae271adb4bb731a2b90f7d62293a7d864 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 10 Aug 2026 03:07:58 +0800 Subject: [PATCH 5/8] Update holes list in designs_exist.toml --- manifests/problems/designs_exist.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manifests/problems/designs_exist.toml b/manifests/problems/designs_exist.toml index 8963e937d..3a61a5422 100644 --- a/manifests/problems/designs_exist.toml +++ b/manifests/problems/designs_exist.toml @@ -2,6 +2,6 @@ id = "designs_exist" title = "The existence of designs" test = false module = "LeanEval.Combinatorics.DesignsExist" -holes = ["keevash", "keevash_resolvable", "keevash_large_set", "keevash_complete_resolution", "keevash_sah_sawhney"] +holes = ["keevash", "steiner_triple_asymptotics", "keevash_resolvable", "keevash_large_set", "keevash_complete_resolution", "keevash_sah_sawhney"] notes = "Keywords: probabilistic method, randomized algebraic constructions, absorption." submitter = "Junyan Xu" From 005ca778fb4c52f544f31bd27bcf68aefb0bc0ae Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Fri, 14 Aug 2026 02:17:00 +0800 Subject: [PATCH 6/8] @[eval_problem] on separate line --- LeanEval/Combinatorics/DesignsExist.lean | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/LeanEval/Combinatorics/DesignsExist.lean b/LeanEval/Combinatorics/DesignsExist.lean index 971211488..f3ba5f436 100644 --- a/LeanEval/Combinatorics/DesignsExist.lean +++ b/LeanEval/Combinatorics/DesignsExist.lean @@ -30,32 +30,36 @@ structure Design (X : Type*) (q r lam : ℕ) where card_subset : ∀ s : Set X, s.encard = r → {b ∈ blocks | s ⊆ b}.encard = lam /-- The obvious necessary condition for a design of given parameters to exist. -/ -def DivisibilityCondition (n q r lam : ℕ) : Prop := +def DivisibilityCondition (n q r lam : ℕ) : Prop := ∀ i ∈ Finset.range r, (q - i).choose (r - i) ∣ lam * (n - i).choose (r - i) /-- Existence of designs. Theorem 0.1 in Kalai's Bourbaki notes. -/ -@[eval_problem] theorem keevash (q r lam : ℕ+) (hrq : r ≤ q) : +@[eval_problem] +theorem keevash (q r lam : ℕ+) (hrq : r ≤ q) : ∃ N : ℕ, ∀ n > N, DivisibilityCondition n q r lam → Nonempty (Design (Fin n) q r lam) := by sorry /-- Asymptotics on the number of Steiner triple systems: if n is 1 or 3 mod 6, then the number of Steiner triple systems on n vertices is (n/e² + o(n)) ^ (n²/6). Theorem 2.2 of *Counting designs*. -/ -@[eval_problem] theorem steiner_triple_asymptotics : +@[eval_problem] +theorem steiner_triple_asymptotics : (fun n : ℕ ↦ Nat.card (Design (Fin n) 3 2 1) ^ (6 / n ^ 2 : ℝ) - if 6 ∣ (n + 5) ∨ 6 ∣ (n + 3) then n / Real.exp 2 else 0) =o[Filter.atTop] ((↑) : ℕ → ℝ) := by sorry /-- Existence of resolvable designs (for which the set of blocks can be partitioned into partitions. Theorem 1.1 in *The existence of designs II*. -/ -@[eval_problem] theorem keevash_resolvable (q r lam : ℕ+) (hrq : r ≤ q) : - ∃ N : ℕ, ∀ n > N, DivisibilityCondition n q r lam → (q : ℕ) ∣ n → +@[eval_problem] +theorem keevash_resolvable (q r lam : ℕ+) (hrq : r ≤ q) : + ∃ N : ℕ, ∀ n > N, DivisibilityCondition n q r lam → (q : ℕ) ∣ n → ∃ d : Design (Fin n) q r lam, ∃ p : Partition d.blocks, ∀ s ∈ p, ∃ p' : Partition (.univ : Set (Fin n)), p' = s := by sorry /-- Existence of a large set of designs. Theorem 1.2 in *The existence of designs II*. -/ -@[eval_problem] theorem keevash_large_set (q r : ℕ+) (hrq : r ≤ q) : +@[eval_problem] +theorem keevash_large_set (q r : ℕ+) (hrq : r ≤ q) : ∃ N : ℕ, ∀ n > N, ∀ lam : ℕ+, DivisibilityCondition n q r lam → (lam : ℕ) ∣ (n - r : ℕ).choose (q - r) → ∃ p : Partition {s : Set (Fin n) | s.encard = q}, @@ -63,10 +67,11 @@ Theorem 1.1 in *The existence of designs II*. -/ sorry /-- Existence of a complete resolution of Kₙ^q. Theorem 1.3 in *The existence of designs II*. -/ -@[eval_problem] theorem keevash_complete_resolution (q : ℕ+) : +@[eval_problem] +theorem keevash_complete_resolution (q : ℕ+) : ∃ N : ℕ, ∀ n > N, (∀ i ≤ q, (i : ℕ) ∣ (n - q)) → ∃ s : Π i : Fin q, Set (Design (Fin n) q (i + 1) 1), - (s (.rev 0)).encard = 1 ∧ ∀ i j : Fin q, i ≤ j → + (s (.rev 0)).encard = 1 ∧ ∀ i j : Fin q, i ≤ j → ∀ d ∈ s j, ∃ p : Partition d.blocks, ↑p ⊆ Design.blocks '' s i := by sorry From 673d6a8b8ac564656d05bbc6c36eefc61ccdeda4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 21 Aug 2026 00:50:19 +0000 Subject: [PATCH 7/8] fix(Combinatorics): require r < q in the design existence statements MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Design` takes `blocks : Set (Set X)`, so designs here are simple. When `r = q` a block of size `q` containing an `r`-set `s` must equal `s`, so `{b ∈ blocks | s ⊆ b}.encard ≤ 1` and no design with `lam ≥ 2` exists, while `DivisibilityCondition n q q lam` holds vacuously because every factor is `(q - i).choose (q - i) = 1`. That makes `keevash` and `keevash_resolvable` false at `q = r`, e.g. `q = r = 1`, `lam = 2`. Both sources state the theorem for `q ≥ r ≥ 1` but also define a design as a set of blocks, so they have the same corner case; it is read out informally. Use the strict inequality, matching `keevash_sah_sawhney` below. `keevash_large_set` is unaffected: at `q = r` its extra hypothesis reads `lam ∣ (n - r).choose 0 = 1`. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011hxUxCg6joVz4hMa3m5Zh5 --- LeanEval/Combinatorics/DesignsExist.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanEval/Combinatorics/DesignsExist.lean b/LeanEval/Combinatorics/DesignsExist.lean index f3ba5f436..e582417b7 100644 --- a/LeanEval/Combinatorics/DesignsExist.lean +++ b/LeanEval/Combinatorics/DesignsExist.lean @@ -35,7 +35,7 @@ def DivisibilityCondition (n q r lam : ℕ) : Prop := /-- Existence of designs. Theorem 0.1 in Kalai's Bourbaki notes. -/ @[eval_problem] -theorem keevash (q r lam : ℕ+) (hrq : r ≤ q) : +theorem keevash (q r lam : ℕ+) (hrq : r < q) : ∃ N : ℕ, ∀ n > N, DivisibilityCondition n q r lam → Nonempty (Design (Fin n) q r lam) := by sorry @@ -51,7 +51,7 @@ theorem steiner_triple_asymptotics : /-- Existence of resolvable designs (for which the set of blocks can be partitioned into partitions. Theorem 1.1 in *The existence of designs II*. -/ @[eval_problem] -theorem keevash_resolvable (q r lam : ℕ+) (hrq : r ≤ q) : +theorem keevash_resolvable (q r lam : ℕ+) (hrq : r < q) : ∃ N : ℕ, ∀ n > N, DivisibilityCondition n q r lam → (q : ℕ) ∣ n → ∃ d : Design (Fin n) q r lam, ∃ p : Partition d.blocks, ∀ s ∈ p, ∃ p' : Partition (.univ : Set (Fin n)), p' = s := by From 3936cd8a5225d6a64c315b40d2f602f6fb209c6f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 21 Aug 2026 01:31:44 +0000 Subject: [PATCH 8/8] chore: add catalog lifecycle metadata to the manifest Main now requires `group`, `status`, `visible`, `statement_revision` and `tags` in every problem manifest (EvalTools/Markers.lean, added in 07848f4). Without them `validate-manifest` fails with "missing required key: group". Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011hxUxCg6joVz4hMa3m5Zh5 --- manifests/problems/designs_exist.toml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/manifests/problems/designs_exist.toml b/manifests/problems/designs_exist.toml index 3a61a5422..be5ae3380 100644 --- a/manifests/problems/designs_exist.toml +++ b/manifests/problems/designs_exist.toml @@ -1,5 +1,10 @@ id = "designs_exist" title = "The existence of designs" +group = "formalization-evaluation" +status = "draft" +visible = true +statement_revision = 1 +tags = [] test = false module = "LeanEval.Combinatorics.DesignsExist" holes = ["keevash", "steiner_triple_asymptotics", "keevash_resolvable", "keevash_large_set", "keevash_complete_resolution", "keevash_sah_sawhney"]