From a7573499733400c03b0ecb6dad2d0fc90fae2c3d Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 2 Oct 2026 10:29:19 -0700 Subject: [PATCH] Remove retired challenge statements, solutions, and registry --- Challenge.lean | 8 - Challenge/BudgetedSubmodular.lean | 80 ------ Challenge/BudgetedSubmodular0405.lean | 80 ------ Challenge/Mazur.lean | 47 ---- Challenge/McKay.lean | 55 ----- Challenge/Odlyzko.lean | 42 ---- Challenge/TestingByBetting.lean | 51 ---- Challenge/challenges.yml | 332 ------------------------- Solution.lean | 5 - Solution/BudgetedSubmodular.lean | 342 -------------------------- Solution/Odlyzko.lean | 40 --- Solution/TestingByBetting.lean | 187 -------------- 12 files changed, 1269 deletions(-) delete mode 100644 Challenge.lean delete mode 100644 Challenge/BudgetedSubmodular.lean delete mode 100644 Challenge/BudgetedSubmodular0405.lean delete mode 100644 Challenge/Mazur.lean delete mode 100644 Challenge/McKay.lean delete mode 100644 Challenge/Odlyzko.lean delete mode 100644 Challenge/TestingByBetting.lean delete mode 100644 Challenge/challenges.yml delete mode 100644 Solution.lean delete mode 100644 Solution/BudgetedSubmodular.lean delete mode 100644 Solution/Odlyzko.lean delete mode 100644 Solution/TestingByBetting.lean diff --git a/Challenge.lean b/Challenge.lean deleted file mode 100644 index b24de6de32..0000000000 --- a/Challenge.lean +++ /dev/null @@ -1,8 +0,0 @@ -module -- shake: keep-all --deprecated_module: ignore - -public import Challenge.BudgetedSubmodular -public import Challenge.BudgetedSubmodular0405 -public import Challenge.Mazur -public import Challenge.McKay -public import Challenge.Odlyzko -public import Challenge.TestingByBetting diff --git a/Challenge/BudgetedSubmodular.lean b/Challenge/BudgetedSubmodular.lean deleted file mode 100644 index afcefd8c09..0000000000 --- a/Challenge/BudgetedSubmodular.lean +++ /dev/null @@ -1,80 +0,0 @@ -/- -Copyright (c) 2026 Mikhail Nemerov. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mikhail Nemerov --/ - -module - -public import Mathlib.Analysis.SpecialFunctions.Exp -public import Mathlib.Algebra.Order.BigOperators.Group.Finset - -/-! -# Modified greedy for budgeted monotone submodular maximisation - -Source: doi:10.1145/3447386, url:https://arxiv.org/abs/2008.05391 -Proposed by: Mikhail Nemerov -Open declarations: `Challenge.BudgetedSubmodular.modifiedGreedy_approx` -Tags: combinatorics, optimization, approximation-algorithms, submodular-functions -MSC: 90C27, 68W25 -Estimated size: ~600 lines of Lean - -Informal statement: -* `Challenge.BudgetedSubmodular.modifiedGreedy_approx` — For a monotone submodular set function F on - finite sets with F of the empty set equal to 0, positive costs, a budget B and a finite ground set - U, the better of the cost-benefit greedy set built from U and the best single item of U that fits - the budget has value at least (1 - 1/e)/2 times the value of every subset of U whose total cost is - at most B. --/ - -public section - -namespace Challenge.BudgetedSubmodular - -open Finset - -variable {ι : Type*} [DecidableEq ι] - -/-- A monotone set function with diminishing returns (submodular). -/ -structure MonoSubmodular (F : Finset ι → ℝ) : Prop where - mono : ∀ {S U : Finset ι}, S ⊆ U → F S ≤ F U - dr : ∀ {S U : Finset ι}, S ⊆ U → ∀ x, F (insert x U) - F U ≤ F (insert x S) - F S - -/-- The items of `U` outside `G` that still fit the budget `B` next to `G`. -/ -noncomputable def fits (c : ι → ℝ) (B : ℝ) (U G : Finset ι) : Finset ι := - (U \ G).filter fun x => ∑ y ∈ G, c y + c x ≤ B - -/-- When some item fits, one of them has the largest gain per unit cost. A named theorem rather -than a proof inside `greedyStep`: Lean moves a nested proof into a private auxiliary lemma whose -name carries the module, which no solution module could reproduce. -/ -theorem exists_best (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U G : Finset ι) - (h : (fits c B U G).Nonempty) : - ∃ x ∈ fits c B U G, ∀ y ∈ fits c B U G, - (F (insert y G) - F G) / c y ≤ (F (insert x G) - F G) / c x := - (fits c B U G).exists_max_image _ h - -/-- One greedy step: add an item of `fits` with the largest gain per unit cost (ties broken -arbitrarily); keep `G` when nothing fits. -/ -noncomputable def greedyStep (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U G : Finset ι) : - Finset ι := - if h : (fits c B U G).Nonempty then insert (Classical.choose (exists_best F c B U G h)) G - else G - -/-- The greedy run on the ground set `U`: `U.card` steps from the empty set. -/ -noncomputable def greedy (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U : Finset ι) : Finset ι := - (greedyStep F c B U)^[U.card] ∅ - -/-- The best value of a single item of `U` that fits the budget (`0` when none fits). -/ -noncomputable def bestSingle (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U : Finset ι) : ℝ := - if h : (U.filter fun x => c x ≤ B).Nonempty then - (U.filter fun x => c x ≤ B).sup' h fun x => F {x} - else 0 - -/-- The modified greedy guarantee `(1 - 1/e)/2` (Khuller–Moss–Naor 1999; see Tang et al. 2021, -who prove `0.405` for the same algorithm). -/ -theorem modifiedGreedy_approx (F : Finset ι → ℝ) (hF : MonoSubmodular F) (hF0 : F ∅ = 0) - (c : ι → ℝ) (hc : ∀ i, 0 < c i) (B : ℝ) (U O : Finset ι) (hOU : O ⊆ U) - (hOB : ∑ y ∈ O, c y ≤ B) : - (1 - Real.exp (-1)) / 2 * F O ≤ max (F (greedy F c B U)) (bestSingle F c B U) := sorry - -end Challenge.BudgetedSubmodular diff --git a/Challenge/BudgetedSubmodular0405.lean b/Challenge/BudgetedSubmodular0405.lean deleted file mode 100644 index 613923d3cd..0000000000 --- a/Challenge/BudgetedSubmodular0405.lean +++ /dev/null @@ -1,80 +0,0 @@ -/- -Copyright (c) 2026 Mikhail Nemerov. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mikhail Nemerov --/ - -module - -public import Mathlib.Analysis.SpecialFunctions.Exp -public import Mathlib.Algebra.Order.BigOperators.Group.Finset - -/-! -# The 0.405 factor of modified greedy for budgeted submodular maximisation - -Source: doi:10.1145/3447386, url:https://arxiv.org/abs/2008.05391 -Proposed by: Mikhail Nemerov -Open declarations: `Challenge.BudgetedSubmodular0405.approximation` -Tags: combinatorics, optimization, approximation-algorithms, submodular-functions -MSC: 90C27, 68W25 -Estimated size: ~1500 lines of Lean - -Informal statement: -* `Challenge.BudgetedSubmodular0405.approximation` — For a monotone submodular set function F on - finite sets with F of the empty set equal to 0, positive costs, a budget B and a finite ground set - U, the better of the cost-benefit greedy set built from U and the best single item of U that fits - the budget has value at least 0.405 times the value of every subset of U whose total cost is at - most B. --/ - -public section - -namespace Challenge.BudgetedSubmodular0405 - -open Finset - -variable {ι : Type*} [DecidableEq ι] - -/-- A monotone set function with diminishing returns (submodular). -/ -structure MonoSubmodular (F : Finset ι → ℝ) : Prop where - mono : ∀ {S U : Finset ι}, S ⊆ U → F S ≤ F U - dr : ∀ {S U : Finset ι}, S ⊆ U → ∀ x, F (insert x U) - F U ≤ F (insert x S) - F S - -/-- The items of `U` outside `G` that still fit the budget `B` next to `G`. -/ -noncomputable def fits (c : ι → ℝ) (B : ℝ) (U G : Finset ι) : Finset ι := - (U \ G).filter fun x => ∑ y ∈ G, c y + c x ≤ B - -/-- When some item fits, one of them has the largest gain per unit cost. A named theorem rather -than a proof inside `greedyStep`: Lean moves a nested proof into a private auxiliary lemma whose -name carries the module, which no solution module could reproduce. -/ -theorem exists_best (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U G : Finset ι) - (h : (fits c B U G).Nonempty) : - ∃ x ∈ fits c B U G, ∀ y ∈ fits c B U G, - (F (insert y G) - F G) / c y ≤ (F (insert x G) - F G) / c x := - (fits c B U G).exists_max_image _ h - -/-- One greedy step: add an item of `fits` with the largest gain per unit cost (ties broken -arbitrarily); keep `G` when nothing fits. -/ -noncomputable def greedyStep (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U G : Finset ι) : - Finset ι := - if h : (fits c B U G).Nonempty then insert (Classical.choose (exists_best F c B U G h)) G - else G - -/-- The greedy run on the ground set `U`: `U.card` steps from the empty set. -/ -noncomputable def greedy (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U : Finset ι) : Finset ι := - (greedyStep F c B U)^[U.card] ∅ - -/-- The best value of a single item of `U` that fits the budget (`0` when none fits). -/ -noncomputable def bestSingle (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U : Finset ι) : ℝ := - if h : (U.filter fun x => c x ≤ B).Nonempty then - (U.filter fun x => c x ≤ B).sup' h fun x => F {x} - else 0 - -/-- The modified greedy guarantee `0.405` (Tang, Tang, Lim, Han, Li and Yuan 2021, Theorem 2.1: the -exact factor is the root of `(1 - α) log (1 - α) + (2 - 1/e)(1 - 2α) = 0` near `0.4053`). -/ -theorem approximation (F : Finset ι → ℝ) (hF : MonoSubmodular F) (hF0 : F ∅ = 0) - (c : ι → ℝ) (hc : ∀ i, 0 < c i) (B : ℝ) (U O : Finset ι) (hOU : O ⊆ U) - (hOB : ∑ y ∈ O, c y ≤ B) : - (0.405 : ℝ) * F O ≤ max (F (greedy F c B U)) (bestSingle F c B U) := sorry - -end Challenge.BudgetedSubmodular0405 diff --git a/Challenge/Mazur.lean b/Challenge/Mazur.lean deleted file mode 100644 index bfc8c1ffc4..0000000000 --- a/Challenge/Mazur.lean +++ /dev/null @@ -1,47 +0,0 @@ -/- -Copyright (c) 2025 Kevin Buzzard. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kevin Buzzard --/ - -module - -public import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point -public import Mathlib.GroupTheory.Torsion - -/-! -# Mazur's bound on the torsion of an elliptic curve over the rationals - -Source: doi:10.1007/BF02684339, url:https://www.numdam.org/item/?id=PMIHES_1977__47__33_0 -Proposed by: Kevin Buzzard, Vasily Ilin -Open declarations: `Challenge.Mazur.torsion_ncard_le` -Tags: elliptic-curves, torsion, modular-curves, flt-assumption -MSC: 11G05, 11G18 -Estimated size: ~50000 lines of Lean - -Informal statement: -* `Challenge.Mazur.torsion_ncard_le` — For every elliptic curve E over the rationals, the torsion - subgroup of the group of rational points of E, viewed as a set, has at most 16 elements. Set.ncard - returns 0 on an infinite set, so the statement reads "at most 16, or infinite"; that is the form - the FLT project assumes, since finiteness of the torsion subgroup is classical and far easier. --/ - -public section - -namespace Challenge.Mazur - -open scoped WeierstrassCurve.Affine - -/-- **Mazur's torsion theorem**, in the form the Fermat's Last Theorem project assumes it as -`FLT.Assumptions.Mazur_statement`: the torsion subgroup of the group of rational points of an -elliptic curve over `ℚ` has at most 16 elements. Mazur classified the possible torsion -subgroups — cyclic of order `n ≤ 10` or `n = 12`, or `ℤ/2ℤ × ℤ/nℤ` for `n = 2, 4, 6, 8` — and -16 is the largest resulting size. - -`Set.ncard` returns `0` on an infinite set, so this says "at most 16, or infinite". That is -enough for the application, because finiteness of the torsion subgroup is a much easier -classical fact (Mordell--Weil); a solution is welcome to prove finiteness as well. -/ -theorem torsion_ncard_le (E : WeierstrassCurve ℚ) [E.IsElliptic] : - (AddCommGroup.torsion (E⁄ℚ).Point : Set (E⁄ℚ).Point).ncard ≤ 16 := sorry - -end Challenge.Mazur diff --git a/Challenge/McKay.lean b/Challenge/McKay.lean deleted file mode 100644 index fbda45cb73..0000000000 --- a/Challenge/McKay.lean +++ /dev/null @@ -1,55 +0,0 @@ -/- -Copyright (c) 2026 Clawristotle contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Clawristotle contributors --/ - -module - -public import Mathlib.Basic.Complex.Basic -public import Mathlib.GroupTheory.Sylow -public import Mathlib.RepresentationTheory.Character - -/-! -# The McKay conjecture - -Source: arxiv:2410.20392, doi:10.4007/annals.2026.203.3.5 -Proposed by: Vasily Ilin -Open declarations: `Challenge.McKay.card_pPrimeCharacters_eq` -Tags: group-theory, representation-theory, character-theory, mckay-conjecture -MSC: 20C15, 20D20 -Estimated size: ~1000000 lines of Lean - -Informal statement: -* `Challenge.McKay.card_pPrimeCharacters_eq` — For every finite group G, every prime p, and every - Sylow p-subgroup P of G, the set of character functions of simple finite-dimensional complex - representations of G whose dimension p does not divide has the same cardinality as the - corresponding set for the normalizer of P in G. Two simple representations have equal characters - exactly when they are isomorphic, so both sets are in bijection with the sets Irr_p'(G) and - Irr_p'(N_G(P)) that the McKay conjecture counts. --/ - -public section - -open CategoryTheory - -namespace Challenge.McKay - -/-- The irreducible complex characters of `G` of `p'`-degree, as a set of functions: the -characters of simple finite-dimensional complex representations whose dimension is not -divisible by `p`. Two simple representations have equal characters exactly when they are -isomorphic, so this set is in canonical bijection with the set `Irr_{p'}(G)` counted by -the McKay conjecture. -/ -def pPrimeCharacters (G : Type*) [Group G] (p : ℕ) : Set (G → ℂ) := - {χ | ∃ V : FDRep ℂ G, Simple V ∧ V.character = χ ∧ ¬p ∣ Module.finrank ℂ V} - -/-- The **McKay conjecture**, now the theorem of Cabanes and Späth: for every finite -group `G`, every prime `p`, and every Sylow `p`-subgroup `P` of `G`, the irreducible -complex characters of `G` of degree not divisible by `p` are equinumerous with those of -the normalizer of `P` in `G`. -/ -theorem card_pPrimeCharacters_eq (G : Type*) [Group G] [Finite G] (p : ℕ) [Fact p.Prime] - (P : Sylow p G) : - Cardinal.mk (pPrimeCharacters G p) = - Cardinal.mk (pPrimeCharacters (Subgroup.normalizer (P : Set G)) p) := sorry - -end Challenge.McKay diff --git a/Challenge/Odlyzko.lean b/Challenge/Odlyzko.lean deleted file mode 100644 index 71f5357a91..0000000000 --- a/Challenge/Odlyzko.lean +++ /dev/null @@ -1,42 +0,0 @@ -/- -Copyright (c) 2025 Kevin Buzzard. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kevin Buzzard --/ - -module - -public import Mathlib.NumberTheory.NumberField.Discriminant.Defs -public import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex - -/-! -# Odlyzko bound for root discriminants - -Source: url:https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/ -Proposed by: Kevin Buzzard, Vasily Ilin -Open declarations: `Challenge.Odlyzko.abs_discr_ge` -Tags: number-theory, discriminants, number-fields, flt-assumption -MSC: 11R29, 11R42 -Estimated size: ~5000 lines of Lean - -Informal statement: -* `Challenge.Odlyzko.abs_discr_ge` — For a totally complex number field K whose degree over the - rationals is at least 18, the absolute value of the discriminant of K is at least 8.25 raised to - the power of that degree. --/ - -public section - -namespace Challenge.Odlyzko - -open Module NumberField - -/-- An **Odlyzko bound** for the root discriminant of a totally complex number field of degree -18 and above: such a field has root discriminant at least `8.25`. Minkowski's elementary -argument is not strong enough; the bound comes from analysing the zeros of the Dedekind zeta -function of `K`. Stated verbatim as the Fermat's Last Theorem project needs it, where it is -assumed as `FLT.Assumptions.Odlyzko_statement`. -/ -theorem abs_discr_ge (K : Type*) [Field K] [NumberField K] [IsTotallyComplex K] - (hdim : finrank ℚ K ≥ 18) : |(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K := sorry - -end Challenge.Odlyzko diff --git a/Challenge/TestingByBetting.lean b/Challenge/TestingByBetting.lean deleted file mode 100644 index da77105f66..0000000000 --- a/Challenge/TestingByBetting.lean +++ /dev/null @@ -1,51 +0,0 @@ -/- -Copyright (c) 2026 deadczarvc. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: deadczarvc --/ - -module - -public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic -public import Mathlib.Probability.Process.Adapted -public import Mathlib.Probability.Process.Filtration - -/-! -# Ville's inequality for testing by betting - -Source: arxiv:2210.01948 -Proposed by: deadczarvc -Open declarations: `Challenge.TestingByBetting.ville` -Tags: probability, martingales, sequential-testing, e-values -MSC: 60G42, 62L10 -Estimated size: ~400 lines of Lean - -Informal statement: -* `Challenge.TestingByBetting.ville` — Let X₁, X₂, … be real random variables adapted to a - filtration (ℱₙ) on a probability space, with values in [-1, 1], such that the conditional - expectation of Xₙ₊₁ given ℱₙ is at most 0 almost surely for every n. Let λ₁, λ₂, … take values in - [0, 1], with λₙ₊₁ measurable with respect to ℱₙ (predictable stakes), and let Wₙ = ∏_{i < n} (1 + - λᵢ₊₁ Xᵢ₊₁) be the wealth after n rounds (W₀ = 1). Then for every α > 0 the probability that Wₙ ≥ - 1/α for some n is at most α. --/ - -public section - -open MeasureTheory -open scoped ENNReal - -namespace Challenge.TestingByBetting - -/-- Ville's inequality for testing by betting: under the null `E[Xₙ₊₁ | ℱₙ] ≤ 0`, the wealth of a -bettor staking a predictable fraction `λₙ₊₁ ∈ [0, 1]` reaches `1/α` with probability at most `α`. -/ -theorem ville {Ω : Type*} {m0 : MeasurableSpace Ω} - (μ : Measure Ω) [IsProbabilityMeasure μ] (ℱ : Filtration ℕ m0) - (X lam : ℕ → Ω → ℝ) - (hX : Adapted ℱ X) (hXb : ∀ n ω, -1 ≤ X n ω ∧ X n ω ≤ 1) - (hlam : ∀ n, StronglyMeasurable[ℱ n] (lam (n + 1))) (hlamb : ∀ n ω, 0 ≤ lam n ω ∧ lam n ω ≤ 1) - (hnull : ∀ n, μ[X (n + 1) | ℱ n] ≤ᵐ[μ] 0) - {α : ℝ} (hα : 0 < α) : - μ {ω | ∃ n : ℕ, α⁻¹ ≤ ∏ i ∈ Finset.range n, (1 + lam (i + 1) ω * X (i + 1) ω)} - ≤ ENNReal.ofReal α := sorry - -end Challenge.TestingByBetting diff --git a/Challenge/challenges.yml b/Challenge/challenges.yml deleted file mode 100644 index e0c1e4d2be..0000000000 --- a/Challenge/challenges.yml +++ /dev/null @@ -1,332 +0,0 @@ -# Registry of Lean Pool challenges: open statements awaiting a proof. -# -# One entry per challenge. `statements` (and the optional `definitions`) name -# the declarations that may be left as `sorry` in the entry module; every other -# declaration in that file must be closed. `informal` is the natural-language -# statement the Lean is judged against — keep the two saying the same thing. -# -# Regenerate the cards after editing: -# cd python && uv run python -m lean_pool.quality --repo .. --write-challenge-cards -challenges: - - slug: odlyzko-root-discriminant-bound - title: Odlyzko bound for root discriminants - summary: >- - Prove that a totally complex number field of degree at least 18 has - absolute discriminant at least 8.25 raised to the degree — equivalently, - root discriminant at least 8.25. Minkowski's elementary bound is too weak; - the result comes from analysing the zeros of the Dedekind zeta function of - the field, and follows from equation 26 and the table on p17 of Poitou's - 1977 "Sur les petits discriminants". The Fermat's Last Theorem project - assumes it as FLT.Assumptions.Odlyzko_statement (tracking issue #458, - which also links Thomas Browning's notes on an approach); Kevin Buzzard - calls it one of the easiest of the results it assumes, and it is not on - the project's own formalization plan. The line estimate is a guess at the - analytic machinery needed — an explicit formula for the Dedekind zeta - function and the resulting inequality — not at the write-up of the - finished argument. - branch: algebraic number theory - entry_module: Challenge.Odlyzko - proposers: - - Kevin Buzzard - - Vasily Ilin - source: - title: Sur les petits discriminants - authors: - - Georges Poitou - url: https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/ - license: Apache-2.0 - provenance: human - status: solved - solution: - module: Solution.Odlyzko - authors: - - The FLT Project - - √2 - project: odlyzko-bound - estimated_lines: 5000 - statements: - - declaration: Challenge.Odlyzko.abs_discr_ge - informal: >- - For a totally complex number field K whose degree over the rationals - is at least 18, the absolute value of the discriminant of K is at - least 8.25 raised to the power of that degree. - tags: - - number-theory - - discriminants - - number-fields - - flt-assumption - msc: - - "11R29" - - "11R42" - - slug: budgeted-submodular-modified-greedy - title: Modified greedy for budgeted monotone submodular maximisation - summary: >- - Prove that for a monotone submodular set function with F(empty) = 0, - positive item costs and a budget, the better of two candidates - the - cost-benefit greedy set (repeatedly add, among the items that still fit, - one with the largest marginal gain per unit cost) and the best single item - that fits, both drawn from a finite ground set U - has value at least - (1 - 1/e)/2 times that of every subset of U within the budget. This is - the classical guarantee of Khuller, Moss and Naor (budgeted maximum - coverage, 1999), recalled for monotone submodular - functions by Tang et al. (2021), who also closed a gap in the often-quoted - 1 - 1/sqrt(e) and proved 0.405 for the same algorithm. It is - the standard model for choosing what fits a size limit - sensor - placement, summarisation, context selection for language-model agents. - Mathlib proves submodularity of matroid rank but has no general - submodular set functions and no greedy approximation results. - The estimate covers the Khuller-Moss-Naor prefix lemma (each greedy pick - closes a cost-proportional share of the gap to the optimum), the case - split at the first optimal item the greedy rejects for budget, and the - maximum with the best single item. - branch: combinatorial optimization - entry_module: Challenge.BudgetedSubmodular - proposers: - - Mikhail Nemerov - source: - title: Revisiting Modified Greedy Algorithm for Monotone Submodular Maximization with a Knapsack Constraint - authors: - - Jing Tang - - Xueyan Tang - - Andrew Lim - - Kai Han - - Chongshou Li - - Junsong Yuan - doi: "10.1145/3447386" - url: https://arxiv.org/abs/2008.05391 - license: Apache-2.0 - provenance: mix - status: solved - solution: - module: Solution.BudgetedSubmodular - authors: - - deadczarvc - estimated_lines: 600 - statements: - - declaration: Challenge.BudgetedSubmodular.modifiedGreedy_approx - informal: >- - For a monotone submodular set function F on finite sets with F of the - empty set equal to 0, positive costs, a budget B and a finite ground - set U, the better of the cost-benefit greedy set built from U and the - best single item of U that fits the budget has value at least - (1 - 1/e)/2 times the value of every subset of U whose total cost is - at most B. - tags: - - combinatorics - - optimization - - approximation-algorithms - - submodular-functions - msc: - - "90C27" - - "68W25" - - slug: budgeted-submodular-modified-greedy-0405 - title: The 0.405 factor of modified greedy for budgeted submodular maximisation - summary: >- - Prove that for a monotone submodular set function with F(empty) = 0, - positive item costs and a budget, the better of the cost-benefit greedy - set (repeatedly add, among the items that still fit, one with the largest - marginal gain per unit cost) and the best single item that fits, both - drawn from a finite ground set U, has value at least 0.405 times that of - every subset of U within the budget. This is Theorem 2.1 of Tang et al. - (2021): the exact factor is the root near 0.4053 of - (1 - a) log(1 - a) + (2 - 1/e)(1 - 2a) = 0, above the classical - (1 - 1/e)/2 of Khuller, Moss and Naor (proved here as - budgeted-submodular-modified-greedy) and the often-quoted 1 - 1/sqrt(e), - whose original proof had a gap. The algorithm and definitions are the same - as in budgeted-submodular-modified-greedy. The estimate covers the - relations at the first and second optimal items the greedy rejects for - budget, the bound for the marginal function on the remaining optimum, and - the minimisation of the resulting two-variable bound. - branch: combinatorial optimization - entry_module: Challenge.BudgetedSubmodular0405 - proposers: - - Mikhail Nemerov - source: - title: Revisiting Modified Greedy Algorithm for Monotone Submodular Maximization with a Knapsack Constraint - authors: - - Jing Tang - - Xueyan Tang - - Andrew Lim - - Kai Han - - Chongshou Li - - Junsong Yuan - doi: "10.1145/3447386" - url: https://arxiv.org/abs/2008.05391 - license: Apache-2.0 - provenance: mix - status: open - estimated_lines: 1500 - statements: - - declaration: Challenge.BudgetedSubmodular0405.approximation - informal: >- - For a monotone submodular set function F on finite sets with F of the - empty set equal to 0, positive costs, a budget B and a finite ground - set U, the better of the cost-benefit greedy set built from U and the - best single item of U that fits the budget has value at least 0.405 - times the value of every subset of U whose total cost is at most B. - tags: - - combinatorics - - optimization - - approximation-algorithms - - submodular-functions - msc: - - "90C27" - - "68W25" - - slug: mazur-torsion-bound - title: Mazur's bound on the torsion of an elliptic curve over the rationals - summary: >- - Prove that the torsion subgroup of the group of rational points of an - elliptic curve over the rationals has at most 16 elements. This is the - numerical consequence of Mazur's 1977 classification of the possible - torsion subgroups — cyclic of order at most 10 or of order 12, and - Z/2Z x Z/nZ for n = 2, 4, 6, 8 — proved in "Modular curves and the - Eisenstein ideal" by descent on the Eisenstein quotient of the Jacobian - of a modular curve of prime level. Every known proof of Fermat's Last - Theorem uses it, and the FLT project assumes it as - FLT.Assumptions.Mazur_statement (tracking issue #477); it is not on the - project's own formalization plan. The line estimate reflects that Mathlib - has none of the modular-curve machinery a proof needs, so it is an - estimate of a programme rather than of a single development; a solution - via the winding quotient and known partial results towards - Birch-Swinnerton-Dyer may be shorter than Mazur's own route. - branch: arithmetic geometry - entry_module: Challenge.Mazur - proposers: - - Kevin Buzzard - - Vasily Ilin - source: - title: Modular curves and the Eisenstein ideal - authors: - - Barry Mazur - doi: "10.1007/BF02684339" - url: https://www.numdam.org/item/?id=PMIHES_1977__47__33_0 - license: Apache-2.0 - provenance: human - status: open - estimated_lines: 50000 - statements: - - declaration: Challenge.Mazur.torsion_ncard_le - informal: >- - For every elliptic curve E over the rationals, the torsion subgroup of - the group of rational points of E, viewed as a set, has at most 16 - elements. Set.ncard returns 0 on an infinite set, so the statement - reads "at most 16, or infinite"; that is the form the FLT project - assumes, since finiteness of the torsion subgroup is classical and far - easier. - tags: - - elliptic-curves - - torsion - - modular-curves - - flt-assumption - msc: - - "11G05" - - "11G18" - - slug: mckay-conjecture - title: The McKay conjecture - summary: >- - Prove the McKay conjecture: for every finite group G, every prime p, and - every Sylow p-subgroup P of G, the number of irreducible complex - characters of G of degree not divisible by p equals the same count for - the normalizer of P in G. Conjectured by McKay in 1972 and proved in - full by Cabanes and Späth (Annals of Mathematics, 2026) by completing - the Isaacs–Malle–Navarro programme: the conjecture reduces to the - inductive McKay condition for quasisimple groups, whose verification - rests on the classification of finite simple groups and on - Deligne–Lusztig theory. Irreducible characters are counted as character - functions of simple finite-dimensional complex representations, which - identifies exactly the isomorphism classes. The line estimate is a - guess at that programme — the character theory Mathlib is missing, the - reduction theorem, the classification, and the case-by-case - verification — not at any single write-up. - branch: group theory - entry_module: Challenge.McKay - proposers: - - Vasily Ilin - source: - title: The McKay Conjecture on character degrees - authors: - - Marc Cabanes - - Britta Späth - arxiv: "2410.20392" - doi: "10.4007/annals.2026.203.3.5" - license: Apache-2.0 - provenance: AI - status: open - estimated_lines: 1000000 - statements: - - declaration: Challenge.McKay.card_pPrimeCharacters_eq - informal: >- - For every finite group G, every prime p, and every Sylow p-subgroup - P of G, the set of character functions of simple finite-dimensional - complex representations of G whose dimension p does not divide has - the same cardinality as the corresponding set for the normalizer of - P in G. Two simple representations have equal characters exactly - when they are isomorphic, so both sets are in bijection with the - sets Irr_p'(G) and Irr_p'(N_G(P)) that the McKay conjecture counts. - tags: - - group-theory - - representation-theory - - character-theory - - mckay-conjecture - msc: - - "20C15" - - "20D20" - - slug: ville-testing-by-betting - title: Ville's inequality for testing by betting - summary: >- - Prove the type-I error guarantee of testing by betting: if outcomes in - [-1, 1] have conditional mean at most 0 given the past, a bettor who - stakes a predictable fraction in [0, 1] of the current wealth reaches - wealth 1/alpha with probability at most alpha, at any time. The wealth - process is a nonnegative supermartingale started at 1, so this is - Ville's 1939 maximal inequality, the result behind e-processes, - confidence sequences and safe anytime-valid inference (Ramdas, - Grünwald, Vovk and Shafer, arXiv 2210.01948). Mathlib has Doob's maximal - inequality for nonnegative submartingales (MeasureTheory.maximal_ineq) - but no supermartingale (Ville) form and nothing on betting wealth - processes. A finite-horizon, finite-support special case — outcome laws - may depend on the past, stakes are predictable — is proved sorry-free - by first-step analysis in the proposer's notes; a measure-theoretic - Ville inequality exists in the third-party repository - Robby955/formal-martingales. The line estimate covers the supermartingale - property of the wealth process, optional stopping at the hitting time, - and the passage from finite to infinite horizon. - branch: probability - entry_module: Challenge.TestingByBetting - proposers: - - deadczarvc - source: - title: Game-theoretic statistics and safe anytime-valid inference - authors: - - Aaditya Ramdas - - Peter Grünwald - - Vladimir Vovk - - Glenn Shafer - arxiv: "2210.01948" - license: Apache-2.0 - provenance: AI - status: solved - solution: - module: Solution.TestingByBetting - authors: - - deadczarvc - estimated_lines: 400 - statements: - - declaration: Challenge.TestingByBetting.ville - informal: >- - Let X₁, X₂, … be real random variables adapted to a filtration (ℱₙ) - on a probability space, with values in [-1, 1], such that the - conditional expectation of Xₙ₊₁ given ℱₙ is at most 0 almost surely - for every n. Let λ₁, λ₂, … take values in [0, 1], with λₙ₊₁ - measurable with respect to ℱₙ (predictable stakes), and let - Wₙ = ∏_{i < n} (1 + λᵢ₊₁ Xᵢ₊₁) be the wealth after n rounds - (W₀ = 1). Then for every α > 0 the probability that Wₙ ≥ 1/α for - some n is at most α. - tags: - - probability - - martingales - - sequential-testing - - e-values - msc: - - "60G42" - - "62L10" diff --git a/Solution.lean b/Solution.lean deleted file mode 100644 index cb46abb570..0000000000 --- a/Solution.lean +++ /dev/null @@ -1,5 +0,0 @@ -module -- shake: keep-all --deprecated_module: ignore - -public import Solution.BudgetedSubmodular -public import Solution.Odlyzko -public import Solution.TestingByBetting diff --git a/Solution/BudgetedSubmodular.lean b/Solution/BudgetedSubmodular.lean deleted file mode 100644 index af95910432..0000000000 --- a/Solution/BudgetedSubmodular.lean +++ /dev/null @@ -1,342 +0,0 @@ -/- -Copyright (c) 2026 deadczarvc. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: deadczarvc --/ - -module - -public import Mathlib.Analysis.SpecialFunctions.Exp -public import Mathlib.Algebra.Order.BigOperators.Group.Finset - -/-! -# Solution: Modified greedy for budgeted monotone submodular maximisation - -Challenge: `budgeted-submodular-modified-greedy` (`Challenge.BudgetedSubmodular`) -Proves: `Challenge.BudgetedSubmodular.modifiedGreedy_approx` -Solved by: deadczarvc - -This module restates the challenge statement under its own name and proves it. It must not import -the challenge module: comparator exports both environments separately and checks that the statements -agree, which is what makes the verdict independent of the statement file. --/ - -/-! -## Proof outline (Khuller, Moss and Naor) - -1. If the optimum `O` lies inside the greedy set, monotonicity finishes. -2. Otherwise let `l` be the first step at which the best item `y` of `O` outside the greedy - set (by marginal gain per unit cost) no longer fits the budget. Before `l`, every greedy pick - has gain per cost at least that of every item of `O`, and submodularity gives - `F O - F G' ≤ (1 - c x / B) * (F O - F G) ≤ exp (-c x / B) * (F O - F G)`, so after the - prefix `F O - F G_l ≤ exp (-c(G_l) / B) * F O`. -3. One virtual step with `y` costs more than `B` in total, so - `F O - F (insert y G_l) ≤ exp (-1) * F O`. -4. Submodularity splits the virtual set: `F (insert y G_l) ≤ F G_l + F {y}`, where `F G_l` is at - most the greedy value and `F {y}` at most the best single item. Hence `(1 - 1/e) * F O` is at - most their sum, and the larger of the two is at least half of it. --/ - -public section - -namespace Challenge.BudgetedSubmodular - -open Finset - -variable {ι : Type*} [DecidableEq ι] - -/-- A monotone set function with diminishing returns (submodular). -/ -structure MonoSubmodular (F : Finset ι → ℝ) : Prop where - mono : ∀ {S U : Finset ι}, S ⊆ U → F S ≤ F U - dr : ∀ {S U : Finset ι}, S ⊆ U → ∀ x, F (insert x U) - F U ≤ F (insert x S) - F S - -/-- The items of `U` outside `G` that still fit the budget `B` next to `G`. -/ -noncomputable def fits (c : ι → ℝ) (B : ℝ) (U G : Finset ι) : Finset ι := - (U \ G).filter fun x => ∑ y ∈ G, c y + c x ≤ B - -/-- When some item fits, one of them has the largest gain per unit cost. A named theorem rather -than a proof inside `greedyStep`: Lean moves a nested proof into a private auxiliary lemma whose -name carries the module, which no solution module could reproduce. -/ -theorem exists_best (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U G : Finset ι) - (h : (fits c B U G).Nonempty) : - ∃ x ∈ fits c B U G, ∀ y ∈ fits c B U G, - (F (insert y G) - F G) / c y ≤ (F (insert x G) - F G) / c x := - (fits c B U G).exists_max_image _ h - -/-- One greedy step: add an item of `fits` with the largest gain per unit cost (ties broken -arbitrarily); keep `G` when nothing fits. -/ -noncomputable def greedyStep (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U G : Finset ι) : - Finset ι := - if h : (fits c B U G).Nonempty then insert (Classical.choose (exists_best F c B U G h)) G - else G - -/-- The greedy run on the ground set `U`: `U.card` steps from the empty set. -/ -noncomputable def greedy (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U : Finset ι) : Finset ι := - (greedyStep F c B U)^[U.card] ∅ - -/-- The best value of a single item of `U` that fits the budget (`0` when none fits). -/ -noncomputable def bestSingle (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U : Finset ι) : ℝ := - if h : (U.filter fun x => c x ≤ B).Nonempty then - (U.filter fun x => c x ≤ B).sup' h fun x => F {x} - else 0 - -section Proof - -variable {F : Finset ι → ℝ} {c : ι → ℝ} {B : ℝ} {U : Finset ι} - -/-- Gain per unit cost of adding `x` to `G`. -/ -private noncomputable def ratio (F : Finset ι → ℝ) (c : ι → ℝ) (G : Finset ι) (x : ι) : ℝ := - (F (insert x G) - F G) / c x - -private lemma ratio_nonneg (hF : MonoSubmodular F) (hc : ∀ i, 0 < c i) (G : Finset ι) (x : ι) : - 0 ≤ ratio F c G x := - div_nonneg (sub_nonneg.2 (hF.mono (subset_insert x G))) (hc x).le - -private lemma ratio_of_mem {G : Finset ι} {x : ι} (hx : x ∈ G) : ratio F c G x = 0 := by - simp [ratio, insert_eq_of_mem hx] - -/-- The greedy pick when something fits: it fits and has the best ratio among what fits. -/ -private lemma step_pos {G : Finset ι} (h : (fits c B U G).Nonempty) : - ∃ x ∈ fits c B U G, (∀ z ∈ fits c B U G, ratio F c G z ≤ ratio F c G x) ∧ - greedyStep F c B U G = insert x G := by - have hs := Classical.choose_spec - ((fits c B U G).exists_max_image (fun x => (F (insert x G) - F G) / c x) h) - exact ⟨_, hs.1, fun z hz => hs.2 z hz, by simp [greedyStep, h]⟩ - -private lemma step_neg {G : Finset ι} (h : ¬ (fits c B U G).Nonempty) : - greedyStep F c B U G = G := by - simp [greedyStep, h] - -private lemma mem_fits {G : Finset ι} {x : ι} : - x ∈ fits c B U G ↔ x ∈ U ∧ x ∉ G ∧ ∑ y ∈ G, c y + c x ≤ B := by - simp [fits, and_assoc] - -private lemma subset_step (G : Finset ι) : G ⊆ greedyStep F c B U G := by - by_cases h : (fits c B U G).Nonempty - · obtain ⟨x, -, -, hx⟩ := step_pos (F := F) h - rw [hx]; exact subset_insert x G - · rw [step_neg h] - -/-- The greedy after `k` steps. -/ -private noncomputable def run (F : Finset ι → ℝ) (c : ι → ℝ) (B : ℝ) (U : Finset ι) (k : ℕ) : - Finset ι := - (greedyStep F c B U)^[k] ∅ - -private lemma run_succ (k : ℕ) : run F c B U (k + 1) = greedyStep F c B U (run F c B U k) := by - simp [run, Function.iterate_succ_apply'] - -private lemma run_mono {j k : ℕ} (hjk : j ≤ k) : run F c B U j ⊆ run F c B U k := by - induction hjk with - | refl => exact Subset.rfl - | step _ ih => exact ih.trans (by rw [run_succ]; exact subset_step _) - -private lemma run_sub (k : ℕ) : run F c B U k ⊆ U := by - induction k with - | zero => simp [run] - | succ k ih => - rw [run_succ] - by_cases h : (fits c B U (run F c B U k)).Nonempty - · obtain ⟨x, hx, -, he⟩ := step_pos (F := F) h - rw [he]; exact insert_subset (mem_fits.1 hx).1 ih - · rw [step_neg h]; exact ih - -/-- Once nothing fits, the greedy stays put. -/ -private lemma run_stable {k : ℕ} (h : ¬ (fits c B U (run F c B U k)).Nonempty) (m : ℕ) : - run F c B U (k + m) = run F c B U k := by - induction m with - | zero => rfl - | succ m ih => rw [← add_assoc, run_succ, ih, step_neg h] - -/-- After `U.card` steps nothing fits any more. -/ -private lemma run_done : ¬ (fits c B U (run F c B U U.card)).Nonempty := by - intro hN - have hcard : ∀ k ≤ U.card, (run F c B U k).card = k := by - intro k hk - induction k with - | zero => simp [run] - | succ k ih => - have hk' : k ≤ U.card := Nat.le_of_succ_le hk - by_cases h : (fits c B U (run F c B U k)).Nonempty - · obtain ⟨x, hx, -, he⟩ := step_pos (F := F) h - rw [run_succ, he, card_insert_of_notMem (mem_fits.1 hx).2.1, ih hk'] - · exfalso - have := run_stable (F := F) h (U.card - k) - rw [Nat.add_sub_cancel' hk'] at this - exact h (this ▸ hN) - have hU : run F c B U U.card = U := - eq_of_subset_of_card_le (run_sub _) (by rw [hcard _ le_rfl]) - obtain ⟨x, hx⟩ := hN - exact (mem_fits.1 hx).2.1 (by rw [hU]; exact (mem_fits.1 hx).1) - -private lemma greedy_eq : greedy F c B U = run F c B U U.card := rfl - -/-- Adding a whole set gains at most the sum of the single gains. -/ -private lemma union_le (hF : MonoSubmodular F) (S O : Finset ι) : - F (S ∪ O) ≤ F S + ∑ y ∈ O, (F (insert y S) - F S) := by - induction O using Finset.induction_on with - | empty => simp - | insert a O ha ih => - rw [union_insert, sum_insert ha] - have h1 := hF.dr (subset_union_left : S ⊆ S ∪ O) a - linarith - -/-- One step against the optimum: a pick whose ratio beats every item of `O` closes `c x / B` -of the gap. -/ -private lemma step_bound (hF : MonoSubmodular F) (hc : ∀ i, 0 < c i) (hB : 0 < B) (G O : Finset ι) - (hO : ∑ y ∈ O, c y ≤ B) (x : ι) (hx : ∀ y ∈ O, ratio F c G y ≤ ratio F c G x) : - c x / B * (F O - F G) ≤ F (insert x G) - F G := by - set r := ratio F c G x with hr_def - have hgain : ∀ y ∈ O, F (insert y G) - F G ≤ r * c y := fun y hy => by - have := hx y hy - rwa [ratio, div_le_iff₀ (hc y)] at this - have h1 : F O ≤ F (G ∪ O) := hF.mono subset_union_right - have h2 := union_le hF G O - have h3 : ∑ y ∈ O, (F (insert y G) - F G) ≤ r * ∑ y ∈ O, c y := by - rw [mul_sum]; exact sum_le_sum hgain - have hr : 0 ≤ r := ratio_nonneg hF hc G x - have h4 : r * ∑ y ∈ O, c y ≤ r * B := mul_le_mul_of_nonneg_left hO hr - have h5 : F O - F G ≤ r * B := by linarith - have h6 : c x / B * (F O - F G) ≤ c x / B * (r * B) := - mul_le_mul_of_nonneg_left h5 (div_nonneg (hc x).le hB.le) - have h7 : c x / B * (r * B) = F (insert x G) - F G := by - rw [hr_def, ratio]; field_simp [(hc x).ne', hB.ne'] - linarith - -/-- The gap after one step that closes `t` of it, with `0 ≤ t`. -/ -private lemma gap_step {gap gap' E t opt : ℝ} (hstep : gap' ≤ (1 - t) * gap) (ht : t ≤ 1) - (hgap : gap ≤ E * opt) (hE : 0 ≤ E * opt) : gap' ≤ Real.exp (-t) * (E * opt) := by - have h1 : (1 - t) * gap ≤ (1 - t) * (E * opt) := mul_le_mul_of_nonneg_left hgap (by linarith) - have h2 : (1 - t) * (E * opt) ≤ Real.exp (-t) * (E * opt) := - mul_le_mul_of_nonneg_right (by linarith [Real.add_one_le_exp (-t)]) hE - linarith - -end Proof - -/-- The modified greedy guarantee `(1 - 1/e)/2` (Khuller–Moss–Naor 1999; see Tang et al. 2021, -who prove `0.405` for the same algorithm). -/ -theorem modifiedGreedy_approx (F : Finset ι → ℝ) (hF : MonoSubmodular F) (hF0 : F ∅ = 0) - (c : ι → ℝ) (hc : ∀ i, 0 < c i) (B : ℝ) (U O : Finset ι) (hOU : O ⊆ U) - (hOB : ∑ y ∈ O, c y ≤ B) : - (1 - Real.exp (-1)) / 2 * F O ≤ max (F (greedy F c B U)) (bestSingle F c B U) := by - classical - have hopt : 0 ≤ F O := hF0 ▸ hF.mono (empty_subset O) - have hexp1 : Real.exp (-1) ≤ 1 := Real.exp_le_one_iff.2 (by norm_num) - have hexp0 : 0 < Real.exp (-1) := Real.exp_pos _ - rw [greedy_eq] - -- the optimum inside the greedy set: done - by_cases hsub : O ⊆ run F c B U U.card - · have h1 := hF.mono hsub - have h2 : (1 - Real.exp (-1)) / 2 * F O ≤ F O := by nlinarith - exact (h2.trans h1).trans (le_max_left _ _) - have hB : 0 < B := by - obtain ⟨y, hy⟩ : O.Nonempty := by - rcases O.eq_empty_or_nonempty with h | h - · exact absurd (h ▸ empty_subset _) hsub - · exact h - linarith [hc y, single_le_sum (fun i _ => (hc i).le) hy (f := c)] - -- Q j: the best item of O outside the greedy set after j steps does not fit - let Q : ℕ → Prop := fun j => ∃ y ∈ O \ run F c B U j, - (∀ z ∈ O \ run F c B U j, ratio F c (run F c B U j) z ≤ ratio F c (run F c B U j) y) ∧ - B < ∑ x ∈ run F c B U j, c x + c y - have hQN : Q U.card := by - obtain ⟨y, hy, hmax⟩ := (O \ run F c B U U.card).exists_max_image - (ratio F c (run F c B U U.card)) (sdiff_nonempty.2 hsub) - refine ⟨y, hy, hmax, ?_⟩ - by_contra hle - push Not at hle - exact run_done (F := F) ⟨y, mem_fits.2 ⟨hOU (mem_sdiff.1 hy).1, (mem_sdiff.1 hy).2, hle⟩⟩ - have hex : ∃ j, Q j := ⟨_, hQN⟩ - set l := Nat.find hex with hl_def - have hl : Q l := Nat.find_spec hex - have hlN : l ≤ U.card := Nat.find_min' hex hQN - have hbefore : ∀ j < l, ¬ Q j := fun j hj => Nat.find_min hex hj - -- until l, every greedy pick beats every item of O: the gap shrinks by exp (-cost / B) - have inv : ∀ j ≤ l, F O - F (run F c B U j) ≤ - Real.exp (-(∑ x ∈ run F c B U j, c x) / B) * F O := by - intro j hj - induction j with - | zero => simp [run, hF0] - | succ j ih => - have hjl : j < l := hj - have ihj := ih hjl.le - have hnq := hbefore j hjl - by_cases hfit : (fits c B U (run F c B U j)).Nonempty - · obtain ⟨x, hx, hxmax, hstep⟩ := step_pos (F := F) hfit - have hxm := mem_fits.1 hx - have hdom : ∀ y ∈ O, ratio F c (run F c B U j) y ≤ ratio F c (run F c B U j) x := by - intro y hy - by_cases hyG : y ∈ run F c B U j - · rw [ratio_of_mem hyG]; exact ratio_nonneg hF hc _ _ - · obtain ⟨y', hy', hmax'⟩ := (O \ run F c B U j).exists_max_image - (ratio F c (run F c B U j)) ⟨y, mem_sdiff.2 ⟨hy, hyG⟩⟩ - have hfit' : ∑ z ∈ run F c B U j, c z + c y' ≤ B := by - by_contra h - push Not at h - exact hnq ⟨y', hy', hmax', h⟩ - have hy'f : y' ∈ fits c B U (run F c B U j) := - mem_fits.2 ⟨hOU (mem_sdiff.1 hy').1, (mem_sdiff.1 hy').2, hfit'⟩ - exact (hmax' y (mem_sdiff.2 ⟨hy, hyG⟩)).trans (hxmax y' hy'f) - have hsb := step_bound hF hc hB _ O hOB x hdom - have hcx : c x ≤ B := by - have : 0 ≤ ∑ z ∈ run F c B U j, c z := sum_nonneg fun i _ => (hc i).le - linarith [hxm.2.2] - rw [run_succ, hstep, sum_insert hxm.2.1] - have hE : 0 ≤ Real.exp (-(∑ z ∈ run F c B U j, c z) / B) * F O := - mul_nonneg (Real.exp_pos _).le hopt - have hlin : F O - F (insert x (run F c B U j)) ≤ - (1 - c x / B) * (F O - F (run F c B U j)) := by - have : (1 - c x / B) * (F O - F (run F c B U j)) = - (F O - F (run F c B U j)) - c x / B * (F O - F (run F c B U j)) := by ring - linarith - have h := gap_step hlin (by rw [div_le_one hB]; exact hcx) ihj hE - calc F O - F (insert x (run F c B U j)) - ≤ Real.exp (-(c x / B)) * (Real.exp (-(∑ z ∈ run F c B U j, c z) / B) * F O) := h - _ = Real.exp (-(c x + ∑ z ∈ run F c B U j, c z) / B) * F O := by - rw [← mul_assoc, ← Real.exp_add]; congr 2; ring - · rw [run_succ, step_neg hfit] - exact ihj - -- a virtual step with the best item of O at l pushes the cost past B - obtain ⟨y, hy, hmax, hover⟩ := hl - have hym := mem_sdiff.1 hy - have hdom : ∀ z ∈ O, ratio F c (run F c B U l) z ≤ ratio F c (run F c B U l) y := by - intro z hz - by_cases hzG : z ∈ run F c B U l - · rw [ratio_of_mem hzG]; exact ratio_nonneg hF hc _ _ - · exact hmax z (mem_sdiff.2 ⟨hz, hzG⟩) - have hsb := step_bound hF hc hB _ O hOB y hdom - have hcy : c y ≤ B := (single_le_sum (fun i _ => (hc i).le) hym.1).trans hOB - have hE : 0 ≤ Real.exp (-(∑ z ∈ run F c B U l, c z) / B) * F O := - mul_nonneg (Real.exp_pos _).le hopt - have hlin : F O - F (insert y (run F c B U l)) ≤ (1 - c y / B) * (F O - F (run F c B U l)) := by - have : (1 - c y / B) * (F O - F (run F c B U l)) = - (F O - F (run F c B U l)) - c y / B * (F O - F (run F c B U l)) := by ring - linarith - have hvirt := gap_step hlin (by rw [div_le_one hB]; exact hcy) (inv l le_rfl) hE - have hcost : Real.exp (-(c y / B)) * (Real.exp (-(∑ z ∈ run F c B U l, c z) / B) * F O) ≤ - Real.exp (-1) * F O := by - rw [← mul_assoc, ← Real.exp_add] - apply mul_le_mul_of_nonneg_right _ hopt - apply Real.exp_le_exp.2 - have h1 : 1 < (∑ z ∈ run F c B U l, c z + c y) / B := (one_lt_div hB).2 hover - have h2 : -(c y / B) + -(∑ z ∈ run F c B U l, c z) / B = - -((∑ z ∈ run F c B U l, c z + c y) / B) := by ring - linarith - -- submodularity splits the virtual set into the greedy prefix and one item - have hsplit : F (insert y (run F c B U l)) ≤ F (run F c B U l) + F {y} := by - have := hF.dr (empty_subset (run F c B U l)) y - simp only [insert_empty, hF0] at this - linarith - have hGl : F (run F c B U l) ≤ F (run F c B U U.card) := hF.mono (run_mono hlN) - have hsingle : F {y} ≤ bestSingle F c B U := by - have hmem : y ∈ U.filter fun x => c x ≤ B := mem_filter.2 ⟨hOU hym.1, hcy⟩ - rw [bestSingle, dite_eq_left_of_eq_true (eq_true ⟨y, hmem⟩)] - exact le_sup' (fun x => F {x}) hmem - have hsum : (1 - Real.exp (-1)) * F O ≤ F (run F c B U U.card) + bestSingle F c B U := by - linarith - have h2 := le_max_left (F (run F c B U U.card)) (bestSingle F c B U) - have h3 := le_max_right (F (run F c B U U.card)) (bestSingle F c B U) - linarith - - - -end Challenge.BudgetedSubmodular diff --git a/Solution/Odlyzko.lean b/Solution/Odlyzko.lean deleted file mode 100644 index e5e477b292..0000000000 --- a/Solution/Odlyzko.lean +++ /dev/null @@ -1,40 +0,0 @@ -/- -Copyright (c) 2026 The FLT Project. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: The FLT Project, √2 --/ - -module - -public import LeanPool.Odlyzko - -/-! -# Solution: Odlyzko bound for root discriminants - -Challenge: `odlyzko-root-discriminant-bound` (`Challenge.Odlyzko`) -Proves: `Challenge.Odlyzko.abs_discr_ge` -Solved by: The FLT Project, √2 -Pool project: `odlyzko-bound` - -This module restates the challenge statement under its own name and proves it. It must not import -the challenge module: comparator exports both environments separately and checks that the statements -agree, which is what makes the verdict independent of the statement file. --/ - -/-! -# Solution to the Odlyzko root-discriminant challenge --/ - -public section - -namespace Challenge.Odlyzko - -open Module NumberField - -/-- A totally complex number field of degree at least 18 has absolute -discriminant at least `8.25` raised to its degree. -/ -theorem abs_discr_ge (K : Type*) [Field K] [NumberField K] [IsTotallyComplex K] - (hdim : finrank ℚ K ≥ 18) : |(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K := - NumberField.Odlyzko.odlyzkoBound K hdim - -end Challenge.Odlyzko diff --git a/Solution/TestingByBetting.lean b/Solution/TestingByBetting.lean deleted file mode 100644 index cf4572b4fa..0000000000 --- a/Solution/TestingByBetting.lean +++ /dev/null @@ -1,187 +0,0 @@ -/- -Copyright (c) 2026 deadczarvc. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: deadczarvc --/ - -module - -public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset -public import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut -public import Mathlib.Probability.Martingale.OptionalStopping - -/-! -# Solution: Ville's inequality for testing by betting - -Challenge: `ville-testing-by-betting` (`Challenge.TestingByBetting`) -Proves: `Challenge.TestingByBetting.ville` -Solved by: deadczarvc - -This module restates the challenge statement under its own name and proves it. It must not import -the challenge module: comparator exports both environments separately and checks that the statements -agree, which is what makes the verdict independent of the statement file. --/ - -/-! -## Proof outline - -1. The wealth `W n = ∏ i < n, (1 + lam (i + 1) * X (i + 1))` is adapted, satisfies - `0 ≤ W n ≤ 2 ^ n`, and is a supermartingale: pulling the `ℱ n`-measurable factor out of the - conditional expectation gives - `E[W (n + 1) | ℱ n] = W n + W n * lam (n + 1) * E[X (n + 1) | ℱ n]`, - which is at most `W n` under the null. -2. Finite horizon: optional stopping at the hitting time of `[c, ∞)` before `N` gives - `E[W τ] ≤ E[W 0] = 1`, and Markov's inequality gives `c * P(∃ n ≤ N, c ≤ W n) ≤ 1`. -3. Infinite horizon: continuity of the measure from below over `N`, with `c = α⁻¹`. --/ - -public section - -open MeasureTheory -open scoped ENNReal - -namespace Challenge.TestingByBetting - -section Helpers - -variable {Ω : Type*} {m0 : MeasurableSpace Ω} - -/-- Wealth after `n` rounds of betting the predictable fraction `lam (i + 1)` on `X (i + 1)`. -/ -private noncomputable def wealth (X lam : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ := - ∏ i ∈ Finset.range n, (1 + lam (i + 1) ω * X (i + 1) ω) - -private lemma wealth_succ (X lam : ℕ → Ω → ℝ) (n : ℕ) : - wealth X lam (n + 1) = fun ω => wealth X lam n ω * (1 + lam (n + 1) ω * X (n + 1) ω) := by - funext ω - simp [wealth, Finset.prod_range_succ] - -private lemma factor_mem {x l : ℝ} (hx : -1 ≤ x ∧ x ≤ 1) (hl : 0 ≤ l ∧ l ≤ 1) : - 0 ≤ 1 + l * x ∧ 1 + l * x ≤ 2 := by - constructor <;> nlinarith [mul_nonneg hl.1 (show 0 ≤ x + 1 by linarith), - mul_nonneg hl.1 (show 0 ≤ 1 - x by linarith)] - -private lemma wealth_nonneg {X lam : ℕ → Ω → ℝ} (hXb : ∀ n ω, -1 ≤ X n ω ∧ X n ω ≤ 1) - (hlamb : ∀ n ω, 0 ≤ lam n ω ∧ lam n ω ≤ 1) (n : ℕ) (ω : Ω) : 0 ≤ wealth X lam n ω := - Finset.prod_nonneg fun i _ => (factor_mem (hXb (i + 1) ω) (hlamb (i + 1) ω)).1 - -private lemma wealth_le {X lam : ℕ → Ω → ℝ} (hXb : ∀ n ω, -1 ≤ X n ω ∧ X n ω ≤ 1) - (hlamb : ∀ n ω, 0 ≤ lam n ω ∧ lam n ω ≤ 1) (n : ℕ) (ω : Ω) : wealth X lam n ω ≤ 2 ^ n := by - calc wealth X lam n ω ≤ ∏ _i ∈ Finset.range n, (2 : ℝ) := - Finset.prod_le_prod₀ (fun i _ => (factor_mem (hXb (i + 1) ω) (hlamb (i + 1) ω)).1) - (fun i _ => (factor_mem (hXb (i + 1) ω) (hlamb (i + 1) ω)).2) - _ = 2 ^ n := by simp - -private lemma wealth_stronglyMeasurable {ℱ : Filtration ℕ m0} {X lam : ℕ → Ω → ℝ} - (hX : Adapted ℱ X) (hlam : ∀ n, StronglyMeasurable[ℱ n] (lam (n + 1))) (n : ℕ) : - StronglyMeasurable[ℱ n] (wealth X lam n) := by - induction n with - | zero => - have h0 : wealth X lam 0 = fun _ => (1 : ℝ) := by funext ω; simp [wealth] - rw [h0]; exact stronglyMeasurable_const - | succ n ih => - rw [wealth_succ] - refine (ih.mono (ℱ.mono n.le_succ)).mul (stronglyMeasurable_const.add ?_) - exact ((hlam n).mono (ℱ.mono n.le_succ)).mul (hX (n + 1)).stronglyMeasurable - -private lemma integrable_of_bounded {μ : Measure Ω} [IsProbabilityMeasure μ] {f : Ω → ℝ} - {m : MeasurableSpace Ω} (hm : m ≤ m0) (hf : StronglyMeasurable[m] f) (C : ℝ) - (hC : ∀ ω, |f ω| ≤ C) : Integrable f μ := - Integrable.of_bound (hf.mono hm).aestronglyMeasurable C (Filter.Eventually.of_forall hC) - -/-- The wealth process is a supermartingale under the null `E[X (n + 1) | ℱ n] ≤ 0`. -/ -private theorem wealth_supermartingale (μ : Measure Ω) [IsProbabilityMeasure μ] - (ℱ : Filtration ℕ m0) (X lam : ℕ → Ω → ℝ) - (hX : Adapted ℱ X) (hXb : ∀ n ω, -1 ≤ X n ω ∧ X n ω ≤ 1) - (hlam : ∀ n, StronglyMeasurable[ℱ n] (lam (n + 1))) (hlamb : ∀ n ω, 0 ≤ lam n ω ∧ lam n ω ≤ 1) - (hnull : ∀ n, μ[X (n + 1) | ℱ n] ≤ᵐ[μ] 0) : - Supermartingale (wealth X lam) ℱ μ := by - have hsm := wealth_stronglyMeasurable hX hlam - have hint : ∀ n, Integrable (wealth X lam n) μ := fun n => - integrable_of_bounded (ℱ.le n) (hsm n) (2 ^ n) fun ω => by - rw [abs_of_nonneg (wealth_nonneg hXb hlamb n ω)]; exact wealth_le hXb hlamb n ω - refine supermartingale_nat hsm hint fun n => ?_ - set g : Ω → ℝ := fun ω => wealth X lam n ω * lam (n + 1) ω with hg_def - have hg_sm : StronglyMeasurable[ℱ n] g := (hsm n).mul (hlam n) - have hXi : Integrable (X (n + 1)) μ := - integrable_of_bounded (ℱ.le (n + 1)) (hX (n + 1)).stronglyMeasurable 1 fun ω => - abs_le.mpr (hXb (n + 1) ω) - have hgX : Integrable (g * X (n + 1)) μ := - integrable_of_bounded (ℱ.le (n + 1)) - ((hg_sm.mono (ℱ.mono n.le_succ)).mul (hX (n + 1)).stronglyMeasurable) (2 ^ n) fun ω => by - have h1 := wealth_nonneg hXb hlamb n ω - have h2 := wealth_le hXb hlamb n ω - have h3 := hlamb (n + 1) ω - have h4 := hXb (n + 1) ω - simp only [Pi.mul_apply, hg_def, abs_mul, abs_of_nonneg h1, abs_of_nonneg h3.1] - have h5 : |X (n + 1) ω| ≤ 1 := abs_le.mpr h4 - calc wealth X lam n ω * lam (n + 1) ω * |X (n + 1) ω| ≤ 2 ^ n * 1 * 1 := - mul_le_mul (mul_le_mul h2 h3.2 h3.1 (by positivity)) h5 (abs_nonneg _) (by positivity) - _ = 2 ^ n := by ring - have hsplit : wealth X lam (n + 1) = wealth X lam n + g * X (n + 1) := by - rw [wealth_succ]; funext ω; simp only [Pi.add_apply, Pi.mul_apply, hg_def]; ring - rw [hsplit] - filter_upwards [condExp_add (hint n) hgX (ℱ n), - condExp_mul_of_stronglyMeasurable_left hg_sm hgX hXi, hnull n] with ω h_add h_pull h_null - rw [h_add, Pi.add_apply, condExp_of_stronglyMeasurable (ℱ.le n) (hsm n) (hint n), h_pull, - Pi.mul_apply] - have hg0 : 0 ≤ g ω := mul_nonneg (wealth_nonneg hXb hlamb n ω) (hlamb (n + 1) ω).1 - have : g ω * μ[X (n + 1) | ℱ n] ω ≤ 0 := mul_nonpos_of_nonneg_of_nonpos hg0 h_null - linarith - -/-- Finite-horizon Ville: `c * P(∃ n ≤ N, c ≤ W n) ≤ E[W 0]` for a nonnegative supermartingale. -/ -private theorem ville_finite (μ : Measure Ω) [IsProbabilityMeasure μ] (ℱ : Filtration ℕ m0) - {W : ℕ → Ω → ℝ} (hW : Supermartingale W ℱ μ) (hW0 : ∀ n ω, 0 ≤ W n ω) {c : ℝ} (hc : 0 < c) - (N : ℕ) : c * μ.real {ω | ∃ n ≤ N, c ≤ W n ω} ≤ ∫ ω, W 0 ω ∂μ := by - set τ : Ω → WithTop ℕ := fun ω => ((hittingBtwn W (Set.Ici c) 0 N ω : ℕ) : WithTop ℕ) - with hτ_def - have hτ : IsStoppingTime ℱ τ := - hW.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici - have hbdd : ∀ ω, τ ω ≤ N := fun ω => WithTop.coe_le_coe.mpr (hittingBtwn_le ω) - have hmono := hW.neg.expected_stoppedValue_mono (isStoppingTime_const ℱ 0) hτ - (fun ω => WithTop.coe_le_coe.mpr (Nat.zero_le _)) hbdd - have hneg : ∀ σ : Ω → WithTop ℕ, stoppedValue (-W) σ = -stoppedValue W σ := fun σ => rfl - rw [hneg, hneg, integral_neg', integral_neg', neg_le_neg_iff, stoppedValue_const] at hmono - have hint_stop : Integrable (stoppedValue W τ) μ := - integrable_stoppedValue ℕ hτ hW.integrable hbdd - have hmarkov := mul_meas_ge_le_integral_of_nonneg - (Filter.Eventually.of_forall fun ω => hW0 _ ω) hint_stop c - refine le_trans ?_ (hmarkov.trans hmono) - refine mul_le_mul_of_nonneg_left (measureReal_mono ?_ (measure_ne_top _ _)) hc.le - intro ω hω - obtain ⟨n, hnN, hcn⟩ := hω - exact stoppedValue_hittingBtwn_mem ⟨n, ⟨Nat.zero_le n, hnN⟩, hcn⟩ - -end Helpers - -/-- Ville's inequality for testing by betting: under the null `E[Xₙ₊₁ | ℱₙ] ≤ 0`, the wealth of a -bettor staking a predictable fraction `λₙ₊₁ ∈ [0, 1]` reaches `1/α` with probability at most `α`. -/ -theorem ville {Ω : Type*} {m0 : MeasurableSpace Ω} - (μ : Measure Ω) [IsProbabilityMeasure μ] (ℱ : Filtration ℕ m0) - (X lam : ℕ → Ω → ℝ) - (hX : Adapted ℱ X) (hXb : ∀ n ω, -1 ≤ X n ω ∧ X n ω ≤ 1) - (hlam : ∀ n, StronglyMeasurable[ℱ n] (lam (n + 1))) (hlamb : ∀ n ω, 0 ≤ lam n ω ∧ lam n ω ≤ 1) - (hnull : ∀ n, μ[X (n + 1) | ℱ n] ≤ᵐ[μ] 0) - {α : ℝ} (hα : 0 < α) : - μ {ω | ∃ n : ℕ, α⁻¹ ≤ ∏ i ∈ Finset.range n, (1 + lam (i + 1) ω * X (i + 1) ω)} - ≤ ENNReal.ofReal α := by - have hsup := wealth_supermartingale μ ℱ X lam hX hXb hlam hlamb hnull - have hc : 0 < α⁻¹ := inv_pos.mpr hα - have hW0 : ∫ ω, wealth X lam 0 ω ∂μ = 1 := by simp [wealth] - set S : ℕ → Set Ω := fun N => {ω | ∃ n ≤ N, α⁻¹ ≤ wealth X lam n ω} with hS - have hmonoS : Monotone S := fun N M hNM ω ⟨n, hn, h⟩ => ⟨n, hn.trans hNM, h⟩ - have hunion : {ω | ∃ n : ℕ, α⁻¹ ≤ ∏ i ∈ Finset.range n, (1 + lam (i + 1) ω * X (i + 1) ω)} - = ⋃ N, S N := by - ext ω - simp only [Set.mem_ofPred_eq, Set.mem_iUnion, hS] - exact ⟨fun ⟨n, h⟩ => ⟨n, n, le_rfl, h⟩, fun ⟨_, n, _, h⟩ => ⟨n, h⟩⟩ - rw [hunion, hmonoS.measure_iUnion] - refine iSup_le fun N => ?_ - have h := ville_finite μ ℱ hsup (wealth_nonneg hXb hlamb) hc N - rw [hW0] at h - have hreal : μ.real (S N) ≤ α := by - have h' := (le_div_iff₀' hc).mpr h - simpa using h' - rw [ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) hα.le] - simpa [measureReal_def] using hreal - -end Challenge.TestingByBetting