Problems

The benchmark catalog consists of carefully curated problems across mathematics, chosen so that their statements are mostly accessible using existing Mathlib definitions, but their solutions are difficult for current publicly available frontier models.

The problem statements below are automatically extracted from the lean-eval repository.

Authors are encouraged to submit new problems via PRs to that repository, for inclusion in future benchmark releases. See Submit for details on submitting solutions.

All problems

Main benchmark problems

Baer–Suzuki theorem

baer_suzuki

Submitter: Kim Morrison.

Notes: An element x of a finite group G lies in the p-core O_p(G) iff every pair (x, x^g) of conjugates generates a p-group. R. Baer, 'Engelsche Elemente Noetherscher Gruppen', Math. Ann. 133 (1957), 256-270 (the case p = 2); M. Suzuki, 'Finite groups in which the centralizer of any element of order 2 is 2-closed', Ann. of Math. 82 (1965), 191-212 (general p). A standard tool in CFSG-era local analysis, used together with the Bender method and signalizer functor theory. Introduces a small Defs/PCore.lean defining the p-core O_p(G) as the supremum of normal p-subgroups (Mathlib has no `pCore` operation).

Source: R. Baer, Engelsche Elemente Noetherscher Gruppen, Math. Ann. 133 (1957), 256-270; M. Suzuki, Finite groups in which the centralizer of any element of order 2 is 2-closed, Ann. of Math. (2) 82 (1965), 191-212.

Informal solution: Forward: O_p(G) is a normal p-subgroup, so it contains both x and x^g and hence their generated subgroup, which is therefore a p-group. Reverse (the deep direction): assume by minimal counterexample. The hypothesis ⟨x, x^g⟩ a p-group for all g (taking g = 1) forces x to be a p-element. Suzuki's original proof passes to a faithful representation and exploits a transitivity argument on the set of conjugates of x. The cleanest modern proof (Aschbacher, *Finite Group Theory*, §31) routes through the lemma that if every two conjugates of x generate a p-group, then ⟨x^G⟩ — the normal closure of x — is itself a p-group, hence contained in O_p(G).

theorem declaration uses `sorry`baer_suzuki {G : Type*} [Group G] [Finite G]
    {p : ℕ} [Fact p.Prime] (x : G) :
    x ∈ LeanEval.GroupTheory.Defs.pCore p G ↔
      ∀ g : G, IsPGroup p
        (Subgroup.closure ({x, g * x * g⁻¹} : Set G)) := byG:Type u_1inst✝²:Group Ginst✝¹:Finite Gp:ℕinst✝:Fact (Nat.Prime p)x:G⊢ x ∈ pCore p G ↔ ∀ (g : G), IsPGroup p ↥(Subgroup.closure {x, g * x * g⁻¹})
  sorryAll goals completed! 🐙

Baker-Wüstholz theorem on linear forms in logarithms

bakerWustholz_linearForms_logs

Submitter: Ralf Stephan.

Notes: Unavailable.

Source: A. Baker, G. Wüstholz, Logarithmic forms and group varieties, J. reine angew. Math. 442 (1993), 19-62.

Informal solution: Unavailable.

theorem declaration uses `sorry`bakerWustholz_linearForms_logs {n : ℕ} (hn : 0 < n)
    {K : Type*} [Field K] [NumberField K] (φ : K →+* ℂ)
    (α : Fin n → K) (hα : ∀ i, α i ≠ 0)
    (b : Fin n → ℤ) {B : ℕ} (hB : 2 ≤ B) (hbB : ∀ i, (b i).natAbs ≤ B)
    (hΛ_ne_zero : (∑ i, (b i : ℂ) * Complex.log (φ (α i))) ≠ 0) :
    Real.log ‖∑ i, (b i : ℂ) * Complex.log (φ (α i))‖
      ≥ -(BakerWustholz.C n (Module.finrank ℚ K)
          * max (Real.log B) (1 / (Module.finrank ℚ K : ℝ))
          * ∏ i, BakerWustholz.modifiedHeight φ (α i)) := byn:ℕhn:0 < nK:Type u_1inst✝¹:Field Kinst✝:NumberField Kφ:K →+* ℂα:Fin n → Khα:∀ (i : Fin n), α i ≠ 0b:Fin n → ℤB:ℕhB:2 ≤ BhbB:∀ (i : Fin n), (b i).natAbs ≤ BhΛ_ne_zero:∑ i, ↑(b i) * log (φ (α i)) ≠ 0⊢ Real.log ‖∑ i, ↑(b i) * log (φ (α i))‖ ≥
  -(BakerWustholz.C n (Module.finrank ℚ K) * max (Real.log ↑B) (1 / ↑(Module.finrank ℚ K)) *
      ∏ i, BakerWustholz.modifiedHeight φ (α i))
  sorryAll goals completed! 🐙

Balanceable k-bounded partitions

balanceable_bounded_partitions

Submitter: Julia M. Himmel.

Notes: Unavailable.

Source: https://projecteuler.net/problem=772

Informal solution: Unavailable.

theorem declaration uses `sorry`minimal_balanceable_of_bounded (k : ℕ) (hk : 0 < k) :
    Minimal (fun n => 0 < n ∧ ∀ p : n.Partition, LeanEval.Combinatorics.Bounded k p → LeanEval.Combinatorics.Balanceable p) (2 * (Finset.Icc 1 k).lcm id) := byk:ℕhk:0 < k⊢ Minimal (fun n => 0 < n ∧ ∀ (p : n.Partition), Bounded k p → Balanceable p) (2 * (Finset.Icc 1 k).lcm id)
  sorryAll goals completed! 🐙

Bézout's theorem (projective, with multiplicity)

bezout_projective_multiplicity

Submitter: Kim Morrison.

Notes: For n homogeneous polynomials f_k of total degrees d_k ≥ 1 in n + 1 variables over an algebraically closed field with finite common projective zero set, the sum of intersection multiplicities equals ∏ d_k (equation in ℕ∞). The intersection multiplicity is constructed via the affine cone (Eisenbud Ch. 12): pick an index i with p.rep i ≠ 0, normalise the i-th coordinate to 1, localise K[X_0, …, X_n] at the maximal ideal of the resulting affine point, and take Module.length K of the quotient by (f_1, …, f_n, X_i − 1). §50 of Knill's 'Some Fundamental Theorems in Mathematics'.

Source: É. Bézout, *Théorie générale des équations algébriques*, Paris, 1779. Modern projective formulation: see Eisenbud, *Commutative Algebra*, Chapter 12, or Hartshorne, *Algebraic Geometry*, Ch. I §7. Listed as §50 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Standard proof via Hilbert series: cutting the homogeneous coordinate ring K[X_0, …, X_n] by the regular sequence f_1, …, f_n gives an Artinian graded algebra whose total length is ∏ d_k (Macaulay 1916). The local-Hilbert-series decomposition redistributes this length as a sum over the finitely many intersection points. Alternative deformation proof: degenerate the f_k continuously to f̃_k = ∏_j (X_{k+1} − α_{k,j} · X_0) for distinct α_{k,j} ∈ K; the deformed intersection has exactly ∏ d_k transverse points (multiplicity 1 each); continuity of the Hilbert function under flat families shows the multiplicity sum is preserved.

theorem declaration uses `sorry`bezout_multiplicity [IsAlgClosed K] {n : ℕ}
    (f : Fin n → MvPolynomial (Fin (n + 1)) K)
    (d : Fin n → ℕ) (_hd : ∀ k, (f k).IsHomogeneous (d k))
    (_hdeg : ∀ k, (f k).totalDegree = d k)
    (_hd_pos : ∀ k, 1 ≤ d k)
    (_hfin : (⋂ k, LeanEval.AlgebraicGeometry.vanishingSet (f k)).Finite) :
    ∑ᶠ p ∈ (⋂ k, LeanEval.AlgebraicGeometry.vanishingSet (f k)), intersectionMultiplicity f p
      = (∏ k, d k : ℕ∞) := byK:Type u_1inst✝¹:Field Kinst✝:IsAlgClosed Kn:ℕf:Fin n → MvPolynomial (Fin (n + 1)) Kd:Fin n → ℕ_hd:∀ (k : Fin n), (f k).IsHomogeneous (d k)_hdeg:∀ (k : Fin n), (f k).totalDegree = d k_hd_pos:∀ (k : Fin n), 1 ≤ d k_hfin:(⋂ k, vanishingSet (f k)).Finite⊢ ∑ᶠ (p : ProjSpace K n) (_ : p ∈ ⋂ k, vanishingSet (f k)), intersectionMultiplicity f p = ∏ k, ↑(d k)
  sorryAll goals completed! 🐙

Character values of finite groups lie in cyclotomic fields

brauer_character_in_cyclotomic

Submitter: Kim Morrison.

Notes: For a finite group G of exponent n, every value of every complex character of G lies in (the image of) the cyclotomic field ℚ(ζₙ). Stated uniformly for the fixed group G: there is a ring embedding φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ whose range contains tr(ρ(g)) for every finite-dimensional complex representation ρ of G and every g. This is a corollary of Brauer's induction theorem; the full splitting-field statement (every irreducible representation has a ℚ(ζₙ)-form) is strictly stronger and requires more scalar-extension scaffolding than mathlib currently exposes cleanly.

Source: R. Brauer, On the representation of a group of order g in the field of g-th roots of unity, Amer. J. Math. 67 (1945).

Informal solution: Choose an embedding φ : ℚ(ζₙ) ↪ ℂ once and for all for the fixed group G. Then apply Brauer's induction theorem uniformly: every complex character of G is a ℤ-combination of characters induced from elementary subgroups, and those induced character values lie in φ(ℚ(ζₙ)). Hence for every finite-dimensional complex representation ρ of G and every g ∈ G, tr(ρ(g)) lies in φ.range.

theorem declaration uses `sorry`brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] :
    ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ,
      ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
        (ρ : Representation ℂ G V) (g : G),
        LinearMap.trace ℂ V (ρ g) ∈ φ.range := byG:Typeinst✝¹:Group Ginst✝:Fintype G⊢ ∃ φ,
  ∀ (V : Type) (x : AddCommGroup V) (x_1 : Module ℂ V),
    FiniteDimensional ℂ V → ∀ (ρ : Representation ℂ G V) (g : G), (LinearMap.trace ℂ V) (ρ g) ∈ φ.range
  sorryAll goals completed! 🐙

Brauer–Fowler theorem

brauer_fowler

Submitter: Kim Morrison.

Notes: The order of a finite nonabelian simple group is bounded by a function of the order of any involution centralizer. R. Brauer and K. A. Fowler, 'On groups of even order', Ann. of Math. 62 (1955), 565-583. A foundational result of the CFSG programme: it reduced (in principle) the classification of finite simple groups to the analysis of involution centralizers — the strategy used by Brauer–Suzuki, Brauer–Suzuki–Wall, Janko, and many others to identify sporadic simple groups. Statement uses only Mathlib (IsSimpleGroup, Nat.card, Subgroup.centralizer, orderOf), no new definitions.

Source: R. Brauer and K. A. Fowler, On groups of even order, Ann. of Math. (2) 62 (1955), 565-583. https://doi.org/10.2307/1970080

Informal solution: Counting argument. For an involution t in a finite simple group G with C := |C_G(t)|, every pair of involutions a, b generates a dihedral subgroup ⟨a,b⟩ of order 2k for some k ≥ 1; the product ab has order k. Use the class equation and orbit-counting on conjugates of t to show that |G| divides (2C^2)! or a similar explicit factorial of a polynomial in C — any such bound furnishes the required f.

theorem declaration uses `sorry`brauer_fowler :
    ∃ f : ℕ → ℕ, ∀ (G : Type) [Group G] [Finite G],
      IsSimpleGroup G → (∃ a b : G, a * b ≠ b * a) →
      ∀ t : G, orderOf t = 2 →
        Nat.card G ≤ f (Nat.card (Subgroup.centralizer ({t} : Set G))) := by⊢ ∃ f,
  ∀ (G : Type) [inst : Group G] [Finite G],
    IsSimpleGroup G →
      (∃ a b, a * b ≠ b * a) → ∀ (t : G), orderOf t = 2 → Nat.card G ≤ f (Nat.card ↥(Subgroup.centralizer {t}))
  sorryAll goals completed! 🐙

Brauer–Suzuki theorem (quaternion Sylow 2-subgroup)

brauer_suzuki

Submitter: Kim Morrison.

Notes: If a finite group G has generalized quaternion Sylow 2-subgroups, then the unique involution of G maps to a central element of G/O(G), where O(G) is the largest normal odd-order subgroup. R. Brauer and M. Suzuki, 'On finite groups of even order whose 2-Sylow group is a quaternion group', Proc. Nat. Acad. Sci. U.S.A. 45 (1959), 1757-1759. Historical precursor of Glauberman's Z*-theorem (1966) and the local-analysis programme in CFSG. Introduces Defs/OddCore.lean defining O(G) as the supremum of all normal odd-order subgroups (Mathlib has no `oddCore` operation).

Source: R. Brauer and M. Suzuki, On finite groups of even order whose 2-Sylow group is a quaternion group, Proc. Nat. Acad. Sci. U.S.A. 45 (1959), 1757-1759. https://doi.org/10.1073/pnas.45.12.1757

Informal solution: The argument is character-theoretic and proceeds via a careful analysis of the principal 2-block of G. In a generalized quaternion 2-Sylow P, the unique involution z = a^{2^{n-2}} is central in P (where a is the generator of the cyclic maximal subgroup of P). Brauer's principal-block reformulation: z lies in the kernel of every ordinary irreducible character not in the principal 2-block, plus an analysis of how the principal block's characters restrict to ⟨z⟩, forces z·O(G) into the center of G/O(G). Modern simplification: Glauberman's Z*-theorem, of which Brauer-Suzuki is the prototypical case, says any isolated involution is in Z*(G); the unique involution of a generalized-quaternion Sylow 2-subgroup is automatically isolated.

theorem declaration uses `sorry`brauer_suzuki {G : Type*} [Group G] [Finite G]
    (n : ℕ) (hn : 3 ≤ n)
    (P : Sylow 2 G)
    (hquat : Nonempty ((P : Subgroup G) ≃* QuaternionGroup (2 ^ (n - 2))))
    (t : G) (ht_mem : t ∈ (P : Subgroup G)) (ht_ord : orderOf t = 2) :
    (QuotientGroup.mk t : G ⧸ LeanEval.GroupTheory.Defs.oddCore G) ∈
      Subgroup.center (G ⧸ LeanEval.GroupTheory.Defs.oddCore G) := byG:Type u_1inst✝¹:Group Ginst✝:Finite Gn:ℕhn:3 ≤ nP:Sylow 2 Ghquat:Nonempty (↥↑P ≃* QuaternionGroup (2 ^ (n - 2)))t:Ght_mem:t ∈ ↑Pht_ord:orderOf t = 2⊢ ↑t ∈ Subgroup.center (G ⧸ oddCore G)
  sorryAll goals completed! 🐙

Brouwer fixed-point theorem

brouwer_fixed_point

Submitter: Kim Morrison.

Notes: §33 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (additional statement of the game-theory section; Brouwer underlies Nash's 1950 proof of equilibrium existence). Every continuous self-map of a nonempty compact convex K ⊆ ℝᵈ has a fixed point. Mathlib has the Banach fixed-point theorem (strictly weaker — needs Lipschitz < 1); `grep -ri brouwer` returns only Brouwerian lattices/logics. Brouwer is theorem #36 on Freek Wiedijk's 'Formalizing 100 Theorems' list and is formalized in Lean outside mathlib (per docs/100.yaml `links` entry), in Isabelle/AFP, HOL Light, and Coq.

Source: L. E. J. Brouwer, Über Abbildung von Mannigfaltigkeiten, Math. Ann. 71 (1912). Listed as §33 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); also #36 on Freek Wiedijk's 100 list (https://www.cs.ru.nl/~freek/100/).

Informal solution: Reduce to the closed unit ball B^d via a homeomorphism (any nonempty compact convex K ⊆ ℝᵈ is homeomorphic to a closed ball of the appropriate dimension). On the ball, suppose for contradiction f has no fixed point; then for each x ∈ B^d the ray from f(x) through x meets ∂B^d in a unique point r(x), defining a continuous retraction r : B^d → ∂B^d with r|∂B^d = id. Such a retraction is impossible by a homotopy/homology argument (the sphere S^{d-1} is not contractible / has H_{d-1} = ℤ while the ball has trivial reduced homology), giving a contradiction. Alternative proofs go through Sperner's lemma, simplicial approximation, or homotopy invariance of degree.

theorem declaration uses `sorry`brouwer_fixed_point {d : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin d))}
    (_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
    (_hK_nonempty : K.Nonempty)
    (f : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d))
    (_hf_cont : ContinuousOn f K) (_hf_maps : MapsTo f K K) :
    ∃ x ∈ K, f x = x := byd:ℕK:Set (EuclideanSpace ℝ (Fin d))_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.Nonemptyf:EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)_hf_cont:ContinuousOn f K_hf_maps:MapsTo f K K⊢ ∃ x ∈ K, f x = x
  sorryAll goals completed! 🐙

Comparison principle for the Dirichlet BVP

bvp_comparison

Submitter: Kim Morrison.

Notes: 1D maximum principle: -u'' <= -v'' on (0,1) and u <= v at the endpoints implies u <= v on [0,1].

Source: Standard maximum-principle argument; Protter-Weinberger.

Informal solution: From -u'' <= -v'' we get (u - v)'' >= 0 on (0, 1), so u - v is convex on [0, 1] (using continuity at the endpoints). A convex function lies below its chord, which here is non-positive at both endpoints, so u - v <= chord <= 0. A perturbation form: psi := (u - v) - delta x (1 - x) is strictly convex (psi'' >= 2 delta > 0) and attains its supremum at the boundary, where psi <= 0; let delta -> 0+.

theorem declaration uses `sorry`bvp_comparison (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 ⊆ J)
    (u v : ℝ → ℝ)
    (hu : ∀ x ∈ J, HasDerivAt u (deriv u x) x)
    (hu' : ∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) x)
    (hv : ∀ x ∈ J, HasDerivAt v (deriv v x) x)
    (hv' : ∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) x)
    (hineq : ∀ x ∈ Set.Ioo (0 : ℝ) 1, -deriv (deriv u) x ≤ -deriv (deriv v) x)
    (hu0 : u 0 ≤ v 0) (hu1 : u 1 ≤ v 1) :
    ∀ x ∈ Set.Icc (0 : ℝ) 1, u x ≤ v x := byJ:Set ℝhJ_open:IsOpen JhJ_sub:Set.Icc 0 1 ⊆ Ju:ℝ → ℝv:ℝ → ℝhu:∀ x ∈ J, HasDerivAt u (deriv u x) xhu':∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) xhv:∀ x ∈ J, HasDerivAt v (deriv v x) xhv':∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) xhineq:∀ x ∈ Set.Ioo 0 1, -deriv (deriv u) x ≤ -deriv (deriv v) xhu0:u 0 ≤ v 0hu1:u 1 ≤ v 1⊢ ∀ x ∈ Set.Icc 0 1, u x ≤ v x
  sorryAll goals completed! 🐙

Cauchy–Kovalevskaya theorem

cauchy_kovalevskaya

Submitter: Kim Morrison.

Notes: §32 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The quasi-linear scalar Cauchy problem with real-analytic data has a unique local analytic solution. Stated with off-the-shelf mathlib (AnalyticOnNhd, fderiv, EuclideanSpace); the PDE is encoded through the Fréchet derivative, with fderiv u p (0,1) the time derivative and fderiv u p (v,0) the spatial directional derivative. Mathlib has no Cauchy-Kovalevskaya theorem, and no formalization of it was found in any other proof assistant.

Source: A.-L. Cauchy (1842) and S. Kovalevskaya (1875). Listed as §32 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Construct the solution as a formal power series in (x, t) whose coefficients are determined recursively by differentiating the PDE and using the initial data; prove convergence by the method of majorants — bound the analytic data F, f, u₀ by geometric majorants for which the majorant Cauchy problem has an explicitly convergent closed-form solution, so the formal series converges on a neighborhood and is analytic there. Uniqueness holds because the power-series coefficients of any analytic solution with the given initial data are forced by the equation.

theorem declaration uses `sorry`cauchy_kovalevskaya {d : ℕ}
    (F : LeanEval.Analysis.E d × ℝ × ℝ → LeanEval.Analysis.E d) (f : LeanEval.Analysis.E d × ℝ × ℝ → ℝ) (u₀ : LeanEval.Analysis.E d → ℝ)
    (_hF : AnalyticOnNhd ℝ F univ) (_hf : AnalyticOnNhd ℝ f univ)
    (_hu₀ : AnalyticOnNhd ℝ u₀ univ) (x₀ : LeanEval.Analysis.E d) :
    ∃ (U : Set (LeanEval.Analysis.E d × ℝ)) (u : LeanEval.Analysis.E d × ℝ → ℝ),
      (x₀, (0 : ℝ)) ∈ U ∧ IsOpen U ∧ AnalyticOnNhd ℝ u U ∧
      (∀ x : LeanEval.Analysis.E d, (x, (0 : ℝ)) ∈ U → u (x, 0) = u₀ x) ∧
      (∀ p ∈ U,
        fderiv ℝ u p ((0 : LeanEval.Analysis.E d), (1 : ℝ)) =
          fderiv ℝ u p (F (p.1, p.2, u p), (0 : ℝ)) + f (p.1, p.2, u p)) ∧
      (∀ v : LeanEval.Analysis.E d × ℝ → ℝ, AnalyticOnNhd ℝ v U →
        (∀ x : LeanEval.Analysis.E d, (x, (0 : ℝ)) ∈ U → v (x, 0) = u₀ x) →
        (∀ p ∈ U,
          fderiv ℝ v p ((0 : LeanEval.Analysis.E d), (1 : ℝ)) =
            fderiv ℝ v p (F (p.1, p.2, v p), (0 : ℝ)) + f (p.1, p.2, v p)) →
        ∀ p ∈ U, u p = v p) := byd:ℕF:E d × ℝ × ℝ → E df:E d × ℝ × ℝ → ℝu₀:E d → ℝ_hF:AnalyticOnNhd ℝ F univ_hf:AnalyticOnNhd ℝ f univ_hu₀:AnalyticOnNhd ℝ u₀ univx₀:E d⊢ ∃ U u,
  (x₀, 0) ∈ U ∧
    IsOpen U ∧
      AnalyticOnNhd ℝ u U ∧
        (∀ (x : E d), (x, 0) ∈ U → u (x, 0) = u₀ x) ∧
          (∀ p ∈ U, (fderiv ℝ u p) (0, 1) = (fderiv ℝ u p) (F (p.1, p.2, u p), 0) + f (p.1, p.2, u p)) ∧
            ∀ (v : E d × ℝ → ℝ),
              AnalyticOnNhd ℝ v U →
                (∀ (x : E d), (x, 0) ∈ U → v (x, 0) = u₀ x) →
                  (∀ p ∈ U, (fderiv ℝ v p) (0, 1) = (fderiv ℝ v p) (F (p.1, p.2, v p), 0) + f (p.1, p.2, v p)) →
                    ∀ p ∈ U, u p = v p
  sorryAll goals completed! 🐙

Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometry

cerf_gamma_four

Submitter: Kim Morrison.

Notes: Cerf's 1968 theorem, the X = point (unparameterized) case of the Smale conjecture. Stated as the existence of a smooth isotopy [0,1] x S3 -> S3 from f to a linear isometry, witnessed by a smooth slice-inverse to encode the diffeomorphism property of each slice without needing a topology on Diffeomorph.

Source: J. Cerf, Sur les diffeomorphismes de la sphere de dimension trois, Lecture Notes in Mathematics 53, Springer (1968).

Informal solution: Cerf's original proof uses pseudo-isotopy theory: a self-diffeomorphism of S3 extends to a pseudo-isotopy of D4, and Cerf's theorem on the triviality of pi_0 of the pseudo-isotopy space in dimension 4 implies the extension is isotopic to a genuine isotopy. Hatcher (1983) reproved this as a corollary of the full Smale conjecture using configurations of 2-spheres.

theorem declaration uses `sorry`cerf_gamma_four (f : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 ≃ₘ⟮𝓡 3, 𝓡 3⟯
         sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) :
    ∃ (A : Matrix.orthogonalGroup (Fin 4) ℝ)
      (F F' : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
      ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F ∧
      ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F' ∧
      (∀ t p, F  (t, F' (t, p)) = p) ∧
      (∀ t p, F' (t, F  (t, p)) = p) ∧
      (∀ p, F (0, p) = f p) ∧
      (∀ p, (F (1, p) : EuclideanSpace ℝ (Fin 4)) =
            Matrix.UnitaryGroup.toLinearEquiv A
              (p : EuclideanSpace ℝ (Fin 4))) := byf:↑(sphere 0 1) ≃ₘ⟮𝓡 3, 𝓡 3⟯ ↑(sphere 0 1)⊢ ∃ A F F',
  ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F ∧
    ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F' ∧
      (∀ (t : ↑unitInterval) (p : ↑(sphere 0 1)), F (t, F' (t, p)) = p) ∧
        (∀ (t : ↑unitInterval) (p : ↑(sphere 0 1)), F' (t, F (t, p)) = p) ∧
          (∀ (p : ↑(sphere 0 1)), F (0, p) = f p) ∧
            ∀ (p : ↑(sphere 0 1)), (↑(F (1, p))).ofLp = (Matrix.UnitaryGroup.toLinearEquiv A) (↑p).ofLp
  sorryAll goals completed! 🐙

Chudnovsky formula for pi inverse

chudnovsky_formula_for_pi_inv

Submitter: Kim Morrison.

Notes: Uses the existing Mathlib definition of the Chudnovsky series and asks for the missing identity with pi inverse. The Chudnovsky formula states 1/π = (12 / 640320^(3/2)) · ∑_{n=0}^∞ (-1)^n · (6n)! · (545140134·n + 13591409) / ((3n)! · (n!)^3 · 640320^(3n)).

Source: https://arxiv.org/abs/1809.00533

Informal solution: Prove that the Chudnovsky series 1/π = (12 / 640320^(3/2)) · ∑_{n=0}^∞ (-1)^n · (6n)! · (545140134·n + 13591409) / ((3n)! · (n!)^3 · 640320^(3n)) holds, e.g. following Milla's detailed complex-analytic proof.

theorem declaration uses `sorry`chudnovsky_formula_for_pi_inv :
    chudnovskySum = π⁻¹ := by⊢ chudnovskySum = π⁻¹
  sorryAll goals completed! 🐙

Commuting probabilities are closed

commProb_closed

Submitter: Thomas Browning.

Notes: The set of commuting probabilities of finite groups is closed.

Source: https://arxiv.org/abs/2201.09402

Informal solution: Neumann's theorem describes the structure of finite groups with bounded below commuting probability. Then pass to subsequences of groups with similar structure.

theorem declaration uses `sorry`commProb_closed : IsClosed ({p : ℝ | ∃ (G : Type) (hG : Group G), commProb G = p}) := by⊢ IsClosed {p | ∃ G hG, ↑(commProb G) = p}
  sorryAll goals completed! 🐙

Bing's house with two rooms is contractible

contractibleSpace_houseWithTwoRooms

Submitter: Junyan Xu.

Notes: Unavailable.

Source: Allen Hatcher, *Algebraic Topology*.

Informal solution: Show that a neighborhood of the space deformation retracts onto it and is homeomorphic to a 3-ball.

theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := by⊢ ContractibleSpace ↑HouseWithTwoRooms
  sorryAll goals completed! 🐙

The Conway knot is not smoothly slice

conway_knot_not_smoothly_slice

Submitter: Kim Morrison.

Notes: Lisa Piccirillo, *The Conway knot is not slice*, Annals of Mathematics 191 (2020). Resolves the last remaining case in the classification of slice knots through 12 crossings. The Conway knot has trivial Alexander polynomial so is topologically slice (Freedman), while Piccirillo's theorem rules out smooth sliceness — pairs with `conway_knot_topologically_slice` for an explicit, low-crossing-number witness to the smooth/topological gap (earlier witnesses such as Akbulut-Matveyev's Whitehead doubles existed).

Source: https://arxiv.org/abs/1808.02923

Informal solution: Piccirillo's strategy: construct a knot K' having the same 0-trace as the Conway knot. The trace-embedding argument then transfers sliceness — if the Conway knot were smoothly slice, K' would be too. Compute Rasmussen's s-invariant of K' (a smooth slice obstruction, via Khovanov homology / Lee's perturbation); show s(K') != 0; conclude both K' and the Conway knot are not smoothly slice. Note that the standard smooth slice obstructions s and tau both vanish on the Conway knot itself, which is why the detour through K' is needed.

theorem declaration uses `sorry`conway_knot_not_smoothly_slice : ¬ conwayKnot.SmoothlySlice := by⊢ ¬conwayKnot.SmoothlySlice
  sorryAll goals completed! 🐙

The Conway knot is topologically slice

conway_knot_topologically_slice

Submitter: Kim Morrison.

Notes: Freedman's theorem applied to the Conway knot 11n34, whose Alexander polynomial is trivial. The proof requires Freedman's full topological surgery machinery in dimension four; this is genuinely hard. Pairs with `conway_knot_not_smoothly_slice` (Piccirillo) to give the celebrated smooth/topological dichotomy for a specific named knot.

Source: Freedman, *The topology of four-dimensional manifolds*, J. Diff. Geom. 17 (1982). See also Freedman-Quinn, *Topology of 4-Manifolds*, Princeton 1990.

Informal solution: Compute the Alexander polynomial of the Conway knot from a Seifert matrix and verify Delta(t) = 1. Apply Freedman's theorem: every knot in S^3 with Alexander polynomial 1 bounds a locally flat topological disk in B^4. Construct the resulting locally flat disk image inside R^3 x [0, infty) and verify the local flatness condition pointwise.

theorem declaration uses `sorry`conway_knot_topologically_slice : conwayKnot.TopologicallySlice := by⊢ conwayKnot.TopologicallySlice
  sorryAll goals completed! 🐙

Polynomial decay rate of y' = -y^3

cubic_decay_asymptotic

Submitter: Kim Morrison.

Notes: Asymptotic rate y t * sqrt t -> 1/sqrt 2 for the unique solution of y' = -y^3 on (0, infty) with y continuous at 0 and y 0 = 1.

Source: Standard ODE textbook exercise.

Informal solution: The closed form is y(t) = (1 + 2t)^{-1/2}, so y(t) sqrt(t) = sqrt(t / (1 + 2t)) -> 1/sqrt(2). Uniqueness on (0, infty) follows by Grönwall: any two solutions u, v of u' = -u^3 with the same right-limit 1 at 0 satisfy |u - v|' bounded by a Lipschitz constant on bounded subintervals, and continuity at 0 forces |u(t) - v(t)| -> 0 as t -> 0+, hence u = v.

theorem declaration uses `sorry`cubic_decay_asymptotic (y : ℝ → ℝ) (hy_diff : ∀ t : ℝ, 0 < t → HasDerivAt y (-(y t) ^ 3) t)
    (hy_cont : ContinuousWithinAt y (Set.Ici 0) 0)
    (hy0 : y 0 = 1) :
    Tendsto (fun t : ℝ => y t * Real.sqrt t) atTop (𝓝 (1 / Real.sqrt 2)) := byy:ℝ → ℝhy_diff:∀ (t : ℝ), 0 < t → HasDerivAt y (-y t ^ 3) thy_cont:ContinuousWithinAt y (Set.Ici 0) 0hy0:y 0 = 1⊢ Tendsto (fun t => y t * √t) atTop (𝓝 (1 / √2))
  sorryAll goals completed! 🐙

Real cyclotomic integer with house in (2, 76/33)

cyclotomic_integer_house_between_two_and_76_33

Submitter: Kim Morrison.

Notes: The 2 < house < 76/33 branch of Theorem 1.0.5 from Calegari--Morrison--Snyder, stated using Mathlib's NumberField.house.

Source: https://arxiv.org/pdf/1004.0665

Informal solution: If the house lies in (2, 76/33), then it is one of the five explicitly listed values.

theorem declaration uses `sorry`cyclotomic_integer_house_between_two_and_76_33 {K : Type*} [Field K] [NumberField K] [Algebra ℚ K]
    (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ K] {β : K}
    (hβ_int : IsIntegral ℤ β)
    (hβ_real : β ∈ NumberField.maximalRealSubfield K) :
    (2 < house β ∧ house β < (76 : ℝ) / 33) →
      house β = (Real.sqrt 7 + Real.sqrt 3) / 2 ∨
      house β = Real.sqrt 5 ∨
      house β = 1 + 2 * Real.cos (2 * Real.pi / 7) ∨
      house β = (1 + Real.sqrt 5) / Real.sqrt 2 ∨
      house β = (1 + Real.sqrt 13) / 2 := byK:Type u_1inst✝⁴:Field Kinst✝³:NumberField Kinst✝²:Algebra ℚ Kn:ℕinst✝¹:NeZero ninst✝:IsCyclotomicExtension {n} ℚ Kβ:Khβ_int:IsIntegral ℤ βhβ_real:β ∈ maximalRealSubfield K⊢ 2 < house β ∧ house β < 76 / 33 →
  house β = (√7 + √3) / 2 ∨
    house β = √5 ∨ house β = 1 + 2 * Real.cos (2 * Real.pi / 7) ∨ house β = (1 + √5) / √2 ∨ house β = (1 + √13) / 2
  sorryAll goals completed! 🐙

Real cyclotomic integer with house at most 2

cyclotomic_integer_house_le_two

Submitter: Kim Morrison.

Notes: The <= 2 branch of Theorem 1.0.5 from Calegari--Morrison--Snyder, stated using Mathlib's NumberField.house.

Source: https://arxiv.org/pdf/1004.0665

Informal solution: If the house is at most 2, then it equals 2 cos(pi / m) for some positive integer m.

theorem declaration uses `sorry`cyclotomic_integer_house_le_two {K : Type*} [Field K] [NumberField K] [Algebra ℚ K]
    (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ K] {β : K}
    (hβ_int : IsIntegral ℤ β)
    (hβ_real : β ∈ NumberField.maximalRealSubfield K) :
    house β ≤ 2 →
      house β = 2 ∨ ∃ m : ℕ, 0 < m ∧ house β = 2 * Real.cos (Real.pi / m) := byK:Type u_1inst✝⁴:Field Kinst✝³:NumberField Kinst✝²:Algebra ℚ Kn:ℕinst✝¹:NeZero ninst✝:IsCyclotomicExtension {n} ℚ Kβ:Khβ_int:IsIntegral ℤ βhβ_real:β ∈ maximalRealSubfield K⊢ house β ≤ 2 → house β = 2 ∨ ∃ m, 0 < m ∧ house β = 2 * Real.cos (Real.pi / ↑m)
  sorryAll goals completed! 🐙

Darboux's theorem (symplectic forms are locally standard)

darboux

Submitter: Kim Morrison.

Notes: §39 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. Every symplectic form on an open U ⊆ ℝ^{2n} is locally symplectomorphic to the standard symplectic form ω₀ = ∑_i dxᵢ ∧ dx_{n+i}. The local content lives on open subsets of ℝ^{2n}; formalized against mathlib's normed-space differential-form machinery (continuous alternating maps, extDeriv, OpenPartialHomeomorph). Mathlib has all the supporting infrastructure but no symplectic forms, no ω₀, and no Darboux theorem (Analysis/Calculus/Darboux.lean is the unrelated derivative-IVT theorem). No formalization of Darboux's theorem was found in any other proof assistant.

Source: J. G. Darboux, Sur le problème de Pfaff, Bull. Sci. Math. 6 (1882), 14-36, 49-68. Listed as §39 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Moser's trick: choose linear coordinates at x ∈ U so that α(x) equals ω₀ on tangent vectors at x (possible because α is non-degenerate, by linear-algebraic normalization of an alternating bilinear form). Define the path of 2-forms αₜ := (1 − t)·ω₀ + t·α; each αₜ is closed and equals α at t = 1, ω₀ at t = 0, and αₜ(x) = ω₀(x) for all t. The closedness lets one write α − ω₀ = dβ for some 1-form β near x; non-degeneracy of αₜ near x lets one solve ι_{Xₜ} αₜ = -β for a time-dependent vector field Xₜ. Integrate Xₜ for t ∈ [0,1] starting at x to get a flow φ_t; then (φ_1)*α = ω₀ on a neighborhood, giving the desired symplectomorphism (after restricting to the open set where the flow is defined and bijective).

theorem declaration uses `sorry`darboux {n : ℕ} {U : Set (LeanEval.Geometry.Darboux.E n)} (_hU : IsOpen U)
    (α : LeanEval.Geometry.Darboux.E n → LeanEval.Geometry.Darboux.E n [⋀^Fin 2]→L[ℝ] ℝ) (_hα : LeanEval.Geometry.Darboux.IsSymplecticOn α U)
    {x : LeanEval.Geometry.Darboux.E n} (_hx : x ∈ U) :
    ∃ φ : OpenPartialHomeomorph (LeanEval.Geometry.Darboux.E n) (LeanEval.Geometry.Darboux.E n),
      x ∈ φ.source ∧ φ.source ⊆ U ∧
      ContDiffOn ℝ ∞ (φ : LeanEval.Geometry.Darboux.E n → LeanEval.Geometry.Darboux.E n) φ.source ∧
      ContDiffOn ℝ ∞ (φ.symm : LeanEval.Geometry.Darboux.E n → LeanEval.Geometry.Darboux.E n) φ.target ∧
      ∀ z ∈ φ.target,
        LeanEval.Geometry.Darboux.IsDarbouxNormal
          ((α (φ.symm z)).compContinuousLinearMap
            (fderiv ℝ (φ.symm : LeanEval.Geometry.Darboux.E n → LeanEval.Geometry.Darboux.E n) z)) := byn:ℕU:Set (E n)_hU:IsOpen Uα:E n → E n [⋀^Fin 2]→L[ℝ] ℝ_hα:IsSymplecticOn α Ux:E n_hx:x ∈ U⊢ ∃ φ,
  x ∈ φ.source ∧
    φ.source ⊆ U ∧
      ContDiffOn ℝ ∞ (↑φ) φ.source ∧
        ContDiffOn ℝ ∞ (↑φ.symm) φ.target ∧
          ∀ z ∈ φ.target, IsDarbouxNormal ((α (↑φ.symm z)).compContinuousLinearMap (fderiv ℝ (↑φ.symm) z))
  sorryAll goals completed! 🐙

De Branges's theorem (Bieberbach conjecture)

deBranges_theorem

Submitter: Junyan Xu.

Notes: Unavailable.

Source: John B. Conway, *Functions of One Complex Variable II*, Chapter 17.

Informal solution: Unavailable.

theorem declaration uses `sorry`deBranges (f : ℂ → ℂ) (diff : DifferentiableOn ℂ f (ball 0 1)) (inj : (ball 0 1).InjOn f)
    (h0 : f 0 = 0) (h1 : deriv f 0 = 1) (n : ℕ) : ‖iteratedDeriv n f 0 / n.factorial‖ ≤ n := byf:ℂ → ℂdiff:DifferentiableOn ℂ f (ball 0 1)inj:Set.InjOn f (ball 0 1)h0:f 0 = 0h1:deriv f 0 = 1n:ℕ⊢ ‖iteratedDeriv n f 0 / ↑n.factorial‖ ≤ ↑n
  sorryAll goals completed! 🐙

Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2

dirichlet_eigenvalues_eq_nat_sq

Submitter: Kim Morrison.

Notes: Characterises the spectrum of the Dirichlet Laplacian on [0,pi]: lambda is an eigenvalue iff lambda = n^2 for some positive natural n.

Source: Classical Sturm-Liouville theory.

Informal solution: Case-split on the sign of lambda. For lambda <= 0 only the zero solution satisfies both boundary conditions. For lambda > 0 the general solution is A sin(sqrt lambda x) + B cos(sqrt lambda x); the boundary conditions force B = 0 and sqrt lambda in N_{>0}. Conversely, for lambda = n^2 with n in N_{>0}, the function sin(n x) is a nontrivial Dirichlet eigenfunction.

theorem declaration uses `sorry`dirichlet_eigenvalues_eq_nat_sq (lam : ℝ) :
    (∃ (y : ℝ → ℝ) (J : Set ℝ),
        IsOpen J ∧ Set.Icc (0 : ℝ) Real.pi ⊆ J ∧
        (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
        (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧
        y 0 = 0 ∧ y Real.pi = 0 ∧
        ∃ x ∈ Set.Ioo (0 : ℝ) Real.pi, y x ≠ 0) ↔
      ∃ n : ℕ, 0 < n ∧ lam = (n : ℝ) ^ 2 := bylam:ℝ⊢ (∃ y J,
    IsOpen J ∧
      Set.Icc 0 π ⊆ J ∧
        (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
          (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y π = 0 ∧ ∃ x ∈ Set.Ioo 0 π, y x ≠ 0) ↔
  ∃ n, 0 < n ∧ lam = ↑n ^ 2
  sorryAll goals completed! 🐙

Chen theorem for Markoff graphs

dvd_card_connectedComponent_markoffGraph

Submitter: Kim Morrison.

Notes: For prime p > 3, every connected component of the nonzero Markoff graph over ZMod p has cardinality divisible by p.

Source: https://link.springer.com/article/10.1007/s00222-025-01346-9

Informal solution: Exploit the Vieta involution symmetries of the Markoff graph over F_p and show each connected component has size divisible by p.

theorem declaration uses `sorry`dvd_card_connectedComponent_markoffGraph {p : ℕ} (hp : Nat.Prime p) (hgt : 3 < p) :
    ∀ c : (LeanEval.Combinatorics.markoffGraph p).ConnectedComponent, p ∣ Nat.card c := byp:ℕhp:Nat.Prime phgt:3 < p⊢ ∀ (c : (markoffGraph p).ConnectedComponent), p ∣ Nat.card ↥c
  sorryAll goals completed! 🐙

Existence of a 779247-dim irreducible e₈-representation with 40 tensor-square isotypic components

e8_irrep_tensor_square_decomp

Submitter: Kim Morrison.

Notes: e₈ is the largest exceptional Lie algebra (dim 248), defined here by the Serre construction (Mathlib's `LieAlgebra.e₈`). The formal statement is existential: it asks for some 779247-dimensional irreducible representation whose tensor square has 40 isotypic components. In the intended solution, one constructs such a witness using the highest-weight representation with highest weight ω₁ + ω₈ (the sum of the first and last fundamental weights, in Bourbaki labelling). The U(g)-module structure on V ⊗ V used in the statement comes from lifting the Lie action via the universal enveloping algebra.

Source: Classical: representation theory of the exceptional Lie algebra e₈.

Informal solution: Construct V as V(ω₁+ω₈), the unique 779247-dim irrep of e₈. Tensor square (LiE-verified) has 40 distinct simple summand isomorphism classes (155 components with multiplicity), with the smallest being the trivial 1-dim, the 248-dim adjoint (mult 2), the 3875-dim V(ω₁), and so on up to the 85,424,220,000-dim summand. This is used to produce the existential witness required by the formal statement.

theorem declaration uses `sorry`e8_irrep_tensor_square_decomp :
    ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
      (_ : LieRingModule (LieAlgebra.e₈ ℂ) V) (_ : LieModule ℂ (LieAlgebra.e₈ ℂ) V),
      Module.finrank ℂ V = 779247 ∧
      LieModule.IsIrreducible ℂ (LieAlgebra.e₈ ℂ) V ∧
      (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.e₈ ℂ))
        (V ⊗[ℂ] V)).ncard = 40 := by⊢ ∃ V x x_1 x_2,
  ∃ (x_3 : LieModule ℂ (LieAlgebra.e₈ ℂ) V),
    Module.finrank ℂ V = 779247 ∧
      LieModule.IsIrreducible ℂ (LieAlgebra.e₈ ℂ) V ∧
        (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.e₈ ℂ)) (V ⊗[ℂ] V)).ncard = 40
  sorryAll goals completed! 🐙

Erdős's unit-distance conjecture is false

erdos_unit_distance_conjecture_false

Submitter: Kim Morrison.

Notes: Erdős (1946) conjectured ν(n) ≤ n^{1 + C / log log n} for some absolute C and all sufficiently large n. The conjecture stood for 80 years and was widely believed to be true prior to OpenAI's 2026 construction, in part because Alon-Bucić-Sauermann (2025) had proved a matching bound (d/2) n log₂ n for typical norms on ℝ^d (later sharpened by Greilhuber-Schildkraut-Tidor, 2025). The refutation also disproves the stronger Erdős-Falconer (1997) k-equidistant variant: along the refuting sequence the unit-distance graph has average degree n^{Ω(1)}, while Erdős-Falconer predicted at most n^{o(1)}. ν is defined as the number of unordered pairs in P ⊆ ℝ² at Euclidean distance exactly 1; the planar metric is the one from EuclideanSpace ℝ (Fin 2), not the product sup-metric.

Source: OpenAI, *Planar Point Sets with Many Unit Distances*, 2026. https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf . Original conjecture: P. Erdős, *On sets of distances of n points*, Amer. Math. Monthly 53 (1946), 248-250. k-equidistant variant: P. Erdős, K. Falconer, *Some problems in combinatorial geometry*, 1997.

Informal solution: Split into an arithmetic and a geometric part. (1) Arithmetic: build an admissible datum (L, K = L(i), t, q₁, …, q_t) where L is a totally real number field of growing degree f, K is its CM extension by i, and each q_b ≡ 1 mod 4 splits completely in L. Use the Hajir-Maire class-field-theoretic tower-cutting trick — start from the cyclic cubic subfield F of ℚ(ζ_{r_1 · … · r_ℓ}) for distinct primes r_i ≡ 1 mod 3, observe M/F is everywhere unramified to get d(G) ≥ ℓ - 1 for the maximal unramified pro-3 tower's Galois group G, kill prescribed Frobenius elements by quotienting G by relations chosen via Chebotarev, and apply Shafarevich's relation-rank estimate r(G) ≤ d(G) + C₀ together with Golod-Shafarevich (r > d²/4 for finite pro-p groups) to keep the quotient tower infinite. Adjoining i preserves bounded root discriminants, so Minkowski gives class numbers at most exponential in the degree: h(K_j) ≤ H^{f_j}. The split primes give m = t · f_j conjugate pairs of prime ideals; pigeonholing 2^m ε-vectors by class gives ≥ 2^m / h(K_j) ≥ exp(γ f_j) elements u ∈ K^× with N_{K/L}(u) = u · c(u) = 1 (hence |σ(u)| = 1 for every complex embedding). (2) Geometric: embed K via the Minkowski map into V = ℂ^f, take a random translate of the lattice Q^{-2} 𝒪_K cut by the polydisc B_R, and project to the first complex coordinate. Lemma 2.4 averages over cosets to find a coset with E_a ≥ exp(γ f / 2) · N_a directed unit-distance pairs; Lemma 2.6 packs the polydisc to bound |P| ≤ exp(B f) uniformly. Combining n_j ≤ exp(B f_j) with ν(P_j) ≥ n_j · exp(γ f_j / 2) / 2 gives ν(P_j) ≥ n_j^{1 + δ} with δ = γ / (4B), refuting any proposed bound n^{1 + C / log log n} once log log n_j < δ.

theorem declaration uses `sorry`erdos_unit_distance_conjecture_false :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ N : ℕ, ∃ (n : ℕ) (P : Finset (EuclideanSpace ℝ (Fin 2))),
        N ≤ n ∧ P.card = n ∧ (n : ℝ) ^ (1 + δ) ≤ (unitDist P : ℝ) := by⊢ ∃ δ, 0 < δ ∧ ∀ (N : ℕ), ∃ n P, N ≤ n ∧ P.card = n ∧ ↑n ^ (1 + δ) ≤ ↑(unitDist P)
  sorryAll goals completed! 🐙

Existence of a chiral oriented knot

exists_chiral_knot

Submitter: Kim Morrison.

Notes: Challenge problem of the knot-theory benchmark. Asks for an oriented smooth knot whose image is not ambient-isotopic to its mirror image (under reflection through the xy-plane), using the benchmark's orientation-sensitive notion of isotopy induced by the parametrization. The model must construct an ambient-isotopy invariant that takes different values on a knot and its mirror -- the knot determinant and Alexander polynomial alone do not suffice, since the figure-eight is amphichiral in the usual unoriented sense.

Source: Classical; see https://en.wikipedia.org/wiki/Chirality_(mathematics) and https://en.wikipedia.org/wiki/Trefoil_knot.

Informal solution: Take K = right-handed trefoil. Construct the knot signature sigma(K) from a Seifert matrix V as the signature of V + V^T, and verify that sigma is an ambient-isotopy invariant of knots that negates under mirror reflection. Compute sigma(right trefoil) = -2, so sigma(K) != sigma(mirror K) and K is chiral. (Alternatively, use the Jones polynomial V_K(t) = -t^{-4} + t^{-3} + t^{-1}, which is not symmetric under t <-> t^{-1}.)

theorem declaration uses `sorry`exists_chiral_knot : ∃ K : LeanEval.KnotTheory.Knot, K.Chiral := by⊢ ∃ K, K.Chiral
  sorryAll goals completed! 🐙

Complementary polynomial on the unit circle

exists_complementary_polynomial_on_unit_circle

Submitter: Kim Morrison.

Notes: If a complex polynomial has modulus at most 1 on the unit circle, then there is a same-degree complementary polynomial whose squared moduli add to 1 on the circle.

Source: https://link.springer.com/article/10.1007/s00220-025-05302-9

Informal solution: Construct a polynomial Q so that |P(z)|^2 + |Q(z)|^2 = 1 for all z on the unit circle.

theorem declaration uses `sorry`exists_complementary_polynomial_on_unit_circle (P : ℂ[X])
    (hP : ∀ z : Circle, ‖P.eval (z : ℂ)‖ ≤ 1) :
    ∃ Q : ℂ[X],
      Q.natDegree ≤ P.natDegree ∧
        ∀ z : Circle, ‖P.eval (z : ℂ)‖ ^ 2 + ‖Q.eval (z : ℂ)‖ ^ 2 = 1 := byP:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1
  sorryAll goals completed! 🐙

Existence of a non-isotopic pair of oriented knots

exists_nonisotopic_knots

Submitter: Kim Morrison.

Notes: Asks for two oriented smooth knots in R^3 that are not ambient-isotopic. The benchmark uses an orientation-sensitive notion of isotopy induced by the parametrizations. Mathlib has no knot-invariant infrastructure, so the model must construct an isotopy invariant from scratch. Suggested: the Alexander polynomial / knot determinant, or the Fox 3-coloring count, both of which distinguish the unknot from the trefoil.

Source: Classical; see https://en.wikipedia.org/wiki/Knot_invariant.

Informal solution: Take K1 = unknot (round circle in the xy-plane) and K2 = right-handed trefoil parametrized as t -> (sin t + 2 sin 2t, cos t - 2 cos 2t, -sin 3t). Construct an ambient-isotopy invariant; the simplest computable choice is the number of Fox 3-colorings of any diagram of K, which counts homomorphisms from the knot group to D_3. The unknot admits 3 such colorings (all monochromatic); the trefoil admits 9. Hence the two knots are not ambient-isotopic.

theorem declaration uses `sorry`exists_nonisotopic_knots : ∃ K₁ K₂ : LeanEval.KnotTheory.Knot, ¬ K₁.Isotopic K₂ := by⊢ ∃ K₁ K₂, ¬K₁.Isotopic K₂
  sorryAll goals completed! 🐙

Existence of a non-isotopic pair of oriented two-component links

exists_nonisotopic_link

Submitter: Kim Morrison.

Notes: Warmup for the knot-theory benchmark. Asks for two oriented smooth two-component links in R^3 that are not ambient-isotopic. The benchmark uses an orientation-sensitive notion of isotopy induced by the parametrizations, so the Gauss linking integral is a natural real-valued invariant distinguishing the unlink (lk = 0) from the Hopf link (lk = +/- 1, depending on orientation choice).

Source: Classical; see https://en.wikipedia.org/wiki/Linking_number.

Informal solution: Take L1 = unlink (two unit circles in parallel planes) and L2 = Hopf link, with explicit orientations induced by the parametrizations. Define lk(K, L) by the Gauss double integral (1/4 pi) int int <K(s) - L(t), K'(s) x L'(t)> / |K(s) - L(t)|^3 ds dt. Prove lk is invariant under ambient isotopy of oriented links by exhibiting it as the integral of a closed 2-form on R^3 minus the origin pulled back along (K, L), so Stokes-style arguments show invariance. Compute lk(unlink) = 0 and choose the Hopf-link orientations so that lk(Hopf) = 1. Conclude L1 and L2 are not ambient-isotopic.

theorem declaration uses `sorry`exists_nonisotopic_link : ∃ L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := by⊢ ∃ L₁ L₂, ¬L₁.Isotopic L₂
  sorryAll goals completed! 🐙

Existence of a topologically slice, not smoothly slice knot

exists_topologically_slice_not_smoothly_slice

Submitter: Kim Morrison.

Notes: The smooth/topological gap in dimension four. Casson, Akbulut-Matveyev, and Hedden-Kirk-Livingston gave explicit witnesses; Piccirillo later resolved the Conway knot 11n34 — a much smaller, celebrated example of the same phenomenon. The solver may choose any witness. Topological sliceness here means bounding a *locally flat* topological 2-disk in R^3 x [0, infty); the locally flat clause is essential since without it the cone over any knot is a topological disk.

Source: Casson, 1980s (unpublished); Akbulut-Matveyev, *A convex decomposition theorem for 4-manifolds*, IMRN 1998. See also Hedden-Kirk-Livingston, *Non-slice linear combinations of algebraic knots*, J. Eur. Math. Soc. 14 (2012).

Informal solution: Take K = positive Whitehead double of a knot K_0 with tau(K_0) > 0 (e.g. the right-handed trefoil; Akbulut-Matveyev). Whitehead doubles always have trivial Alexander polynomial, so K is topologically slice by Freedman's theorem. The Ozsvath-Szabo tau-invariant of K equals tau(K_0) > 0, and tau is a smooth slice obstruction (tau != 0 implies not smoothly slice), so K is not smoothly slice.

theorem declaration uses `sorry`exists_topologically_slice_not_smoothly_slice :
    ∃ K : LeanEval.KnotTheory.PLKnot, K.TopologicallySlice ∧ ¬ K.SmoothlySlice := by⊢ ∃ K, K.TopologicallySlice ∧ ¬K.SmoothlySlice
  sorryAll goals completed! 🐙

Fatou–Julia / Cantor dichotomy

fatou_julia_dichotomy

Submitter: Kim Morrison.

Notes: For the quadratic family T_c(z) = z² + c, the filled Julia set K_c is connected when c is in the Mandelbrot set and homeomorphic to the Cantor space ℕ → Bool when c is not. §62 (additional statement 1) of Knill's 'Some Fundamental Theorems in Mathematics'. The submitted statement uses the filled Julia set rather than the boundary Julia set ∂K_c; this is equivalent for the dichotomy since K_c is connected iff ∂K_c is, and in the escaping case K_c = ∂K_c is a Cantor set.

Source: P. Fatou, *Sur les équations fonctionnelles*, Bull. Soc. Math. France 47 (1919), 161-271; 48 (1920), 33-94, 208-314. G. Julia, *Mémoire sur l'itération des fonctions rationnelles*, J. Math. Pures Appl. 1 (1918), 47-245. Modern statement: A. Douady and J. H. Hubbard, *Étude dynamique des polynômes complexes I, II*, Publ. Math. Orsay 84-02, 85-04. Listed as §62 (additional statement 1) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Connected case: use the standard theorem for polynomials that the filled Julia set is connected iff all critical orbits are bounded; for z² + c the only critical point is 0, so K_c is connected iff the orbit of 0 is bounded, i.e. iff c ∈ M. Escaping case: outside M the critical orbit escapes, K_c is compact, perfect, totally disconnected, and homeomorphic to Cantor space — the standard symbolic-dynamics conjugacy via the 2-branched preimages of a large invariant disc.

theorem declaration uses `sorry`julia_cantor_dichotomy (c : ℂ) :
    (c ∈ LeanEval.ComplexAnalysis.FatouJuliaProblem.Mandelbrot → IsConnected (LeanEval.ComplexAnalysis.FatouJuliaProblem.FilledJulia c)) ∧
    (c ∉ LeanEval.ComplexAnalysis.FatouJuliaProblem.Mandelbrot → Nonempty ((LeanEval.ComplexAnalysis.FatouJuliaProblem.FilledJulia c) ≃ₜ (ℕ → Bool))) := byc:ℂ⊢ (c ∈ Mandelbrot → IsConnected (FilledJulia c)) ∧ (c ∉ Mandelbrot → Nonempty (↑(FilledJulia c) ≃ₜ (ℕ → Bool)))
  sorryAll goals completed! 🐙

Feit–Thompson odd-order theorem

feit_thompson

Submitter: Kim Morrison.

Notes: Every finite group of odd order is solvable. W. Feit and J. G. Thompson, Pacific J. Math. 13 (1963), 775-1029. A 255-page paper that opened the path to the Classification of Finite Simple Groups; Thompson received the Fields Medal in 1970 in part for this work. Coq formalization by Gonthier et al. 2012 (~170 000 lines); no Lean port. Stated with zero new definitions on top of mathlib (IsSolvable, Odd, Nat.card, Group, Finite). Honorable-mention entry on Freek Wiedijk's 'Formalizing 100 Theorems' page (alongside the Classification of Finite Simple Groups itself).

Source: W. Feit and J. G. Thompson, Solvability of groups of odd order, Pacific J. Math. 13 (1963), 775-1029. Coq formalization: G. Gonthier et al., A Machine-Checked Proof of the Odd Order Theorem, ITP 2013 (https://hal.inria.fr/hal-00816699). Listed as a named honorable mention on https://www.cs.ru.nl/~freek/100/.

Informal solution: The proof proceeds by contradiction: assume G is a minimal counterexample, a non-solvable group of minimal odd order. (i) Generic case: by Hall-Wielandt and the Feit-Hall theorem on solvable signalizer functors, G has a unique conjugacy class of maximal subgroups containing every Sylow normalizer; rule out via character-theoretic identities (Suzuki's Brauer table machinery). (ii) Uniqueness case: G has a single 'large' maximal subgroup M whose structure is heavily constrained; case analysis on |M|/|G| and the action of M on its Frobenius-like complements gives the contradiction. (iii) The 'CN' (centralizer-normalizer) and 'CIT' (centralizer-of-involution-trivial) case analyses use the Frobenius theorem on Frobenius groups (whose only known proof uses character theory) to constrain centralizer structure. The whole argument is organized around the dichotomy 'large' vs 'small' Sylow 2-subgroups (or rather Sylow 2-substructures, since |G| is odd: there are none, so the dichotomy is about Sylow p for the smallest p dividing |G|).

theorem declaration uses `sorry`feit_thompson {G : Type*} [Group G] [Finite G]
    (_h : Odd (Nat.card G)) : IsSolvable G := byG:Type u_1inst✝¹:Group Ginst✝:Finite G_h:Odd (Nat.card G)⊢ IsSolvable G
  sorryAll goals completed! 🐙

Fermat's Last Theorem

fermat_last_theorem

Submitter: Xuanji Li.

Notes: Fermat's Last Theorem: a^n + b^n = c^n has no nontrivial natural solution when n >= 3.

Source: https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem

Informal solution: via https://en.wikipedia.org/wiki/Modularity_theorem

theorem declaration uses `sorry`fermat_last_theorem :
    FermatLastTheorem := by⊢ FermatLastTheorem
  sorryAll goals completed! 🐙

Finite Ramsey theorem for graphs

finite_graph_ramsey_theorem

Submitter: Kim Morrison.

Notes: States finite Ramsey existence for red/blue edge colourings of complete graphs, encoded by a graph and its complement.

Source: Classical theorem in Ramsey theory.

Informal solution: Show that for every r and s there is an n such that every graph on n vertices contains either a clique of size r or an independent set of size s.

theorem declaration uses `sorry`finite_graph_ramsey_theorem :
    ∀ r s : ℕ, 2 ≤ r → 2 ≤ s → ∃ n : ℕ, ∀ G : SimpleGraph (Fin n), ¬ G.CliqueFree r ∨ ¬ Gᶜ.CliqueFree s := by⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s
  sorryAll goals completed! 🐙

Burnside p^a q^b theorem

finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow

Submitter: Kim Morrison.

Notes: Burnside's theorem that a finite group of order p^a q^b is solvable.

Source: Classical theorem in finite group theory.

Informal solution: Use character theory and induction on the group order to prove solvability.

theorem declaration uses `sorry`finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow {G : Type*} [Group G] [Fintype G]
    {p q a b : ℕ}
    (hp : Nat.Prime p)
    (hq : Nat.Prime q)
    (hpq : p ≠ q)
    (hcard : Fintype.card G = p ^ a * q ^ b) :
    IsSolvable G := byG:Type u_1inst✝¹:Group Ginst✝:Fintype Gp:ℕq:ℕa:ℕb:ℕhp:Nat.Prime phq:Nat.Prime qhpq:p ≠ qhcard:Fintype.card G = p ^ a * q ^ b⊢ IsSolvable G
  sorryAll goals completed! 🐙

Possible orders of 5-transitive finite permutation groups

five_transitive_card_classification

Submitter: Kim Morrison.

Notes: If a finite group acts faithfully and 5-transitively on a set X with |X| ≥ 5, then |G| is one of n!, n!/2 (only when n ≥ 7), 95040 (= |M₁₂|), or 244823040 (= |M₂₄|). The 5 ≤ |X| hypothesis prevents the 5-transitivity condition from being vacuously satisfied (otherwise small groups like C₃ on Fin 3 would qualify). Classification is folklore via CFSG; no CFSG-free proof is known.

Source: Folklore via CFSG; classical work of Mathieu, Jordan; modern accounts in P. Cameron, Permutation Groups (1999).

Informal solution: By CFSG, the only finite 2-transitive groups are explicitly classified. Restricting to 5-transitive: the symmetric group Sₙ is k-transitive for all k ≤ n; the alternating group Aₙ is k-transitive for k ≤ n − 2 (so 5-transitive for n ≥ 7); among the Mathieu groups, M₁₂ is sharply 5-transitive on 12 points and M₂₄ is 5-transitive on 24 points. M₁₁ and M₂₃ are only 4-transitive and so do not appear. No other finite simple group has a 5-transitive permutation representation.

theorem declaration uses `sorry`five_transitive_card_classification (G X : Type) [Group G] [Fintype G] [Fintype X]
    [MulAction G X] [FaithfulSMul G X]
    (hcard : 5 ≤ Fintype.card X)
    (h5 : ∀ a b : Fin 5 → X, Function.Injective a → Function.Injective b →
      ∃ g : G, ∀ i, g • a i = b i) :
    let n := Fintype.card X
    Fintype.card G = n.factorial ∨
    (7 ≤ n ∧ Fintype.card G = n.factorial / 2) ∨
    (n = 12 ∧ Fintype.card G = 95040) ∨
    (n = 24 ∧ Fintype.card G = 244823040) := byG:TypeX:Typeinst✝⁴:Group Ginst✝³:Fintype Ginst✝²:Fintype Xinst✝¹:MulAction G Xinst✝:FaithfulSMul G Xhcard:5 ≤ Fintype.card Xh5:∀ (a b : Fin 5 → X), Function.Injective a → Function.Injective b → ∃ g, ∀ (i : Fin 5), g • a i = b i⊢ let n := Fintype.card X;
Fintype.card G = n.factorial ∨
  7 ≤ n ∧ Fintype.card G = n.factorial / 2 ∨ n = 12 ∧ Fintype.card G = 95040 ∨ n = 24 ∧ Fintype.card G = 244823040
  sorryAll goals completed! 🐙

Frobenius's theorem: the Frobenius kernel is normal

frobenius_kernel_isNormal

Submitter: Kim Morrison.

Notes: For a Frobenius group G acting transitively and faithfully on X with |X| ≥ 2, non-trivial point stabilisers, and the Frobenius condition (no non-identity element fixes more than one point), the set {1} ∪ {g | g fixes no point} is a normal subgroup. The only known proof uses Frobenius's induction-of-characters argument; no purely group-theoretic proof has been found in over a century.

Source: G. Frobenius, Über auflösbare Gruppen IV, Sitzungsber. Akad. Wiss. Berlin (1901).

Informal solution: Let H = stabilizer(x₀). Construct a class function θ on H of the form (1_H minus restriction of certain induced characters), and apply Frobenius reciprocity to lift θ to a generalised character of G whose kernel is exactly the Frobenius kernel K. The fact that the lift remains a virtual character (i.e. integer-valued combination of irreducibles) is exactly the content; that K is then a subgroup follows from K being a kernel.

theorem declaration uses `sorry`frobenius_kernel_isNormal (G X : Type) [Group G] [Fintype G] [Fintype X]
    [MulAction G X] [FaithfulSMul G X]
    (hcard : 2 ≤ Fintype.card X)
    (htrans : ∀ x y : X, ∃ g : G, g • x = y)
    (hstab : ∀ x : X, MulAction.stabilizer G x ≠ ⊥)
    (hfrob : ∀ g : G, g ≠ 1 → ∀ x y : X, g • x = x → g • y = y → x = y) :
    ∃ N : Subgroup G, N.Normal ∧
      (N : Set G) = {1} ∪ {g : G | ∀ x : X, g • x ≠ x} := byG:TypeX:Typeinst✝⁴:Group Ginst✝³:Fintype Ginst✝²:Fintype Xinst✝¹:MulAction G Xinst✝:FaithfulSMul G Xhcard:2 ≤ Fintype.card Xhtrans:∀ (x y : X), ∃ g, g • x = yhstab:∀ (x : X), MulAction.stabilizer G x ≠ ⊥hfrob:∀ (g : G), g ≠ 1 → ∀ (x y : X), g • x = x → g • y = y → x = y⊢ ∃ N, N.Normal ∧ ↑N = {1} ∪ {g | ∀ (x : X), g • x ≠ x}
  sorryAll goals completed! 🐙

Furstenberg measure-preserving multiple recurrence

furstenberg_measure

Submitter: Kim Morrison.

Notes: Furstenberg's 1977 measure-preserving multiple recurrence theorem. For every measure-preserving T on a probability space (Ω, μ), every measurable A with μ A > 0, and every d ≥ 1, some n ≥ 1 satisfies μ(A ∩ T^{-n}A ∩ T^{-2n}A ∩ ⋯ ∩ T^{-d·n}A) > 0. §56 (additional statement) of Knill's 'Some Fundamental Theorems in Mathematics'. Knill states the automorphism/image version; this file uses the standard preimage formulation for a general measure-preserving transformation. For invertible T the two are equivalent (apply the statement to T⁻¹, or shift the intersection by an iterate). The d = 1 case is the classical Poincaré recurrence theorem.

Source: H. Furstenberg, *Ergodic behavior of diagonal measures and a theorem of Szemerédi on arithmetic progressions*, Journal d'Analyse Mathématique 31 (1977), 204-256. Listed as §56 (additional statement 1) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Furstenberg's structure-theorem proof decomposes the measure-preserving system (Ω, μ, T) into a transfinite tower of relatively compact (Kronecker) extensions and weakly-mixing extensions. Multiple recurrence is established for each layer — for compact factors via uniform almost-periodicity and equidistribution; for weakly-mixing extensions via van der Corput estimates — and lifted through the tower by a Furstenberg–Zimmer-style relative theorem. Furstenberg used this multiple recurrence theorem to give the first ergodic-theoretic proof of Szemerédi's theorem on arithmetic progressions.

theorem declaration uses `sorry`furstenberg_measure_recurrence {Ω : Type*}
    [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
    [MeasureTheory.IsProbabilityMeasure μ]
    {T : Ω → Ω} (_hT : MeasureTheory.MeasurePreserving T μ μ)
    {A : Set Ω} (_hA : MeasurableSet A) (_h0 : 0 < μ A)
    (d : ℕ) (_hd : 1 ≤ d) :
    ∃ n : ℕ, 1 ≤ n ∧
      0 < μ (A ∩ ⋂ j ∈ Finset.Icc 1 d, T^[j * n] ⁻¹' A) := byΩ:Type u_1inst✝¹:MeasurableSpace Ωμ:Measure Ωinst✝:IsProbabilityMeasure μT:Ω → Ω_hT:MeasurePreserving T μ μA:Set Ω_hA:MeasurableSet A_h0:0 < μ Ad:ℕ_hd:1 ≤ d⊢ ∃ n, 1 ≤ n ∧ 0 < μ (A ∩ ⋂ j ∈ Finset.Icc 1 d, T^[j * n] ⁻¹' A)
  sorryAll goals completed! 🐙

Furstenberg–Weiss topological multiple recurrence (single-transformation form)

furstenberg_topological

Submitter: Kim Morrison.

Notes: Single-transformation form of the Furstenberg–Weiss topological multiple recurrence theorem (1978), as stated in §56 of Knill's 'Some Fundamental Theorems in Mathematics'. For every homeomorphism T of a nonempty compact metric space X, there is a multiply recurrent point: for every d ≥ 1 there is a strictly increasing n : ℕ → ℕ with T^{j · n_k}(x) → x for every j ∈ {1, …, d}. The file ships the IsMultiplyRecurrent predicate. Compact-Hausdorff alone is insufficient for the sequential formulation (the shift on Ultrafilter ℤ is a counterexample); first-countability would suffice, but the standard Furstenberg–Weiss statement uses compact metric. This is the specialisation to the family T, T², …, T^d of the more general theorem for commuting homeomorphisms.

Source: H. Furstenberg and B. Weiss, *Topological dynamics and combinatorial number theory*, Journal d'Analyse Mathématique 34 (1978), 61-85. Listed as §56 (main theorem) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Standard proof via compactness + Zorn's lemma. Consider the product diagonal T̃ := (T, T², …, T^d) acting on the product Xᵈ, and pass to a minimal nonempty closed T̃-invariant subset M ⊆ Xᵈ (Zorn). The diagonal point (x, x, …, x) ∈ M for some x ∈ X is the multiply recurrent point: the recurrence of (x, …, x) under T̃ is exactly simultaneous return of T(x), …, T^d(x) to x. Showing the diagonal point lies in M requires the multiple-recurrence content of the proof, typically via topological IP-recurrence in product systems or via Furstenberg's correspondence principle reducing to van der Waerden / Hales–Jewett. The d = 1 case is the classical Birkhoff recurrence, which uses the same Zorn-minimality argument.

theorem declaration uses `sorry`furstenberg_topological_recurrence {X : Type*} [MetricSpace X]
    [CompactSpace X] [Nonempty X] (T : X ≃ₜ X) :
    ∃ x : X, LeanEval.Dynamics.IsMultiplyRecurrent (T : X → X) x := byX:Type u_1inst✝²:MetricSpace Xinst✝¹:CompactSpace Xinst✝:Nonempty XT:X ≃ₜ X⊢ ∃ x, IsMultiplyRecurrent (⇑T) x
  sorryAll goals completed! 🐙

Existence of a 64-dim irreducible g₂-representation with 14 tensor-square isotypic components

g2_irrep_tensor_square_decomp

Submitter: Kim Morrison.

Notes: g₂ is the smallest exceptional Lie algebra, defined here by the Serre construction (Mathlib's `LieAlgebra.g₂`). The formal statement is existential: it asks for some 64-dimensional irreducible representation whose tensor square has 14 isotypic components. In the intended solution, one constructs such a witness using the highest-weight representation with highest weight ω₁ + ω₂ (the sum of the two fundamental weights). The U(g)-module structure on V ⊗ V used in the statement comes from lifting the Lie action via the universal enveloping algebra.

Source: Classical: representation theory of the exceptional Lie algebra g₂.

Informal solution: Construct V as the irreducible 64-dim representation V(ω₁+ω₂). Decomposition (LiE-verified): V⊗V = V(0,0) + V(1,0) + 2V(0,1) + 2V(2,0) + 2V(1,1) + 2V(0,2) + 3V(3,0) + 3V(2,1) + V(1,2) + V(0,3) + 2V(4,0) + 2V(3,1) + V(2,2) + V(5,0). This is used to produce the existential witness required by the formal statement.

theorem declaration uses `sorry`g2_irrep_tensor_square_decomp :
    ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
      (_ : LieRingModule (LieAlgebra.g₂ ℂ) V) (_ : LieModule ℂ (LieAlgebra.g₂ ℂ) V),
      Module.finrank ℂ V = 64 ∧
      LieModule.IsIrreducible ℂ (LieAlgebra.g₂ ℂ) V ∧
      (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.g₂ ℂ))
        (V ⊗[ℂ] V)).ncard = 14 := by⊢ ∃ V x x_1 x_2,
  ∃ (x_3 : LieModule ℂ (LieAlgebra.g₂ ℂ) V),
    Module.finrank ℂ V = 64 ∧
      LieModule.IsIrreducible ℂ (LieAlgebra.g₂ ℂ) V ∧
        (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.g₂ ℂ)) (V ⊗[ℂ] V)).ncard = 14
  sorryAll goals completed! 🐙

Schur-Weyl duality: GL(V) image equals centralizer of S_k image

glAction_range_eq_centralizer_symAction

Submitter: Kim Morrison.

Notes: The other direction of Schur-Weyl duality: the subalgebra of End(V^⊗k) generated by the diagonal GL(V) action equals the centralizer of the subalgebra generated by the S_k action.

Source: H. Weyl, The Classical Groups, 1939; I. Schur, Über die rationalen Darstellungen der allgemeinen linearen Gruppe, 1927.

Informal solution: By polarization over R with k! invertible, the subalgebra generated by {g^⊗k : g ∈ GL(V)} is precisely the image of Sym^k(End V), i.e., the endomorphisms of V^⊗k fixed by the S_k-action on tensor factors of End V. An endomorphism of V^⊗k fixed by this action is exactly one commuting with the S_k action on V^⊗k.

theorem declaration uses `sorry`glAction_range_eq_centralizer_symAction {R : Type*} [Field R]
    {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M]
    {k : ℕ} [Invertible (k.factorial : R)] :
    Algebra.adjoin R (Set.range (LeanEval.RepresentationTheory.glAction R M k)) =
      Subalgebra.centralizer R (Set.range (LeanEval.RepresentationTheory.symAction R M k)) := byR:Type u_1inst✝⁴:Field RM:Type u_2inst✝³:AddCommGroup Minst✝²:Module R Minst✝¹:FiniteDimensional R Mk:ℕinst✝:Invertible ↑k.factorial⊢ Algebra.adjoin R (Set.range ⇑(glAction R M k)) = Subalgebra.centralizer R (Set.range ⇑(symAction R M k))
  sorryAll goals completed! 🐙

Glauberman's Z* theorem for isolated involutions

glauberman_zStar

Submitter: Kim Morrison.

Notes: For a finite group G with an isolated involution t (no distinct conjugate of t commutes with t), there is a normal subgroup N ⊴ G of odd order such that every commutator g·t·g⁻¹·t⁻¹ lies in N — i.e., t is central in G/N. The hypothesis is the global form of isolation, equivalent to (but more self-contained than) the standard Sylow-local form. Proof uses modular Brauer character theory.

Source: G. Glauberman, Central elements in core-free groups, J. Algebra 4 (1966).

Informal solution: Take N = O(G), the largest normal subgroup of odd order. By Glauberman's modular character argument, isolation of t in C_G(t) implies t commutes with every element of G modulo O(G). The core of the proof is the analysis of the principal 2-block of G via Brauer characters and the Z*-style fusion theorem.

theorem declaration uses `sorry`glauberman_zStar (G : Type) [Group G] [Fintype G]
    (t : G) (ht1 : t ≠ 1) (ht2 : t * t = 1)
    (hisolated : ∀ g : G, (g * t * g⁻¹) * t = t * (g * t * g⁻¹) →
      g * t * g⁻¹ = t) :
    ∃ N : Subgroup G, N.Normal ∧ Odd (Nat.card N) ∧
      ∀ g : G, g * t * g⁻¹ * t⁻¹ ∈ N := byG:Typeinst✝¹:Group Ginst✝:Fintype Gt:Ght1:t ≠ 1ht2:t * t = 1hisolated:∀ (g : G), g * t * g⁻¹ * t = t * (g * t * g⁻¹) → g * t * g⁻¹ = t⊢ ∃ N, N.Normal ∧ Odd (Nat.card ↥N) ∧ ∀ (g : G), g * t * g⁻¹ * t⁻¹ ∈ N
  sorryAll goals completed! 🐙

Gleason's theorem (finite-dimensional)

gleason_theorem_finite

Submitter: Kim Morrison.

Notes: Gleason's theorem in finite dimensions: every frame function on the orthogonal projections of a complex Hilbert space of dimension at least 3 is given by P ↦ Tr(ρ P) for the unique density operator ρ. Stated using a bespoke `FrameFunction` structure (non-negative, additive on orthogonal projection pairs, normalized at the identity) and the standard Mathlib trace `LinearMap.trace`. Finite additivity on orthogonal pairs already implies countable additivity in finite dimensions, so the hypothesis matches Gleason's original σ-additive frame functions.

Source: A. M. Gleason, Measures on the closed subspaces of a Hilbert space, J. Math. Mech. 6 (1957), 885-893.

Informal solution: Gleason's original proof analyses regular frame functions on the unit sphere of R^3 by showing they are continuous and then quadratic, then promotes the resulting positive quadratic form on every 3-dimensional real subspace of H to a positive operator ρ on H whose diagonal in any orthonormal basis recovers the frame function, with Tr(ρ) = μ(I) = 1 ensuring ρ is a density operator.

theorem declaration uses `sorry`gleason_theorem_finite {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [FiniteDimensional ℂ H]
    (hdim : 3 ≤ Module.finrank ℂ H)
    (f : LeanEval.Analysis.FrameFunction H) :
    ∃! ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      reTr ρ = 1 ∧
      ∀ P : H →L[ℂ] H, LeanEval.Analysis.IsOrthProj P → f.μ P = reTr (ρ * P) := byH:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ Hinst✝¹:CompleteSpace Hinst✝:FiniteDimensional ℂ Hhdim:3 ≤ Module.finrank ℂ Hf:FrameFunction H⊢ ∃! ρ, ρ.IsPositive ∧ reTr ρ = 1 ∧ ∀ (P : H →L[ℂ] H), IsOrthProj P → f.μ P = reTr (ρ * P)
  sorryAll goals completed! 🐙

Gleason's theorem (separable Hilbert space)

gleason_theorem_separable

Submitter: Kim Morrison.

Notes: Gleason's theorem for a separable complex Hilbert space H of dimension at least 3, in Gleason's original `frame function on the unit sphere' formulation: any non-negative function on the unit sphere whose values sum to 1 along every Hilbert basis is given by x ↦ re ⟨x, ρ x⟩ for some positive bounded operator ρ. The Lean conclusion does not assert that ρ is trace-class with Tr(ρ) = 1; stating that would require trace-class infrastructure not yet at this Mathlib pin. This side-steps the absence of Schatten 1 / trace-class infrastructure in Mathlib at the time of writing.

Source: A. M. Gleason, Measures on the closed subspaces of a Hilbert space, J. Math. Mech. 6 (1957), 885-893.

Informal solution: Reduce to the real 3-dimensional case via restriction to real subspaces of H, where Gleason's continuity argument plus an analysis of regular frame functions on S^2 gives a positive quadratic form. Patch these forms together using rotation-invariance and the assumed basis-sum normalization to obtain a globally defined positive bounded operator ρ on H reproducing the frame function on every unit vector.

theorem declaration uses `sorry`gleason_theorem_separable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
    (hdim : 3 ≤ Module.rank ℂ H)
    (f : LeanEval.Analysis.SphereFrameFunction H) :
    ∃ ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      ∀ x : Metric.sphere (0 : H) 1,
        f.f x = (inner ℂ (x : H) (ρ (x : H))).re := byH:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ Hinst✝¹:CompleteSpace Hinst✝:TopologicalSpace.SeparableSpace Hhdim:3 ≤ Module.rank ℂ Hf:SphereFrameFunction H⊢ ∃ ρ, ρ.IsPositive ∧ ∀ (x : ↑(Metric.sphere 0 1)), f.f x = (inner ℂ (↑x) (ρ ↑x)).re
  sorryAll goals completed! 🐙

Gorenstein–Walter theorem (dihedral Sylow 2-subgroup)

gorenstein_walter

Submitter: Kim Morrison.

Notes: A finite nonabelian simple group with dihedral Sylow 2-subgroups is isomorphic to PSL₂(q) for some odd prime power q ≥ 5, or to A₇. D. Gorenstein and J. H. Walter, 'The characterization of finite groups with dihedral Sylow 2-subgroups', J. Algebra 2 (1965), 85-151, 218-270, 354-393 (in three parts, ~250 pages). The first major application of the Bender method in CFSG and a template for the later Sylow-2-structure papers. No new definitions: uses Mathlib's PSL notation, DihedralGroup, alternatingGroup, GaloisField, and Sylow.

Source: D. Gorenstein and J. H. Walter, The characterization of finite groups with dihedral Sylow 2-subgroups, J. Algebra 2 (1965), 85-151, 218-270, 354-393. https://doi.org/10.1016/0021-8693(65)90027-X

Informal solution: Three-part argument. Part I (Gorenstein-Walter): if G has dihedral Sylow 2-subgroup, then either G ≅ A₇, or O(G) — the largest normal subgroup of odd order — has G/O(G) of a very specific structure: an extension of PSL₂(q) for some odd q ≥ 5 by an outer automorphism. Part II rules out the outer-automorphism case using Brauer's theory of blocks of defect one and the analysis of involution centralizers (this is where the Bender method first appears). Part III shows O(G) = 1 under the simplicity hypothesis, using the Z*-theorem and signalizer functor methods. Combined, the simple G is isomorphic to PSL₂(q) for some odd q ≥ 5 or to A₇.

theorem declaration uses `sorry`gorenstein_walter (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (P : Sylow 2 G)
    (_hdih : ∃ n : ℕ, Nonempty ((P : Subgroup G) ≃* DihedralGroup n)) :
    Nonempty (G ≃* alternatingGroup (Fin 7)) ∨
    ∃ p k : ℕ, ∃ _hp : Fact p.Prime, Odd p ∧ 5 ≤ p ^ k ∧
      Nonempty (G ≃* PSL(2, GaloisField p k)) := byG:Typeinst✝²:Group Ginst✝¹:Finite Ginst✝:IsSimpleGroup Ghnonab:∃ a b, a * b ≠ b * aP:Sylow 2 G_hdih:∃ n, Nonempty (↥↑P ≃* DihedralGroup n)⊢ Nonempty (G ≃* ↥(alternatingGroup (Fin 7))) ∨
  ∃ p k, ∃ (_hp : Fact (Nat.Prime p)), Odd p ∧ 5 ≤ p ^ k ∧ Nonempty (G ≃* PSL(2, GaloisField p k))
  sorryAll goals completed! 🐙

Green–Tao theorem

green_tao

Submitter: Kim Morrison.

Notes: §37 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The set of primes contains arbitrarily long arithmetic progressions: for every k there exist a ≥ 0 and b ≥ 1 such that a + b·j is prime for every j < k. Mathlib has Dirichlet's theorem (Nat.infinite_setOf_prime_and_modEq) and Roth's theorem on 3-APs (roth_3ap_theorem_nat) but not Green-Tao. As of 2026 the theorem has not been formalized in any major proof assistant (a long-standing open formalization target).

Source: B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Ann. of Math. 167 (2008), 481-547 (announced 2004). Listed as §37 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: The proof has three main steps. (i) A transference principle: it suffices to find arbitrarily long APs in any set of positive density in a suitable pseudorandom super-set. (ii) Pseudorandomness of the primes after a `W-trick': removing small prime factors via a Selberg-style sieve makes the indicator function of the primes dominated by a pseudorandom measure ν. (iii) Apply Szemerédi's theorem in the relative form (a Furstenberg-style multiple recurrence / Gowers-uniformity argument) to that pseudorandom set, transferring the AP-rich conclusion back to the primes.

theorem declaration uses `sorry`green_tao : LeanEval.NumberTheory.ContainsArbitraryAPs {p : ℕ | Nat.Prime p} := by⊢ ContainsArbitraryAPs {p | Nat.Prime p}
  sorryAll goals completed! 🐙

Hadwiger's theorem

hadwiger

Submitter: Kim Morrison.

Notes: §31 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The real vector space of continuous, rigid-motion-invariant valuations on convex bodies in ℝⁿ has dimension n + 1. The problem defines the IsValuation predicate (continuity in the Hausdorff metric, inclusion-exclusion additivity, invariance under linear isometries and translations) and the valuations submodule. mathlib has ConvexBody with its Hausdorff MetricSpace but no valuations, intrinsic volumes, or Hadwiger's theorem; no formalization was found in any other proof assistant. The Submodule membership-closure fields of `valuations` are shipped as sorry (routine: valuations are closed under sum and scalar multiple).

Source: H. Hadwiger (1937). Listed as §31 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Hadwiger's classification: every continuous rigid-motion-invariant valuation on convex bodies in ℝⁿ is a linear combination of the n + 1 intrinsic volumes V₀, …, Vₙ (equivalently the coefficients of the Steiner polynomial Vol(K + tB) = ∑ⱼ aⱼ tʲ). The intrinsic volumes are linearly independent valuations, so they form a basis and the space has dimension exactly n + 1. The hard direction (every such valuation is a combination of intrinsic volumes) is Hadwiger's characterization theorem, proved by reduction to the one-dimensional case via the behaviour of valuations on simple convex bodies.

theorem declaration uses `sorry`hadwiger (n : ℕ) : Module.finrank ℝ (valuations n) = n + 1 := byn:ℕ⊢ Module.finrank ℝ ↥(valuations n) = n + 1
  sorryAll goals completed! 🐙

Gaussian heat kernel solves the 1D heat equation

heat_kernel_solves_heat_equation

Submitter: Kim Morrison.

Notes: The Gaussian convolution u(t,x) = (4 pi t)^{-1/2} integral exp(-(x-y)^2/(4t)) f(y) dy satisfies the heat equation on (0, infty) x R, with initial datum f recovered as t -> 0+.

Source: Classical heat-equation theory.

Informal solution: Differentiate under the integral sign in t and twice in x; the kernel itself satisfies the heat equation, so does its convolution with f. As t -> 0+, the Gaussian is an approximate identity with total mass 1. After the change of variables y = x + sqrt(t) z, the integral becomes an average of f(x + sqrt(t) z) against a fixed integrable Gaussian weight; continuity of f at x and boundedness of f then give pointwise convergence to f(x) by dominated convergence in z.

theorem declaration uses `sorry`heat_kernel_solves_heat_equation (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) :
    -- The PDE on (0, ∞) × ℝ.
    (∀ t : ℝ, 0 < t → ∀ x : ℝ, ∃ ux : ℝ → ℝ, ∃ uxx : ℝ,
        (∀ y : ℝ, HasDerivAt (fun z => heatSolution f t z) (ux y) y) ∧
        HasDerivAt ux uxx x ∧
        HasDerivAt (fun s => heatSolution f s x) uxx t) ∧
    -- Initial condition recovered as a one-sided limit at t = 0.
    (∀ x : ℝ,
        Filter.Tendsto (fun t : ℝ => heatSolution f t x)
          (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (f x))) := byf:ℝ → ℝhf_cont:Continuous fhf_bdd:∃ M, ∀ (x : ℝ), |f x| ≤ M⊢ (∀ (t : ℝ),
    0 < t →
      ∀ (x : ℝ),
        ∃ ux uxx,
          (∀ (y : ℝ), HasDerivAt (fun z => heatSolution f t z) (ux y) y) ∧
            HasDerivAt ux uxx x ∧ HasDerivAt (fun s => heatSolution f s x) uxx t) ∧
  ∀ (x : ℝ), Filter.Tendsto (fun t => heatSolution f t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))
  sorryAll goals completed! 🐙

Hopf–Rinow theorem

hopf_rinow

Submitter: Kim Morrison.

Notes: For a connected, finite-dimensional, smooth Riemannian manifold M that is also locally compact, metric completeness and geodesic completeness are equivalent. §93 of Knill's 'Some Fundamental Theorems in Mathematics'. The file ships IsGeodesic (a path with locally linear edist — a metric formulation of affinely parametrised local minimising geodesics, avoiding any Levi-Civita / connection infrastructure) and IsGeodesicallyComplete (every geodesic on a bounded open interval extends to all of ℝ).

Source: H. Hopf and W. Rinow, *Ueber den Begriff der vollständigen differentialgeometrischen Fläche*, Comment. Math. Helv. 3 (1931), 209-225. Listed as §93 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Standard Hopf–Rinow proof. Metric ⇒ geodesic completeness: a constant-speed geodesic γ : (a, b) → M is uniformly Cauchy as t → b⁻ because edist (γ s) (γ t) = c · |s − t|; the limit exists by metric completeness, and the geodesic ODE extends past the limit point using local existence of geodesics (Picard–Lindelöf on the tangent bundle). Geodesic ⇒ metric completeness: the central Hopf–Rinow lemma shows that under the smooth-Riemannian-and-locally-compact hypotheses, closed bounded subsets of M are compact (Heine–Borel). A Cauchy sequence is bounded, hence contained in a compact set, hence convergent.

theorem declaration uses `sorry`hopf_rinow {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E]
    {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
    (M : Type*) [EMetricSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
    [Bundle.RiemannianBundle (fun x : M => TangentSpace I x)]
    [IsRiemannianManifold I M]
    [LocallyCompactSpace M] [ConnectedSpace M] :
    LeanEval.Geometry.IsGeodesicallyComplete M ↔ CompleteSpace M := byE:Type u_1inst✝¹⁰:NormedAddCommGroup Einst✝⁹:NormedSpace ℝ Einst✝⁸:FiniteDimensional ℝ EH:Type u_2inst✝⁷:TopologicalSpace HI:ModelWithCorners ℝ E HM:Type u_3inst✝⁶:EMetricSpace Minst✝⁵:ChartedSpace H Minst✝⁴:IsManifold I ∞ Minst✝³:Bundle.RiemannianBundle fun x => TangentSpace I xinst✝²:IsRiemannianManifold I Minst✝¹:LocallyCompactSpace Minst✝:ConnectedSpace M⊢ IsGeodesicallyComplete M ↔ CompleteSpace M
  sorryAll goals completed! 🐙

Perron-Frobenius for irreducible nonnegative matrices

irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

Submitter: Kim Morrison.

Notes: A Perron-Frobenius style eigenvector existence statement at the spectral radius.

Source: Classical theorem in linear algebra.

Informal solution: Show that an irreducible nonnegative matrix has a strictly positive eigenvector with eigenvalue equal to its spectral radius.

theorem declaration uses `sorry`irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius {n : Type*} [Fintype n] [DecidableEq n] [Nonempty n]
    (A : Matrix n n ℝ)
    (hA : A.IsIrreducible) :
    ∃ v : n → ℝ,
      Module.End.HasEigenvector (Matrix.toLin' A) (spectralRadius ℝ A).toReal v ∧
      (∀ i, 0 < v i) := byn:Type u_1inst✝²:Fintype ninst✝¹:DecidableEq ninst✝:Nonempty nA:Matrix n n ℝhA:A.IsIrreducible⊢ ∃ v, Module.End.HasEigenvector (Matrix.toLin' A) (spectralRadius ℝ A).toReal v ∧ ∀ (i : n), 0 < v i
  sorryAll goals completed! 🐙

Isoperimetric inequality (n-dim, topological-frontier form)

isoperimetric_inequality

Submitter: Kim Morrison.

Notes: n-dimensional isoperimetric inequality for measurable bounded B ⊆ ℝⁿ, n ≥ 2: n^n · volume(B)^{n−1} · volume(closedBall 0 1) ≤ μHE[n−1](frontier B)^n, with μHE[n−1] the (n−1)-dim Euclidean Hausdorff measure on the topological frontier. The topological-frontier formulation is strictly weaker than the canonical De Giorgi finite-perimeter form: the topological frontier can strictly contain the reduced boundary, so this RHS is pointwise larger than the perimeter. For a smooth bounded domain with regular bounding hypersurface S = frontier B, μHE[n−1](frontier B) agrees with the classical surface area. The 2 ≤ n hypothesis excludes the n = 1 case where the ENNReal formulation has B = ∅ as a counterexample (0^0 · 2 = 2 ≠ 0). §71 of Knill's 'Some Fundamental Theorems in Mathematics'.

Source: Classical isoperimetric inequality; modern finite-perimeter / GMT formulations are due to E. De Giorgi and H. Federer. Listed as §71 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). The Wiedijk-100 entry 'The Isoperimetric Theorem' is unformalised in Lean.

Informal solution: Standard proofs work at the De Giorgi perimeter level via Brunn–Minkowski plus Steiner symmetrization: Steiner-symmetrize B with respect to n hyperplanes, each step preserves volume and decreases perimeter, converging to a ball B* of the same volume, where equality holds. Lower-semicontinuity of perimeter under Steiner symmetrization closes the inequality. The frontier version of this PR follows from the perimeter version because the De Giorgi perimeter is bounded above by μHE[n−1](frontier B). Alternative routes: optimal transport (Brenier / Knothe), Sobolev W^{1,1} → L^{n/(n−1)} via Federer–Fleming with co-area, or Gromov's proof.

theorem declaration uses `sorry`isoperimetric (n : ℕ) (_hn : 2 ≤ n) (B : Set (LeanEval.Geometry.E n))
    (_hB : MeasurableSet B) (_hBdd : Bornology.IsBounded B) :
    (n : ℝ≥0∞) ^ n * (volume B) ^ (n - 1) * volume (closedBall (0 : LeanEval.Geometry.E n) 1)
      ≤ (μHE[n - 1] (frontier B)) ^ n := byn:ℕ_hn:2 ≤ nB:Set (E n)_hB:MeasurableSet B_hBdd:Bornology.IsBounded B⊢ ↑n ^ n * volume B ^ (n - 1) * volume (closedBall 0 1) ≤ μHE[n - 1] (frontier B) ^ n
  sorryAll goals completed! 🐙

Jacobian of a smooth proper curve (Merten challenge)

jacobian_challenge_alggeo

Submitter: Christian Merten.

Notes: Unavailable.

Source: https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685

Informal solution: Build the Albanese variety of C as the universal abelian variety receiving a pointed map from C; Weil's construction of the Jacobian of a curve makes this concrete via Pic^0(C). The universal property is the no-cheating clamp.

/-- The genus of a smooth proper curve. -/
def declaration uses `sorry`genus (C : Over (Spec (.of k))) [IsProper C.hom] [SmoothOfRelativeDimension 1 C.hom]
    [GeometricallyIrreducible C.hom] : ℕ :=
  sorry

/-- The Jacobian of a smooth, proper curve over a field `k`. -/
def declaration uses `sorry`Jacobian (C : Over (Spec (.of k))) [IsProper C.hom] [SmoothOfRelativeDimension 1 C.hom]
    [GeometricallyIrreducible C.hom] : Over (Spec (.of k)) :=
  sorry

/-- The group scheme structure on the Jacobian of the curve `C`. -/
instance declaration uses `sorry`instGrpObj : GrpObj (Jacobian C) :=
  sorry

/-- The Jacobian of `C` is smooth of relative dimension `g` over `k`, where `g` is the
genus of `C`. -/
instance declaration uses `sorry`smoothOfRelativeDimension_genus :
    SmoothOfRelativeDimension (genus C) (Jacobian C).hom :=
  sorry

/-- The Jacobian of `C` is proper over `k`. -/
instance declaration uses `sorry`instIsProper : IsProper (Jacobian C).hom :=
  sorry

/-- The Jacobian of `C` is geometrically irreducible over `k`. -/
instance declaration uses `sorry`instGeometricallyIrreducible : GeometricallyIrreducible (Jacobian C).hom :=
  sorry

/-- The Abel-Jacobi map from a smooth, proper curve to its Jacobian associated
to a `k`-rational point of `C`. -/
def declaration uses `sorry`ofCurve (P : 𝟙_ (Over (Spec (.of k))) ⟶ C) : C ⟶ Jacobian C :=
  sorry

/-- The Abel-Jacobi map sends the `k`-rational point `P` to `0`, where `0` (denoted by `η` below) is
the neutral element of the group scheme `Jacobian C`. -/
theorem declaration uses `sorry`comp_ofCurve (C : Over (Spec (.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (.of k))) ⟶ C) :
    P ≫ ofCurve P = η[Jacobian C] :=
  sorry

/--
The universal property of the Jacobian variety: For any abelian variety `A`,
any morphism `f : C ⟶ A` such that `f(P) = 0` factors uniquely through the
Jacobian of `C`.
In other words, `Jacobian C` is the Albanese variety of `C`.
-/
theorem declaration uses `sorry`exists_unique_ofCurve_comp (C : Over (Spec (.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (.of k))) ⟶ C)
    {A : Over (Spec (.of k))} [Smooth A.hom] [IsProper A.hom] [GrpObj A]
    [GeometricallyIrreducible A.hom] (f : C ⟶ A) (hf : P ≫ f = η[A]) :
    ∃! (g : Jacobian C ⟶ A), f = ofCurve P ≫ g :=
  sorry

Jacobian of a compact Riemann surface (Buzzard challenge)

jacobian_challenge_diffgeo

Submitter: Kevin Buzzard.

Notes: Unavailable.

Source: https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge

Informal solution: Construct J(X) as H^0(X, Omega^1)* / H_1(X, Z), the period lattice quotient; the Abel-Jacobi map sends a point to the linear functional 'integrate from a fixed basepoint to here'. Functoriality and the projection formula come from pushforward and pullback of differential forms.

def declaration uses `sorry`genus (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ω X] : ℕ := sorry

theorem declaration uses `sorry`genus_eq_zero_iff_homeo :
    genus X = 0 ↔ Nonempty (X ≃ₜ (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)) :=
  sorry

def declaration uses `sorry`Jacobian (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ω X] : Type u := sorry

instance declaration uses `sorry`instAddCommGroup : AddCommGroup (Jacobian X) := sorry

instance declaration uses `sorry`instTopologicalSpace : TopologicalSpace (Jacobian X) := sorry

instance declaration uses `sorry`instT2Space : T2Space (Jacobian X) := sorry

instance declaration uses `sorry`instCompactSpace : CompactSpace (Jacobian X) := sorry

instance declaration uses `sorry`instChartedSpace : ChartedSpace (Fin (genus X) → ℂ) (Jacobian X) := sorry

instance declaration uses `sorry`instIsManifold :
    IsManifold (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (Jacobian X) := sorry

instance declaration uses `sorry`instLieAddGroup :
    LieAddGroup (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (Jacobian X) := sorry

def declaration uses `sorry`ofCurve (P : X) : X → Jacobian X := sorry

theorem declaration uses `sorry`ofCurve_contMDiff (P : X) :
    ContMDiff (modelWithCornersSelf ℂ ℂ)
      (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (ofCurve P) := sorry

theorem declaration uses `sorry`ofCurve_self (P : X) : ofCurve P P = 0 := sorry

theorem declaration uses `sorry`ofCurve_inj (P : X) (h : 0 < genus X) : Function.Injective (ofCurve P) := sorry

def declaration uses `sorry`pushforward (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    Jacobian X →ₜ+ Jacobian Y := sorry

theorem declaration uses `sorry`pushforward_contMDiff (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ContMDiff (modelWithCornersSelf ℂ (Fin (genus X) → ℂ))
      (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ)) ω (pushforward f hf) := sorry

theorem declaration uses `sorry`pushforward_id_apply (P : Jacobian X) :
    pushforward id contMDiff_id P = P := sorry

theorem declaration uses `sorry`pushforward_comp_apply (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω g)
    (P : Jacobian X) :
    pushforward (g ∘ f) (hg.comp hf) P = pushforward g hg (pushforward f hf P) :=
  sorry

def declaration uses `sorry`pullback (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    Jacobian Y →ₜ+ Jacobian X := sorry

theorem declaration uses `sorry`pullback_contMDiff (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ContMDiff (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ))
      (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (pullback f hf) := sorry

theorem declaration uses `sorry`pullback_id_apply (P : Jacobian X) :
    pullback id contMDiff_id P = P := sorry

theorem declaration uses `sorry`pullback_comp_apply (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω g)
    (P : Jacobian Z) :
    pullback (g.comp f) (hg.comp hf) P = pullback f hf (pullback g hg P) := sorry

def declaration uses `sorry`degree (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) : ℕ :=
  sorry -- 0 for constant case

theorem declaration uses `sorry`pushforward_pullback (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
    (P : Jacobian Y) :
    pushforward f hf (pullback f hf P) = (degree f hf) • P := sorry

Jordan–Brouwer separation theorem

jordan_brouwer

Submitter: Kim Morrison.

Notes: §48 of Knill's 'Some Fundamental Theorems in Mathematics'. The high-dimensional generalization of the Jordan curve theorem: for d ≥ 2, the complement in ℝᵈ of a topological (d-1)-sphere has exactly two connected components. The hypothesis 2 ≤ d is essential: in dimension d = 1 the (d-1)-sphere is the two-point set {-1, 1}, whose complement in ℝ has three connected components. Mathlib has Metric.sphere, EuclideanSpace, ConnectedComponents, Nat.card, but no Jordan–Brouwer separation theorem, no Alexander duality, no invariance of domain in a form that would discharge it. Stateable with zero new definitions.

Source: L. E. J. Brouwer, *Beweis des Jordanschen Satzes für den n-dimensionalen Raum*, Math. Annalen 71 (1912) (first proof). Listed as §48 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover.

Informal solution: Modern proofs use singular homology via Alexander duality: H̃_0(ℝᵈ ∖ Σ) ≅ H̃^{d-1}(Σ), and an embedded (d-1)-sphere Σ has H̃^{d-1}(Σ) ≅ ℤ, giving exactly two components. Brouwer's original proof used direct simplicial-approximation arguments without modern homology.

theorem declaration uses `sorry`jordan_brouwer (d : ℕ) (_hd : 2 ≤ d)
    (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 → EuclideanSpace ℝ (Fin d))
    (_hcont : Continuous r) (_hinj : Function.Injective r) :
    Nat.card
        (ConnectedComponents ((Set.range r)ᶜ : Set (EuclideanSpace ℝ (Fin d)))) =
      2 := byd:ℕ_hd:2 ≤ dr:↑(Metric.sphere 0 1) → EuclideanSpace ℝ (Fin d)_hcont:Continuous r_hinj:Function.Injective r⊢ Nat.card (ConnectedComponents ↑(Set.range r)ᶜ) = 2
  sorryAll goals completed! 🐙

Jordan curve theorem

jordan_curve

Submitter: Kim Morrison.

Notes: §48 of Knill's 'Some Fundamental Theorems in Mathematics'. Every continuous injection r : S¹ → ℝ² has a complement with exactly two connected components. Mathlib has Metric.sphere, EuclideanSpace, ConnectedComponents, and Nat.card, but no Jordan curve theorem (`grep -ri 'jordan curve' Mathlib/`: no hits), no winding numbers / invariance of domain in a form that would discharge it. Stateable with zero new definitions.

Source: C. Jordan, *Cours d'analyse* (1887, 2nd ed.; first statement and a famously gap-laden proof). The first rigorous proof is by O. Veblen, *Theory on plane curves in non-metrical analysis situs*, Trans. AMS 6 (1905). Listed as §48 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Formalized in Mizar (Korniłowicz et al., 2005) and HOL Light (Hales, 2007); not in Lean or Coq mathlib-equivalents.

Informal solution: Modern proofs use either singular homology of the complement (Alexander duality H̃_0(ℝ² ∖ C) ≅ H̃¹(S¹) = ℤ giving exactly two components) or planar combinatorics (approximate by polygonal Jordan curves, use winding-number parity to define inside/outside, transfer to the continuous curve via uniform convergence).

theorem declaration uses `sorry`jordan_curve (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 → EuclideanSpace ℝ (Fin 2))
    (_hcont : Continuous r) (_hinj : Function.Injective r) :
    Nat.card
        (ConnectedComponents ((Set.range r)ᶜ : Set (EuclideanSpace ℝ (Fin 2)))) =
      2 := byr:↑(Metric.sphere 0 1) → EuclideanSpace ℝ (Fin 2)_hcont:Continuous r_hinj:Function.Injective r⊢ Nat.card (ConnectedComponents ↑(Set.range r)ᶜ) = 2
  sorryAll goals completed! 🐙

Kakutani fixed-point theorem

kakutani_fixed_point

Submitter: Kim Morrison.

Notes: §33 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (additional statement of the game-theory section; underlies Nash's 1951 equilibrium-existence proof). The set-valued generalization of Brouwer: every upper-hemicontinuous correspondence F from a nonempty compact convex K ⊆ ℝᵈ to itself with nonempty convex closed values has a fixed point x ∈ F x. Mathlib's `grep -ri kakutani` returns only the Riesz-Markov-Kakutani representation theorem (a different theorem); the fixed-point theorem itself is not in mathlib.

Source: S. Kakutani, A generalization of Brouwer's fixed point theorem, Duke Math. J. 8 (1941), 457-459. Listed as an additional statement of §33 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Reduce to Brouwer by an approximation argument. Cover K by ε-balls and pick a finite subcover; on each ball define f_ε(x) := average of some selection from F(x) over the cover, producing a continuous single-valued ε-approximation f_ε : K → K. Apply Brouwer to f_ε to get a fixed point x_ε with x_ε ∈ F(x_ε) up to ε-error in the closed-graph sense. Take ε → 0 along a convergent subsequence (K compact); the limit point x is in the graph of F by upper hemicontinuity (closed graph), so x ∈ F(x).

theorem declaration uses `sorry`kakutani_fixed_point {d : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin d))}
    (_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
    (_hK_nonempty : K.Nonempty)
    (F : EuclideanSpace ℝ (Fin d) → Set (EuclideanSpace ℝ (Fin d)))
    (_hF_uhc : LeanEval.Topology.IsUpperHemicontinuous F)
    (_hF_nonempty : ∀ x ∈ K, (F x).Nonempty)
    (_hF_convex : ∀ x ∈ K, Convex ℝ (F x))
    (_hF_closed : ∀ x ∈ K, IsClosed (F x))
    (_hF_maps : ∀ x ∈ K, F x ⊆ K) :
    ∃ x ∈ K, x ∈ F x := byd:ℕK:Set (EuclideanSpace ℝ (Fin d))_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.NonemptyF:EuclideanSpace ℝ (Fin d) → Set (EuclideanSpace ℝ (Fin d))_hF_uhc:IsUpperHemicontinuous F_hF_nonempty:∀ x ∈ K, (F x).Nonempty_hF_convex:∀ x ∈ K, Convex ℝ (F x)_hF_closed:∀ x ∈ K, IsClosed (F x)_hF_maps:∀ x ∈ K, F x ⊆ K⊢ ∃ x ∈ K, x ∈ F x
  sorryAll goals completed! 🐙

Kolmogorov–Arnold superposition theorem (non-universal Lorentz form)

kolmogorov_arnold_superposition

Submitter: Kim Morrison.

Notes: Non-universal Lorentz-form existence statement of the Kolmogorov–Arnold superposition theorem on the closed cube Set.Icc (0 : Fin n → ℝ) 1. Both the outer function g : ℝ → ℝ and the inner functions φ_{k,l} : ℝ → ℝ may depend on f; this is weaker than formulations with universal inner functions. Resolves the continuous form of Hilbert's 13th problem since the two-variable combining function is addition.

Source: A. N. Kolmogorov, *On the representation of continuous functions of several variables by superposition of continuous functions of one variable and addition*, Doklady Akad. Nauk SSSR 114 (1957), 953-956. V. I. Arnold, *On functions of three variables*, Doklady Akad. Nauk SSSR 114 (1957), 679-681. G. G. Lorentz, *Metric entropy, widths, and superpositions of functions*, Amer. Math. Monthly 69 (1962), 469-485 (single-outer-function refinement). Listed as §80 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Standard consequence of the Kolmogorov–Arnold superposition theorem in Lorentz form: for each continuous f on [0, 1]^n, the theorem provides continuous one-variable inner functions and a single continuous outer function such that f is the stated finite sum over 2n+1 layers. The construction uses rationally-independent positive reals λ_1, …, λ_n and step-approximating monotone Lipschitz functions ψ_0, …, ψ_{2n} separating cells of a nested partition of [0, 1]; the inner sums y_k(x) = ∑_l λ_l ψ_k(x_l) distinguish nearby points of the cube in at least one of the 2n + 1 indices k. The outer function is built iteratively using uniform continuity of f. Functions originally defined only on the compact sets where they are used can be extended to continuous functions on ℝ by Tietze extension.

theorem declaration uses `sorry`kolmogorov_arnold (n : ℕ) (_hn : 1 ≤ n)
    (f : (Fin n → ℝ) → ℝ) (_hf : ContinuousOn f (Set.Icc 0 1)) :
    ∃ (g : ℝ → ℝ) (φ : Fin (2 * n + 1) → Fin n → ℝ → ℝ),
      Continuous g ∧ (∀ k l, Continuous (φ k l)) ∧
      ∀ x ∈ Set.Icc (0 : Fin n → ℝ) 1,
        f x = ∑ k, g (∑ l, φ k l (x l)) := byn:ℕ_hn:1 ≤ nf:(Fin n → ℝ) → ℝ_hf:ContinuousOn f (Set.Icc 0 1)⊢ ∃ g φ,
  Continuous g ∧
    (∀ (k : Fin (2 * n + 1)) (l : Fin n), Continuous (φ k l)) ∧ ∀ x ∈ Set.Icc 0 1, f x = ∑ k, g (∑ l, φ k l (x l))
  sorryAll goals completed! 🐙

Koszul formula

koszul_formula

Submitter: Kim Morrison.

Notes: §38 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement of the Riemannian-geometry section; the boxed main theorem is Levi-Civita). The Koszul formula: 2⟨∇_X Y, Z⟩ equals the cyclic sum of directional derivatives X·⟨Y,Z⟩ + Y·⟨X,Z⟩ − Z·⟨X,Y⟩ minus the Lie-bracket cyclic sum ⟨X,[Y,Z]⟩ + ⟨Y,[X,Z]⟩ − ⟨Z,[X,Y]⟩. The identity that forces uniqueness of the Levi-Civita connection. Mathlib has the covariant-derivative / Riemannian-bundle / Lie-bracket machinery but no metric-compatibility predicate and no Koszul formula. The Challenge ships one helper (IsMetricCompatible).

Source: J.-L. Koszul (course notes, 1950s); cf. do Carmo, Riemannian Geometry. Listed as §38 additional statement in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Direct algebraic manipulation from metric compatibility and torsion-freeness. Metric compatibility gives X·g(Y,Z) = g(∇_X Y, Z) + g(Y, ∇_X Z), and cyclic permutations Y·g(Z,X) and Z·g(X,Y). Torsion-freeness gives ∇_X Y − ∇_Y X = [X,Y] (and permutations). Form the linear combination X·g(Y,Z) + Y·g(X,Z) − Z·g(X,Y); expand each term via metric compatibility; substitute the torsion-free identities to convert ∇_X Z − ∇_Z X, ∇_Y Z − ∇_Z Y, and ∇_X Y − ∇_Y X into Lie brackets. The cross-terms ±g(∇_Y X, Z), ±g(∇_X Z, Y), ±g(∇_Y Z, X) collapse pairwise except for 2·g(∇_X Y, Z), yielding the formula.

theorem declaration uses `sorry`koszul_formula {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
      [FiniteDimensional ℝ E] [CompleteSpace E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
      [IsManifold I ∞ M]
    [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
    [IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)]
    (cov : CovariantDerivative I E (TangentSpace I (M := M)))
    [ContMDiffCovariantDerivative cov ∞]
    (_htor : cov.torsion = 0) (_hmet : LeanEval.Geometry.KoszulFormula.IsMetricCompatible cov)
    (X Y Z : Π x : M, TangentSpace I x)
    (_hX : CMDiff ∞ (T% X)) (_hY : CMDiff ∞ (T% Y)) (_hZ : CMDiff ∞ (T% Z))
    (x : M) :
    2 * inner ℝ (cov Y x (X x)) (Z x) =
      extDerivFun (fun y : M => inner ℝ (Y y) (Z y)) x (X x)
      + extDerivFun (fun y : M => inner ℝ (X y) (Z y)) x (Y x)
      - extDerivFun (fun y : M => inner ℝ (X y) (Y y)) x (Z x)
      - inner ℝ (X x) (mlieBracket I Y Z x)
      - inner ℝ (Y x) (mlieBracket I X Z x)
      + inner ℝ (Z x) (mlieBracket I X Y x) := byE:Type u_1inst✝¹⁰:NormedAddCommGroup Einst✝⁹:NormedSpace ℝ Einst✝⁸:FiniteDimensional ℝ Einst✝⁷:CompleteSpace EH:Type u_2inst✝⁶:TopologicalSpace HI:ModelWithCorners ℝ E HM:Type u_3inst✝⁵:TopologicalSpace Minst✝⁴:ChartedSpace H Minst✝³:IsManifold I ∞ Minst✝²:RiemannianBundle fun x => TangentSpace I xinst✝¹:IsContMDiffRiemannianBundle I ∞ E fun x => TangentSpace I xcov:CovariantDerivative I E (TangentSpace I)inst✝:cov.ContMDiffCovariantDerivative ∞_htor:cov.torsion = 0_hmet:IsMetricCompatible covX:(x : M) → TangentSpace I xY:(x : M) → TangentSpace I xZ:(x : M) → TangentSpace I x_hX:ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ fun x => ⟨x, X x⟩_hY:ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ fun x => ⟨x, Y x⟩_hZ:ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ fun x => ⟨x, Z x⟩x:M⊢ 2 * Inner.inner ℝ ((↑cov Y x) (X x)) (Z x) =
  (extDerivFun (fun y => Inner.inner ℝ (Y y) (Z y)) x) (X x) +
            (extDerivFun (fun y => Inner.inner ℝ (X y) (Z y)) x) (Y x) -
          (extDerivFun (fun y => Inner.inner ℝ (X y) (Y y)) x) (Z x) -
        Inner.inner ℝ (X x) (mlieBracket I Y Z x) -
      Inner.inner ℝ (Y x) (mlieBracket I X Z x) +
    Inner.inner ℝ (Z x) (mlieBracket I X Y x)
  sorryAll goals completed! 🐙

Fundamental theorem of Riemannian geometry (Levi-Civita)

levi_civita_exists_unique

Submitter: Kim Morrison.

Notes: §38 of Knill's 'Some Fundamental Theorems in Mathematics'. On a C^∞ finite-dimensional Riemannian manifold, there exists a unique smooth torsion-free metric-compatible covariant derivative on TM (the Levi-Civita connection); uniqueness is stated on the smooth-section subspace via `SameOnSmooth` since mathlib's `CovariantDerivative` is bundled over all sections. Mathlib has the covariant-derivative / Riemannian-bundle / Lie-bracket machinery but no metric-compatibility predicate and no Levi-Civita existence/uniqueness.

Source: T. Levi-Civita, Nozione di parallelismo in una varietà qualunque, Rend. Circ. Mat. Palermo 42 (1917). Listed as §38 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Existence + uniqueness via the Koszul formula. Solve 2·g(∇_X Y, Z) = X·g(Y,Z) + Y·g(X,Z) − Z·g(X,Y) − g(X,[Y,Z]) − g(Y,[X,Z]) + g(Z,[X,Y]) for the unknown ∇_X Y: the right-hand side is C^∞(M)-linear in Z and a derivation in Y, so by non-degeneracy of g it determines ∇_X Y as a smooth section. Direct verification that this `cov` is torsion-free and metric-compatible. For uniqueness: any other torsion-free metric-compatible smooth connection ∇' must satisfy the same Koszul identity, hence agrees with ∇ on smooth Y at every smooth X-direction.

theorem declaration uses `sorry`levi_civita_exists_unique {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
      [FiniteDimensional ℝ E] [CompleteSpace E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
      [IsManifold I ∞ M]
    [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
    [IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)] :
    ∃ cov : CovariantDerivative I E (TangentSpace I (M := M)),
      (ContMDiffCovariantDerivative cov ∞ ∧
        cov.torsion = 0 ∧ LeanEval.Geometry.LeviCivita.IsMetricCompatible cov) ∧
      ∀ cov' : CovariantDerivative I E (TangentSpace I (M := M)),
        (ContMDiffCovariantDerivative cov' ∞ ∧
          cov'.torsion = 0 ∧ LeanEval.Geometry.LeviCivita.IsMetricCompatible cov') →
        LeanEval.Geometry.LeviCivita.SameOnSmooth cov cov' := byE:Type u_1inst✝⁹:NormedAddCommGroup Einst✝⁸:NormedSpace ℝ Einst✝⁷:FiniteDimensional ℝ Einst✝⁶:CompleteSpace EH:Type u_2inst✝⁵:TopologicalSpace HI:ModelWithCorners ℝ E HM:Type u_3inst✝⁴:TopologicalSpace Minst✝³:ChartedSpace H Minst✝²:IsManifold I ∞ Minst✝¹:RiemannianBundle fun x => TangentSpace I xinst✝:IsContMDiffRiemannianBundle I ∞ E fun x => TangentSpace I x⊢ ∃ cov,
  (cov.ContMDiffCovariantDerivative ∞ ∧ cov.torsion = 0 ∧ IsMetricCompatible cov) ∧
    ∀ (cov' : CovariantDerivative I E (TangentSpace I)),
      cov'.ContMDiffCovariantDerivative ∞ ∧ cov'.torsion = 0 ∧ IsMetricCompatible cov' → SameOnSmooth cov cov'
  sorryAll goals completed! 🐙

Lidskii's inequality

lidskii_inequality

Submitter: Kim Morrison.

Notes: §99 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (additional statement of the section on spectral perturbation; the boxed main theorem lidskii_last is the p = 1 case combined with an entrywise bound). For self-adjoint complex matrices A, B with eigenvalues sorted in the same order and p ≥ 1, ∑_j |α_j - β_j|^p ≤ ∑_j |γ_j|^p where γ_j are the eigenvalues of B - A. Uses Matrix.IsHermitian.eigenvalues₀; mathlib has no Lidskii, Ky Fan, or Hoffman-Wielandt perturbation bounds, and no formalization of Lidskii's inequality was found in any other proof assistant. Companion problem: lidskii_last (#274) is the p = 1 entrywise-distance corollary.

Source: V. B. Lidskii, On the proper values of a sum and product of symmetric matrices, Dokl. Akad. Nauk SSSR 75 (1950), 769-772. Listed as an additional statement of §99 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: The eigenvalues of B = A + C interlace those of A according to Weyl's inequalities, giving componentwise α_j + γ_n ≤ β_j ≤ α_j + γ_1 for sorted eigenvalues; tightening this via the Ky Fan extremal characterization of partial sums of eigenvalues (∑_{j=1}^k α_j = max{tr(P A) : P projection of rank k}) yields the majorization ∑_{j=1}^k (β_j - α_j)_↓ ≤ ∑_{j=1}^k γ_j for sorted differences. Schur's theorem on Hermitian matrices then upgrades the partial-sum majorization to ∑_j |α_j - β_j|^p ≤ ∑_j |γ_j|^p for any convex function applied componentwise, in particular x ↦ |x|^p for p ≥ 1 (Hardy-Littlewood-Pólya / Hardy-Littlewood majorization principle).

theorem declaration uses `sorry`lidskii_inequality {n : Type*} [Fintype n] [DecidableEq n]
    {A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian)
    {p : ℝ} (_hp : 1 ≤ p) :
    ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ^ p ≤
      ∑ j, |(hB.sub hA).eigenvalues₀ j| ^ p := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℂB:Matrix n n ℂhA:A.IsHermitianhB:B.IsHermitianp:ℝ_hp:1 ≤ p⊢ ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ^ p ≤ ∑ j, |⋯.eigenvalues₀ j| ^ p
  sorryAll goals completed! 🐙

Lidskii–Last eigenvalue-perturbation theorem

lidskii_last

Submitter: Kim Morrison.

Notes: §99 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. For two self-adjoint complex n×n matrices A, B with eigenvalues sorted in the same order, the total eigenvalue displacement ∑|α_j - β_j| is bounded by the entrywise ℓ¹ distance ∑|A_ij - B_ij|. This is Last's theorem (≈1993), a consequence of Lidskii's inequality (1950). Uses Matrix.IsHermitian.eigenvalues₀; mathlib has no Lidskii, Ky Fan, or Hoffman-Wielandt perturbation bounds, and no formalization of the theorem was found in any other proof assistant.

Source: V. B. Lidskii (1950); the entrywise ℓ¹ form is due to Y. Last (around 1993). Listed as §99 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: By Lidskii's inequality the vector of sorted-eigenvalue displacements of A and B is majorized by the vector of eigenvalues of C := B - A (proved via the Ky Fan extremal characterization of partial sums of eigenvalues), so ∑_j |α_j - β_j| ≤ ∑_j |γ_j| with γ the eigenvalues of C. Then ∑_j |γ_j| ≤ ∑_{i,j} |C_ij|: for Hermitian C the ℓ¹ norm of the eigenvalues is dominated by the ℓ¹ norm of the matrix entries (bound each |γ_j| using the spectral decomposition and the triangle inequality). Combining the two gives the entrywise bound.

theorem declaration uses `sorry`lidskii_last {n : Type*} [Fintype n] [DecidableEq n]
    {A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) :
    ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ≤
      ∑ i, ∑ j, ‖A i j - B i j‖ := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℂB:Matrix n n ℂhA:A.IsHermitianhB:B.IsHermitian⊢ ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ≤ ∑ i, ∑ j, ‖A i j - B i j‖
  sorryAll goals completed! 🐙

Linear ODE with negative-real-part eigenvalues is asymptotically stable

linear_ode_asymptotic_stability

Submitter: Kim Morrison.

Notes: If every eigenvalue of A has negative real part, every solution of x' = Ax decays to zero in norm.

Source: Classical linear stability theory; Hirsch-Smale-Devaney.

Informal solution: Pass to the complexification; bring A to (Schur or Jordan) upper-triangular form; the matrix exponential satisfies ||exp(tA)|| <= C(1+t^{n-1}) exp(alpha t) for any alpha greater than the maximum real part of the spectrum, hence decays to 0. For any t_1 > 0, x(t) = exp((t - t_1) A) x(t_1) for t >= t_1 by uniqueness of the linear IVP, so ||x(t)|| -> 0 as t -> infty.

theorem declaration uses `sorry`linear_ode_asymptotic_stability (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : ∀ μ : ℂ,
        Module.End.HasEigenvalue
          (Matrix.toLin' (A.map (algebraMap ℝ ℂ))) μ → μ.re < 0)
    (x : ℝ → (Fin n → ℝ))
    (hx : ∀ t : ℝ, 0 < t → HasDerivAt x (A.mulVec (x t)) t) :
    Filter.Tendsto (fun t : ℝ => ‖x t‖) Filter.atTop (nhds 0) := byn:ℕA:Matrix (Fin n) (Fin n) ℝhA:∀ (μ : ℂ), Module.End.HasEigenvalue (Matrix.toLin' (A.map ⇑(algebraMap ℝ ℂ))) μ → μ.re < 0x:ℝ → Fin n → ℝhx:∀ (t : ℝ), 0 < t → HasDerivAt x (A *ᵥ x t) t⊢ Filter.Tendsto (fun t => ‖x t‖) Filter.atTop (nhds 0)
  sorryAll goals completed! 🐙

Liouville–Arnold theorem on integrable systems

liouville_arnold

Submitter: Kim Morrison.

Notes: §45 of Knill's 'Some Fundamental Theorems in Mathematics'. On a 2n-dimensional symplectic manifold with n smooth, pointwise linearly independent, pairwise Poisson-commuting first integrals F₁, …, F_n, every compact connected component of a joint level set is diffeomorphic to the n-torus T^n. Formalized on ℝ^{2n} with the standard symplectic form ω₀ = ∑ᵢ dpᵢ ∧ dqᵢ. Mathlib has EuclideanSpace, fderiv, AddCircle, Homeomorph but no Poisson brackets, no symplectic manifolds beyond Matrix.symplecticGroup, no first integrals, and no Liouville–Arnold theorem in any form (the Liouville files in Mathlib/Analysis/Complex/ are Liouville's theorem on bounded entire functions, a different result). The Challenge ships ~1 page of helper definitions (E, idxP, idxQ, poissonBracket, IsLiouvilleIntegrable, levelSet).

Source: V. I. Arnold, *Mathematical Methods of Classical Mechanics* (2nd ed., 1989), Theorem 49.A.1 (the standard modern reference). The result is due to Liouville (1855) for the local existence of action-angle coordinates and Arnold (1963) for the compact-connected-component topology. Listed as §45 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Joint hamiltonian flows of F₁, …, F_n commute (by Poisson-commutativity) and are everywhere transverse to the level set (by linear independence of the gradients), so each compact connected component carries a transitive free action of ℝⁿ. The stabilizer is a discrete subgroup of full rank n (compactness), hence isomorphic to ℤⁿ, exhibiting M_c as ℝⁿ/ℤⁿ ≃ T^n.

theorem declaration uses `sorry`liouville_arnold {n : ℕ} (F : Fin n → LeanEval.Geometry.LiouvilleArnold.E n → ℝ) (U : Set (LeanEval.Geometry.LiouvilleArnold.E n)) (_hU : IsOpen U)
    (_hLI : LeanEval.Geometry.LiouvilleArnold.IsLiouvilleIntegrable F U)
    (c : Fin n → ℝ)
    (_hMc_sub : LeanEval.Geometry.LiouvilleArnold.levelSet F c ⊆ U)
    (_hMc_compact : IsCompact (LeanEval.Geometry.LiouvilleArnold.levelSet F c))
    (_hMc_connected : IsConnected (LeanEval.Geometry.LiouvilleArnold.levelSet F c)) :
    Nonempty ((LeanEval.Geometry.LiouvilleArnold.levelSet F c) ≃ₜ (Fin n → AddCircle (1 : ℝ))) := byn:ℕF:Fin n → E n → ℝU:Set (E n)_hU:IsOpen U_hLI:IsLiouvilleIntegrable F Uc:Fin n → ℝ_hMc_sub:levelSet F c ⊆ U_hMc_compact:IsCompact (levelSet F c)_hMc_connected:IsConnected (levelSet F c)⊢ Nonempty (↑(levelSet F c) ≃ₜ (Fin n → AddCircle 1))
  sorryAll goals completed! 🐙

Existence of an order-10200960 group with a 22-dim irrep whose tensor square has 4 isotypic components

m23_irrep_tensor_square_decomp

Submitter: Kim Morrison.

Notes: Existential: a finite group G of order 10200960 (= |M₂₃|) with a 22-dimensional irreducible complex representation V whose tensor square (with the diagonal G-action) has exactly 4 isotypic components. Both the MonoidAlgebra ℂ G action on V and on V ⊗[ℂ] V are bound explicitly, with IsScalarTower and an explicit diagonal-action equation g•(v⊗w) = (g•v)⊗(g•w) pinning the V⊗V action. The intended witness is M₂₃ acting on its 22-dim irreducible: V ⊗ V = 1 ⊕ V ⊕ W₂₃₀ ⊕ Λ²V. While the formal statement does not technically require constructing M₂₃ and studying its representation theory, we suspect that in practice it does.

Source: É. Mathieu, Sur les fonctions cinq fois transitives de 24 quantités, J. Math. Pures Appl. (1873); ATLAS of Finite Groups, M₂₃ character table.

Informal solution: Realise M₂₃ as a subgroup of S₂₃ (e.g. via the Steiner system S(4,7,23) or as the automorphism group of a ternary Golay code construction). Take V to be the 22-dimensional deleted permutation representation. By 4-transitivity Sym²V is the permutation representation on the 23 choose 2 = 253 unordered pairs, decomposing as 1 + V + W₂₃₀ where W is the unique 230-dimensional irrep; Λ²V is irreducible of dimension 231, giving four pairwise non-isomorphic isotypic components in V⊗V.

theorem declaration uses `sorry`m23_irrep_tensor_square_decomp :
    ∃ (G : Type) (_ : Group G) (_ : Fintype G),
      Fintype.card G = 10200960 ∧
      ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
        (_ : Module (MonoidAlgebra ℂ G) V)
        (_ : IsScalarTower ℂ (MonoidAlgebra ℂ G) V)
        (_ : Module (MonoidAlgebra ℂ G) (V ⊗[ℂ] V))
        (_ : IsScalarTower ℂ (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)),
        Module.finrank ℂ V = 22 ∧
        IsSimpleModule (MonoidAlgebra ℂ G) V ∧
        (∀ (g : G) (v w : V),
          (MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • (v ⊗ₜ[ℂ] w) =
            ((MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • v) ⊗ₜ[ℂ]
              ((MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • w)) ∧
        (isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)).ncard = 4 := by⊢ ∃ G x x_1,
  Fintype.card G = 10200960 ∧
    ∃ V x_2 x_3 x_4,
      ∃ (x_5 : IsScalarTower ℂ (MonoidAlgebra ℂ G) V),
        ∃ x_6,
          ∃ (_ : IsScalarTower ℂ (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)),
            Module.finrank ℂ V = 22 ∧
              IsSimpleModule (MonoidAlgebra ℂ G) V ∧
                (∀ (g : G) (v w : V),
                    (MonoidAlgebra.of ℂ G) g • v ⊗ₜ[ℂ] w =
                      ((MonoidAlgebra.of ℂ G) g • v) ⊗ₜ[ℂ] ((MonoidAlgebra.of ℂ G) g • w)) ∧
                  (isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)).ncard = 4
  sorryAll goals completed! 🐙

Mandelbar (tricorn) is not path-connected (Hubbard–Schleicher)

mandelbar_not_path_connected

Submitter: Kim Morrison.

Notes: The d = 2 case of Hubbard–Schleicher's theorem that multicorns — connectedness loci of unicritical antiholomorphic polynomials z ↦ z̄^d + c — are not path-connected for d ≥ 2. For d = 2 this is the mandelbar / tricorn, the connectedness locus of z ↦ z̄² + c. The file ships Tantibar and Mandelbar definitions. Knill writes the iterator as z̄ + c (degree 1), but with that literal map the connectedness locus is the imaginary axis — path-connected, contradicting the claim. The formal statement uses the standard degree-2 form.

Source: John H. Hubbard and Dierk Schleicher, *Multicorns are not Path Connected*, arXiv:1209.1753 (2012); published in *Frontiers in Complex Dynamics* (Princeton University Press, 2014), pp. 73-102. Listed as §62 (additional statement 2) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: This is the d = 2 case of Hubbard–Schleicher's theorem that no multicorn for d ≥ 2 is path-connected. They study the connectedness loci of unicritical antiholomorphic polynomials z ↦ z̄^d + c and show that certain odd-period hyperbolic components cannot be connected to the principal component by paths inside the multicorn. Specialising to d = 2 gives that the mandelbar / tricorn is not path-connected.

theorem declaration uses `sorry`mandelbar_not_path_connected : ¬ IsPathConnected LeanEval.ComplexAnalysis.Mandelbar := by⊢ ¬IsPathConnected Mandelbar
  sorryAll goals completed! 🐙

Mandelbrot set is connected (Douady–Hubbard)

mandelbrot_connected

Submitter: Kim Morrison.

Notes: The Mandelbrot set for the quadratic family T_c(z) = z² + c is the parameter set for which the critical orbit of 0 is bounded. This problem states Douady–Hubbard's connectedness theorem. §62 of Knill's 'Some Fundamental Theorems in Mathematics'.

Source: A. Douady and J. H. Hubbard, *Étude dynamique des polynômes complexes I, II*, Publ. Math. Orsay 84-02, 85-04. Listed as §62 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Use the Douady–Hubbard uniformisation: the Böttcher coordinate at infinity gives a conformal isomorphism from ℂ \ M to the exterior of the closed unit disk. Equivalently, after adjoining ∞, the complement of M in the Riemann sphere is simply connected, hence M is connected.

theorem declaration uses `sorry`mandelbrot_connected : IsConnected LeanEval.ComplexAnalysis.MandelbrotProblem.Mandelbrot := by⊢ IsConnected Mandelbrot
  sorryAll goals completed! 🐙

Minkowski-Caratheodory theorem

mem_convexHull_finset_extremePoints_of_mem_compact_convex

Submitter: Kim Morrison.

Notes: Finite-dimensional compact convex sets are generated by their extreme points, with a finrank + 1 bound.

Source: Classical theorem in convex geometry.

Informal solution: Combine Krein-Milman with Caratheodory to represent each point as a convex combination of at most finrank + 1 extreme points.

theorem declaration uses `sorry`mem_convexHull_finset_extremePoints_of_mem_compact_convex {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {s : Set E} {x : E}
    (hscomp : IsCompact s)
    (hsconv : Convex ℝ s)
    (hx : x ∈ s) :
    ∃ t : Finset E,
      (↑t : Set E) ⊆ s.extremePoints ℝ ∧
      t.card ≤ Module.finrank ℝ E + 1 ∧
      x ∈ convexHull ℝ (↑t : Set E) := byE:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:FiniteDimensional ℝ Es:Set Ex:Ehscomp:IsCompact shsconv:Convex ℝ shx:x ∈ s⊢ ∃ t, ↑t ⊆ extremePoints ℝ s ∧ t.card ≤ Module.finrank ℝ E + 1 ∧ x ∈ (convexHull ℝ) ↑t
  sorryAll goals completed! 🐙

Mergelyan's theorem

mergelyan_theorem

Submitter: Kim Morrison.

Notes: Mergelyan's theorem: if K ⊆ ℂ is compact with connected complement, then every function continuous on K and holomorphic on interior K is uniformly approximable on K by complex polynomials. §64 of Knill's 'Some Fundamental Theorems in Mathematics'.

Source: S. N. Mergelyan, *On the representation of functions by series of polynomials on closed sets*, Doklady Akad. Nauk SSSR 78 (1951), 405-408 (Russian). Listed as §64 (additional statement 4) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: A standard proof approximates f uniformly on K by an entire function, using Cauchy–Green / Pompeiu or related ∂̄ methods, and then approximates the entire function uniformly on the compact set K by Taylor polynomials.

theorem declaration uses `sorry`mergelyan (K : Set ℂ) (_hK : IsCompact K) (_hKc : IsConnected (Kᶜ))
    (f : ℂ → ℂ) (_hfc : ContinuousOn f K) (_hfh : AnalyticOnNhd ℂ f (interior K))
    (ε : ℝ) (_hε : 0 < ε) :
    ∃ p : ℂ[X], ∀ z ∈ K, ‖f z - p.eval z‖ < ε := byK:Set ℂ_hK:IsCompact K_hKc:IsConnected Kᶜf:ℂ → ℂ_hfc:ContinuousOn f K_hfh:AnalyticOnNhd ℂ f (interior K)ε:ℝ_hε:0 < ε⊢ ∃ p, ∀ z ∈ K, ‖f z - Polynomial.eval z p‖ < ε
  sorryAll goals completed! 🐙

Milnor's exotic 7-sphere

milnor_exotic_sphere_seven

Submitter: Kim Morrison.

Notes: Existence of a smooth 7-manifold homeomorphic but not diffeomorphic to 𝕊⁷. Recorded as `proof_wanted exists_homeomorph_isEmpty_diffeomorph_sphere_seven` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Milnor's 1956 discovery and the birth of differential topology as a distinct subject. The construction uses S³-bundles over S⁴; the non-diffeomorphism is detected by Milnor's λ-invariant built from the signature of an 8-manifold bounding the candidate (Hirzebruch's signature theorem + an integrality / mod-7 argument).

Source: J. Milnor, On manifolds homeomorphic to the 7-sphere, Ann. of Math. 64 (1956), 399-405. Recorded as a `proof_wanted` in Mathlib/Geometry/Manifold/PoincareConjecture.lean at rev 5450b53e5ddc.

Informal solution: Milnor's construction: for k ∈ ℤ let M_k → S⁴ be the S³-bundle whose Euler number is k+1 and first Pontryagin class is 2(2k+1). Each M_k carries a natural smooth structure and is, by direct construction of a Morse function with two critical points, homeomorphic to S⁷. To detect that M_k is not diffeomorphic to S⁷ for k ≢ 0 (mod 7), Milnor introduced the invariant λ(M) ∈ ℤ/7 by computing λ(M) = (2σ(W) − p₁(W)²) / 7 mod 7 for any smooth 8-manifold W with ∂W = M (Hirzebruch's signature theorem makes 2σ(W) − p₁(W)² divisible by 7); a Mayer-Vietoris / cobordism argument shows λ is well-defined and a diffeomorphism invariant. For the bundles M_k a direct calculation gives λ(M_k) ≡ k(k+1) mod 7, which is nonzero for k = 1 (and many other k); the corresponding M_1 is therefore an exotic 7-sphere.

theorem declaration uses `sorry`milnor_exotic_sphere_seven :
    ∃ (M : Type) (_ : TopologicalSpace M)
      (_ : ChartedSpace (EuclideanSpace ℝ (Fin 7)) M)
      (_ : IsManifold (𝓡 7) ∞ M)
      (_homeo : M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 8)) 1),
      IsEmpty (M ≃ₘ⟮𝓡 7, 𝓡 7⟯ sphere (0 : EuclideanSpace ℝ (Fin 8)) 1) := by⊢ ∃ M x x_1, ∃ (_ : IsManifold (𝓡 7) ∞ M), ∃ _homeo, IsEmpty (M ≃ₘ⟮𝓡 7, 𝓡 7⟯ ↑(sphere 0 1))
  sorryAll goals completed! 🐙

Morley's categoricity theorem

morley_categoricity_theorem

Submitter: A. M. Berns.

Notes: A complete theory in a countable language with only infinite models that is categorical in some uncountable cardinal is categorical in every uncountable cardinal.

Source: M. Ramsey, *Morley's Categoricity Theorem* (UChicago VIGRE REU 2010), Corollary 7.3. https://www.math.uchicago.edu/~may/VIGRE/VIGRE2010/REUPapers/RamseyN.pdf

Informal solution: Show that categoricity in an uncountable cardinal forces the theory to be ω-stable, and then use Vaughtian pairs to prove that any two models of the same uncountable size are isomorphic and categoricity transfers to all uncountable cardinals.

theorem declaration uses `sorry`morley_categoricity_theorem (L : FirstOrder.Language.{0, 0}) (hL : L.card ≤ ℵ₀)
    (T : L.Theory) (hT : T.IsComplete)
    (hInf : ∀ M : FirstOrder.Language.Theory.ModelType.{0, 0, 0} T, Infinite M)
    {κ : Cardinal.{0}} (hκ : ℵ₀ < κ) (hcat : κ.Categorical T)
    {μ : Cardinal.{0}} (hμ : ℵ₀ < μ) :
    μ.Categorical T := byL:FirstOrder.LanguagehL:L.card ≤ ℵ₀T:L.TheoryhT:T.IsCompletehInf:∀ (M : T.ModelType), Infinite ↑Mκ:Cardinal.{0}hκ:ℵ₀ < κhcat:κ.Categorical Tμ:Cardinal.{0}hμ:ℵ₀ < μ⊢ μ.Categorical T
  sorryAll goals completed! 🐙

Morse inequalities

morse_inequality

Submitter: Kim Morrison.

Notes: §40 of Knill's 'Some Fundamental Theorems in Mathematics' (Marston Morse, 1934). For a Morse function f on a closed smooth finite-dimensional manifold M, ∑_{j≤k}(−1)^{k−j} c_j(f) ≥ ∑_{j≤k}(−1)^{k−j} b_j(M) for every k. Mathlib has the smooth-manifold framework, mfderiv, higher Fréchet derivatives, and singularHomologyFunctor but no Morse functions, Morse index, critical-point counts, Betti numbers as a named definition, or the Morse inequalities. The Challenge ships seven helper definitions (IsCriticalPoint, localHessian, IsNondegenerateCritical, IsMorseFunction, morseIndex, morseCount, bettiNumber, alternatingPartialSum).

Source: M. Morse, The Calculus of Variations in the Large, AMS Colloq. Publ. 18 (1934). Listed as §40 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Strong Morse inequality via the Morse-Smale complex: order the critical points by increasing critical value t_1 < t_2 < … < t_N and consider the sublevel sets M_t = f⁻¹((−∞,t]). Crossing a critical value attaches a k-cell where k is the Morse index, so M_t is obtained from M_{t−} by attaching one k-cell per index-k critical point at level t (Morse lemma + handle attachment). This gives a CW structure on M with c_k cells in dimension k, hence a chain complex C_k = ℤ^{c_k} computing H_k(M; ℤ). The strong inequality follows from the rank-nullity-style relation rank H_k = c_k − rank ∂_{k+1} − rank ∂_k applied to alternating partial sums, combined with subadditivity of rank under boundary maps.

theorem declaration uses `sorry`morse_inequality {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless]
    {M : Type} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
    [CompactSpace M] (f : M → ℝ) (_hf : LeanEval.Geometry.MorseInequalities.IsMorseFunction I f) (k : ℕ) :
    LeanEval.Geometry.MorseInequalities.alternatingPartialSum (bettiNumber M) k ≤
      LeanEval.Geometry.MorseInequalities.alternatingPartialSum (morseCount I f) k := byE:Type u_1inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace ℝ Einst✝⁶:FiniteDimensional ℝ EH:Type u_2inst✝⁵:TopologicalSpace HI:ModelWithCorners ℝ E Hinst✝⁴:I.BoundarylessM:Typeinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:IsManifold I ∞ Minst✝:CompactSpace Mf:M → ℝ_hf:IsMorseFunction I fk:ℕ⊢ alternatingPartialSum (bettiNumber M) k ≤ alternatingPartialSum (morseCount I f) k
  sorryAll goals completed! 🐙

Cayley graph connected iff generators generate the group

mulCayley_connected_iff_closure_eq_top

Submitter: Kim Morrison.

Notes: A foundational result in geometric group theory using the newly defined Cayley graph. Connectivity of the Cayley graph is equivalent to the generating set S generating G as a group.

Source: A. Cayley, On the theory of groups, as depending on the symbolic equation θ^n = 1, 1878.

Informal solution: Forward: if connected, any g ∈ G is reached from 1 by a path, which corresponds to a product of generators. Reverse: if S generates, any g is a product of generators, giving a path from 1 to g.

theorem declaration uses `sorry`mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G]
    (S : Set G) :
    (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := byG:Type u_1inst✝:Group GS:Set G⊢ (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤
  sorryAll goals completed! 🐙

Nash equilibrium existence theorem

nash_equilibrium_exists

Submitter: Kim Morrison.

Notes: §33 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (the section's boxed main theorem). Every finite n-player game in mixed strategies admits at least one Nash equilibrium. Mathlib has stdSimplex ℝ S (the natural model of a mixed strategy) and finite-sum/product machinery but no game theory at all — no Mathlib/GameTheory/ module, and grep for nash/mixed.strategy/best.response returns nothing relevant. No formalization of Nash equilibrium existence was found in any major proof assistant.

Source: J. F. Nash, Equilibrium points in n-person games, Proc. Nat. Acad. Sci. U.S.A. 36 (1950), 48-49; Non-cooperative games, Ann. of Math. 54 (1951), 286-295. Listed as §33 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Nash's 1950 proof (via Brouwer): define the best-response function r : Δ → Δ on the product of mixed-strategy simplices Δ = ∏ᵢ Δ(Sᵢ), where r(σ)ᵢ(sᵢ) = (σᵢ(sᵢ) + max(0, gain_i(σ, sᵢ))) / (normalization), and gain_i(σ, sᵢ) is the improvement player i would get by playing the pure strategy sᵢ against σ_{-i}. r is continuous and Δ is nonempty compact convex; Brouwer gives a fixed point σ*, and a short calculation shows σ* must be a Nash equilibrium (the only fixed points of r are exactly the equilibria). Nash's 1951 proof uses Kakutani directly: the best-response correspondence (set-valued, not single-valued) is upper-hemicontinuous with nonempty convex values; apply Kakutani to get a fixed point.

theorem declaration uses `sorry`nash_equilibrium_exists {n : ℕ} {S : Fin n → Type*}
    [∀ i, Fintype (S i)] [∀ i, Nonempty (S i)]
    (u : Fin n → LeanEval.GameTheory.StrategyProfile n S → ℝ) :
    ∃ σ : ∀ i, S i → ℝ, LeanEval.GameTheory.IsNashEquilibrium u σ := byn:ℕS:Fin n → Type u_1inst✝¹:(i : Fin n) → Fintype (S i)inst✝:∀ (i : Fin n), Nonempty (S i)u:Fin n → StrategyProfile n S → ℝ⊢ ∃ σ, IsNashEquilibrium u σ
  sorryAll goals completed! 🐙

Neukirch–Uchida theorem

neukirch_uchida

Submitter: Junyan Xu.

Notes: Unavailable.

Source: Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1.

Informal solution: Unavailable.

theorem declaration uses `sorry`neukirch_uchida {K₁ K₂ K₁' K₂' : Type*} [Field K₁] [Field K₂] [Field K₁'] [Field K₂']
    [NumberField K₁] [NumberField K₂] [Algebra K₁ K₁'] [Algebra K₂ K₂'] [IsSepClosure K₁ K₁']
    [IsSepClosure K₂ K₂'] (ϕ : Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)) (he : IsHomeomorph ϕ) :
    ∃! σ : K₂' ≃+* K₁', (algebraMap K₂ K₂').range.map σ.toRingHom = (algebraMap K₁ K₁').range ∧
      ∀ g : Gal(K₁'/K₁), ϕ g = σ.trans (g.toRingEquiv.trans σ.symm) := byK₁:Type u_1K₂:Type u_2K₁':Type u_3K₂':Type u_4inst✝⁹:Field K₁inst✝⁸:Field K₂inst✝⁷:Field K₁'inst✝⁶:Field K₂'inst✝⁵:NumberField K₁inst✝⁴:NumberField K₂inst✝³:Algebra K₁ K₁'inst✝²:Algebra K₂ K₂'inst✝¹:IsSepClosure K₁ K₁'inst✝:IsSepClosure K₂ K₂'ϕ:Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)he:IsHomeomorph ⇑ϕ⊢ ∃! σ,
  Subring.map σ.toRingHom (algebraMap K₂ K₂').range = (algebraMap K₁ K₁').range ∧
    ∀ (g : Gal(K₁'/K₁)), (ϕ g).toRingEquiv = σ.trans (g.toRingEquiv.trans σ.symm)
  sorryAll goals completed! 🐙

Oppenheim's inequality for Hadamard products

oppenheim_inequality

Submitter: Kim Morrison.

Notes: Oppenheim's 1930 inequality: for PSD matrices A, B, det(A ⊙ B) ≥ det(A) · ∏ᵢ Bᵢᵢ. Uses the Schur product theorem (newly formalized) as a key ingredient.

Source: I. Schur, Bemerkungen zur Theorie der beschränkten Bilinearformen, 1911; A. Oppenheim, Inequalities connected with definite Hermitian forms, 1930.

Informal solution: Use induction on the matrix size, extracting a Schur complement at each step and applying the Schur product theorem to bound the determinant.

theorem declaration uses `sorry`oppenheim_inequality {n : Type*} [Fintype n] [DecidableEq n]
    {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) :
    A.det * ∏ i, B i i ≤ (A ⊙ B).det := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝB:Matrix n n ℝhA:A.PosSemidefhB:B.PosSemidef⊢ A.det * ∏ i, B i i ≤ (A ⊙ B).det
  sorryAll goals completed! 🐙

Ornstein–Weiss ℤᵈ Rokhlin lemma

ornstein_weiss_rokhlin

Submitter: Kim Morrison.

Notes: §109 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement; the boxed main theorem is the classical Rokhlin lemma). The multidimensional generalization: for every free measure-preserving ℤᵈ-action T on a standard Borel probability space, every box size N ≥ 1, and every ε > 0, there is a measurable base B such that the translates T v '' B for v ∈ [0, N)ᵈ are pairwise disjoint with measure ≥ 1 - ε. Three hypotheses beyond the classical lemma: 1 ≤ d (rules out d = 0 degeneracy); the identity axiom T 0 = id (homomorphism alone only forces T 0 idempotent); [StandardBorelSpace Ω] (rules out the countable-cocountable σ-algebra defect). Mathlib has MeasurePreserving, IsProbabilityMeasure, Set.PairwiseDisjoint, Fintype.piFinset, Finset.Ico, StandardBorelSpace, but no Ornstein–Weiss lemma, no free measure-preserving ℤᵈ-actions, no multidimensional Rokhlin towers. The Challenge ships two small helper defs (IsFreeAction, boxShape).

Source: D. S. Ornstein and B. Weiss, *Entropy and isomorphism theorems for actions of amenable groups*, J. Anal. Math. 48 (1987), 1-141 — Theorem 5.2 establishes the multidimensional (and amenable-group) Rokhlin lemma. Listed as §109 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover.

Informal solution: Standard proof reduces to the one-dimensional Rokhlin lemma by induction on d using the quasi-tiling lemma of Ornstein–Weiss: every Følner set in ℤᵈ can be ε-quasi-tiled by finitely many translates of cubes [0, N)ᵈ, so a one-dimensional skyscraper over a transversal of one direction can be folded into a d-dimensional Rokhlin tower with arbitrarily small remainder.

theorem declaration uses `sorry`ornstein_weiss_rokhlin {Ω : Type*} [MeasurableSpace Ω]
    [StandardBorelSpace Ω]
    {d : ℕ} (_hd : 1 ≤ d) (μ : Measure Ω) [IsProbabilityMeasure μ]
    (T : (Fin d → ℤ) → Ω → Ω)
    (_hid : ∀ x, T 0 x = x)
    (_hT : ∀ v, MeasurePreserving (T v) μ μ)
    (_hgrp : ∀ u v x, T (u + v) x = T u (T v x))
    (_hfree : LeanEval.Dynamics.IsFreeAction μ T)
    (N : ℕ) (_hN : 1 ≤ N) {ε : ENNReal} (_hε : 0 < ε) :
    ∃ B : Set Ω,
      MeasurableSet B ∧
      ((boxShape d N : Finset (Fin d → ℤ)) : Set (Fin d → ℤ)).PairwiseDisjoint
        (fun v => T v '' B) ∧
      μ (⋃ v ∈ boxShape d N, T v '' B) ≥ 1 - ε := byΩ:Type u_1inst✝²:MeasurableSpace Ωinst✝¹:StandardBorelSpace Ωd:ℕ_hd:1 ≤ dμ:Measure Ωinst✝:IsProbabilityMeasure μT:(Fin d → ℤ) → Ω → Ω_hid:∀ (x : Ω), T 0 x = x_hT:∀ (v : Fin d → ℤ), MeasurePreserving (T v) μ μ_hgrp:∀ (u v : Fin d → ℤ) (x : Ω), T (u + v) x = T u (T v x)_hfree:IsFreeAction μ TN:ℕ_hN:1 ≤ Nε:ENNReal_hε:0 < ε⊢ ∃ B, MeasurableSet B ∧ ((↑(boxShape d N)).PairwiseDisjoint fun v => T v '' B) ∧ μ (⋃ v ∈ boxShape d N, T v '' B) ≥ 1 - ε
  sorryAll goals completed! 🐙

Independence of the parallel postulate

parallel_postulate_independent

Submitter: Kim Morrison.

Notes: Theorem #12 on Freek Wiedijk's 'Formalizing 100 Theorems' list (https://www.cs.ru.nl/~freek/100/). Euclid's parallel postulate is independent of the remaining axioms of plane geometry. Stated via Tarski's axiomatization: the `TarskiAbsolute` class bundles betweenness and congruence with axioms A1-A9 and the continuity axiom A11, the Euclidean axiom A10 is a separate Prop, and independence is the conjunction of two existentials (a model satisfying A10, a model refuting it). Cross-checked against the two existing formalizations on Freek's list: John Harrison's HOL Light (Multivariate/tarski.ml + 100/independence.ml) and Tim Makarios's Isabelle/AFP entry Tarskis_Geometry; axioms A1-A10 match Harrison's TARSKI_AXIOM_n character-for-character and A11 is his second-order continuity axiom.

Source: Independence of Euclid's parallel postulate; the hyperbolic-plane models are due to E. Beltrami (1868) and F. Klein (1871). Tarski's axiomatization: W. Schwabhäuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Springer (1983). Formalized in HOL Light by John Harrison and in Isabelle by Tim Makarios (T.J.M. Makarios, A Mechanical Verification of the Independence of Tarski's Euclidean Axiom, MSc thesis, Victoria University of Wellington, 2012; Isabelle/AFP entry Tarskis_Geometry).

Informal solution: Exhibit two models of `TarskiAbsolute` (axioms A1-A9, A11). For the Euclidean existential, take the real coordinate plane ℝ² with `B` the metric betweenness and `C` segment-length equality; it satisfies all of A1-A11 including the Euclidean axiom A10. For the non-Euclidean existential, take the Klein-Beltrami disk model of the hyperbolic plane: points are the open unit disk, betweenness and congruence are defined from cross-ratios / the projective structure; it satisfies A1-A9 and A11 but refutes A10 (through a point not on a line there is more than one parallel). Verifying the axioms for the Klein model is the substantial part — Makarios's Isabelle development and Harrison's HOL Light file both carry it out in full.

theorem declaration uses `sorry`parallel_postulate_independent :
    (∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), LeanEval.Geometry.Euclidean M T) ∧
    (∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), ¬ LeanEval.Geometry.Euclidean M T) := by⊢ (∃ M T, Euclidean M T) ∧ ∃ M T, ¬Euclidean M T
  sorryAll goals completed! 🐙

A competition programming problem about permuting a permutation to be unimodal

permute_to_unimodal

Submitter: Julia M. Himmel.

Notes: Unavailable.

Source: NWERC 2025 Problem G, see https://2025.nwerc.eu/problem-set.pdf

Informal solution: See https://2025.nwerc.eu/solutions.pdf for a sketch of the correctness, which goes in two steps: construct a quadratic-time dynamic programming solution, then efficiently evaluate that in O(n log n). The hard part is showing the correspondence between LISs of prefixes of the constructed sequence and values of the DP.

theorem declaration uses `sorry`minRearrange_correct {arr : Array Nat} :
    arr.Perm (1...=arr.size).toArray →
      (∃ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x ∧ LeanEval.ProgramVerification.differences (Vector.mk x (byarr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size simpa using hx.size_eqAll goals completed! 🐙)) arr.toVector = LeanEval.ProgramVerification.minRearrange arr) ∧
      (∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x → LeanEval.ProgramVerification.minRearrange arr ≤ LeanEval.ProgramVerification.differences (Vector.mk x (byarr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size simpa using hx.size_eqAll goals completed! 🐙)) arr.toVector) := byarr:Array Nat⊢ arr.Perm (1...=arr.size).toArray →
  (∃ x hx, Unimodal x ∧ differences (Vector.mk x ⋯) arr.toVector = minRearrange arr) ∧
    ∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray),
      Unimodal x → minRearrange arr ≤ differences (Vector.mk x ⋯) arr.toVector
  sorryAll goals completed! 🐙

pi_1 of the circle is Z

pi1_circle_mulEquiv_int

Submitter: Kim Morrison.

Notes: Computes the fundamental group of the complex unit circle.

Source: Classical theorem in algebraic topology.

Informal solution: Use winding number to identify loops in the circle up to homotopy with the integers.

theorem declaration uses `sorry`pi1_circle_mulEquiv_int :
    Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := by⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ)
  sorryAll goals completed! 🐙

pi_3 of the 2-sphere is Z

pi3_sphere_two_mulEquiv_int

Submitter: Kim Morrison.

Notes: The classical computation pi_3(S^2) = Z, with an explicit basepoint.

Source: Classical theorem in algebraic topology.

Informal solution: Use the Hopf fibration to identify the third homotopy group of the 2-sphere with the integers.

theorem declaration uses `sorry`pi3_sphere_two_mulEquiv_int (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) :
    Nonempty
      (HomotopyGroup.Pi 3 (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) x ≃*
        Multiplicative ℤ) := byx:↑(Metric.sphere 0 1)⊢ Nonempty (HomotopyGroup.Pi 3 (↑(Metric.sphere 0 1)) x ≃* Multiplicative ℤ)
  sorryAll goals completed! 🐙

pi_(n+1) of S^n is Z/2 for n at least 3

pi_succ_sphere_n_mulEquiv_zmod_two

Submitter: Kim Morrison.

Notes: A concrete stable-family homotopy-group computation.

Source: Classical theorem in unstable homotopy theory.

Informal solution: Use suspension and the stable range to show the first stable stem is Z/2.

theorem declaration uses `sorry`pi_succ_sphere_n_mulEquiv_zmod_two (n : ℕ) (hn : 3 ≤ n)
    (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) :
    Nonempty
      (HomotopyGroup.Pi (n + 1) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) x ≃*
        Multiplicative (ZMod 2)) := byn:ℕhn:3 ≤ nx:↑(Metric.sphere 0 1)⊢ Nonempty (HomotopyGroup.Pi (n + 1) (↑(Metric.sphere 0 1)) x ≃* Multiplicative (ZMod 2))
  sorryAll goals completed! 🐙

pi_n of the n-sphere is Z

pin_sphere_n_mulEquiv_int

Submitter: Kim Morrison.

Notes: The diagonal sphere homotopy-group computation pi_n(S^n) = Z for n at least 1.

Source: Classical theorem in algebraic topology.

Informal solution: Identify homotopy classes of self-maps of S^n with their degree.

theorem declaration uses `sorry`pin_sphere_n_mulEquiv_int (n : ℕ)
    (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 2))) 1) :
    Nonempty
      (HomotopyGroup.Pi (n + 1) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 2))) 1) x ≃*
        Multiplicative ℤ) := byn:ℕx:↑(Metric.sphere 0 1)⊢ Nonempty (HomotopyGroup.Pi (n + 1) (↑(Metric.sphere 0 1)) x ≃* Multiplicative ℤ)
  sorryAll goals completed! 🐙

Platonic classification

platonic_classification

Submitter: Kim Morrison.

Notes: §42 of Knill's 'Some Fundamental Theorems in Mathematics'. The count p_d of regular convex d-polytopes (Platonic polytopes) up to similarity is p_2 = ∞ (regular polygons), p_3 = 5 (Euclid XIII), p_4 = 6 (Schläfli 1850s), and p_d = 3 for d ≥ 5. Mathlib has convexHull, extremePoints, IsExposed, vectorSpan, AffineIsometryEquiv, Set.encard but no convex-polytope datatype, no face lattice, no regular-polytope concept, and none of the classification counts. The Challenge ships ~1.5 pages of helper defs (ConvexPolytope, dim, IsFace, Flag, isSymmetry, IsRegular, Similar, regularPolytopes, regularSimilar, platonicCount).

Source: Euclid, Elements, Book XIII (~300 BC, p_3 = 5); L. Schläfli, Theorie der vielfachen Kontinuität (1852, posthumous publication; p_4 = 6, p_d = 3 for d ≥ 5). Listed as §42 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: p_2 = ⊤: for each n ≥ 3 the regular n-gon (vertices = n-th roots of unity) is regular and any two non-congruent regular polygons are non-similar; the construction gives infinitely many similarity classes. p_3 = 5: any regular 3-polytope has Schläfli symbol {p, q} with p, q ≥ 3 and 1/p + 1/q > 1/2 (the spherical-angle-sum constraint at each vertex), giving exactly (3,3), (4,3), (3,4), (5,3), (3,5) — the five Platonic solids. p_4 = 6: any regular 4-polytope {p, q, r} satisfies the analogous spherical inequality, giving (3,3,3), (4,3,3), (3,3,4), (3,4,3), (5,3,3), (3,3,5) — Schläfli's six. p_d ≥ 5 = 3: in dim ≥ 5 the only solutions to the iterated angle constraint are the regular simplex {3, …, 3, 3}, hypercube {4, 3, …, 3}, and cross-polytope {3, …, 3, 4}. Existence of each candidate is by explicit construction (vertex coordinates); uniqueness within Schläfli class is by induction on dimension via vertex figures.

theorem declaration uses `sorry`platonic_classification :
    platonicCount 2 = ⊤ ∧
      platonicCount 3 = 5 ∧
        platonicCount 4 = 6 ∧
          ∀ d, 5 ≤ d → platonicCount d = 3 := by⊢ platonicCount 2 = ⊤ ∧ platonicCount 3 = 5 ∧ platonicCount 4 = 6 ∧ ∀ (d : ℕ), 5 ≤ d → platonicCount d = 3
  sorryAll goals completed! 🐙

3D smooth Poincaré conjecture (Perelman)

poincare_3d_smooth

Submitter: Kim Morrison.

Notes: Every simply connected compact Hausdorff smooth 3-manifold is diffeomorphic to 𝕊³. Recorded as `proof_wanted SimplyConnectedSpace.nonempty_diffeomorph_sphere_three` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. The smooth-category strengthening of the topological 3D Poincaré conjecture; also Perelman 2002-2003. In dim 3 the smooth and topological versions are equivalent (Moise's theorem says every topological 3-manifold admits a unique smooth structure), but the Lean statement carries the smooth structure explicitly. Mathlib has all the differential-topology / manifold scaffolding but neither Ricci flow nor Moise's theorem.

Source: G. Perelman, three arXiv preprints 2002-2003 (math/0211159, math/0303109, math/0307245). Recorded as a `proof_wanted` in Mathlib/Geometry/Manifold/PoincareConjecture.lean. In dim 3, Smooth ⇔ PL ⇔ Topological via Moise (1952) / Bing (1959).

Informal solution: Apply the topological 3D Poincaré conjecture to obtain a homeomorphism M ≃ₜ S³, then promote it to a diffeomorphism via Moise's theorem (every topological 3-manifold admits a unique smooth structure up to diffeomorphism), or equivalently observe that Hamilton-Perelman Ricci flow with surgery runs in the smooth category and produces a smooth diffeomorphism directly. Either route involves the same Perelman input on the geometric side; the dim-3 special feature is Moise/Bing which collapses the smooth/topological distinction (false in dim 4 and above).

theorem declaration uses `sorry`poincare_3d_smooth {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] [IsManifold (𝓡 3) ∞ M]
    [SimplyConnectedSpace M] [CompactSpace M] :
    Nonempty (M ≃ₘ⟮𝓡 3, 𝓡 3⟯ sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) := byM:Type u_1inst✝⁵:TopologicalSpace Minst✝⁴:T2Space Minst✝³:ChartedSpace (EuclideanSpace ℝ (Fin 3)) Minst✝²:IsManifold (𝓡 3) ∞ Minst✝¹:SimplyConnectedSpace Minst✝:CompactSpace M⊢ Nonempty (M ≃ₘ⟮𝓡 3, 𝓡 3⟯ ↑(sphere 0 1))
  sorryAll goals completed! 🐙

3D topological Poincaré conjecture (Perelman)

poincare_3d_topological

Submitter: Kim Morrison.

Notes: Every simply connected compact Hausdorff 3-manifold is homeomorphic to 𝕊³. Recorded as `proof_wanted SimplyConnectedSpace.nonempty_homeomorph_sphere_three` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Proved by Perelman in 2002-2003 via Hamilton's Ricci flow with surgery; one of the seven Millennium Problems. Mathlib has ChartedSpace, SimplyConnectedSpace, CompactSpace, T2Space, Homeomorph and the unit sphere as a smooth manifold but no Ricci flow, no Hamilton-Perelman surgery, and no Poincaré conjecture itself.

Source: G. Perelman, The entropy formula for the Ricci flow and its geometric applications (arXiv:math/0211159, 2002); Ricci flow with surgery on three-manifolds (arXiv:math/0303109, 2003); Finite extinction time for the solutions to the Ricci flow on certain three-manifolds (arXiv:math/0307245, 2003). Recorded as a `proof_wanted` in Mathlib/Geometry/Manifold/PoincareConjecture.lean. Originally conjectured by Henri Poincaré in 1904.

Informal solution: Run Ricci flow ∂g/∂t = -2 Ric(g) on M with surgery to remove finite-time singularities (Hamilton's program, completed by Perelman). The flow simplifies the metric, and Perelman's monotonicity formulas (reduced volume, ℒ-functional, no local collapsing) together with the canonical-neighbourhood theorem control the geometry. In finite time the flow either becomes extinct (M is a connected sum of spherical space forms and S²×S¹s, in particular when π_1(M) = 1, M = S³) or decomposes M along incompressible 2-tori into pieces of one of Thurston's eight geometric types; the simply-connected hypothesis rules out the toroidal decomposition and the spherical-space-form ambiguity, leaving M ≃ S³.

theorem declaration uses `sorry`poincare_3d_topological {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]
    [SimplyConnectedSpace M] [CompactSpace M] :
    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) := byM:Type u_1inst✝⁴:TopologicalSpace Minst✝³:T2Space Minst✝²:ChartedSpace (EuclideanSpace ℝ (Fin 3)) Minst✝¹:SimplyConnectedSpace Minst✝:CompactSpace M⊢ Nonempty (M ≃ₜ ↑(sphere 0 1))
  sorryAll goals completed! 🐙

4D topological Poincaré conjecture (Freedman)

poincare_4d_topological

Submitter: Kim Morrison.

Notes: Every Hausdorff 4-manifold homotopy-equivalent to 𝕊⁴ is homeomorphic to 𝕊⁴. Specialization to n = 4 of mathlib's generalized `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Michael Freedman's 1982 theorem (J. Differential Geom. 17), Fields Medal 1986. Proof uses Casson handles and the Bing-topology infinite-process construction. The corresponding smooth 4D Poincaré conjecture (every smooth homotopy 4-sphere is diffeomorphic to S⁴) remains famously OPEN and is not included here. Mathlib has the homotopy-equiv / homeo / ChartedSpace scaffolding but no Casson handles or Freedman's theorem.

Source: M. H. Freedman, The topology of four-dimensional manifolds, J. Differential Geom. 17 (1982), 357-453. Specialization of `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in Mathlib/Geometry/Manifold/PoincareConjecture.lean.

Informal solution: Freedman's main theorem: every topological 4-manifold homotopy equivalent to a topological model is homeomorphic to it, provided one can construct topological Casson handles. The construction of Casson handles is via a Bing-style limiting process (countably many handle additions, infinite tower of 2-handles) that produces a topological — but not smooth — 4-ball. Applying this to a homotopy 4-sphere M, one writes M as the union of two 2-handlebodies along their boundary, replaces handles with Casson handles, and assembles a homeomorphism to S⁴. The smooth analogue is open because Casson handles need not be smoothly standard (Donaldson's invariants distinguish smooth structures in dim 4).

theorem declaration uses `sorry`poincare_4d_topological {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M]
    (_h : M ≃ₕ sphere (0 : EuclideanSpace ℝ (Fin 5)) 1) :
    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 5)) 1) := byM:Type u_1inst✝²:TopologicalSpace Minst✝¹:T2Space Minst✝:ChartedSpace (EuclideanSpace ℝ (Fin 4)) M_h:M ≃ₕ ↑(sphere 0 1)⊢ Nonempty (M ≃ₜ ↑(sphere 0 1))
  sorryAll goals completed! 🐙

Poincaré–Bendixson theorem

poincare_bendixson

Submitter: Kim Morrison.

Notes: Planar trichotomy for the forward integral curve γ of a C¹ autonomous vector field F : ℝ² → ℝ². Either the forward orbit is unbounded; the ω-limit set ⋂ s, closure (γ '' Ici s) contains an equilibrium of F; or the ω-limit set equals the range of a non-constant periodic integral curve. The bounded branch uses 'ω-limit contains an equilibrium' rather than pointwise convergence (planar orbits may accumulate on continua of equilibria or polycycles). Case 3 requires F (β 0) ≠ 0 to exclude a constant equilibrium curve; the conclusion is a non-constant periodic orbit, not a limit cycle in the strict sense. §63 of Knill's 'Some Fundamental Theorems in Mathematics'.

Source: H. Poincaré, *Mémoire sur les courbes définies par une équation différentielle*, Journal de Mathématiques 7 (1881), 8 (1882), 1 (1885), 2 (1886); I. Bendixson, *Sur les courbes définies par des équations différentielles*, Acta Mathematica 24 (1901), 1-88. Listed as §63 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). The Isabelle/HOL/AFP entry by Fabian Immler and Yong Kiam Tan (https://www.isa-afp.org/entries/Poincare_Bendixson.html) uses John Harrison's Jordan curve theorem.

Informal solution: Classical proof: assume the forward orbit is bounded and the ω-limit set contains no equilibrium. Pick a regular point p of the ω-limit set and a transverse arc Σ at p. The first-return map P : Σ → Σ along the flow is well-defined and monotone in the natural linear order on Σ; the orbit's intersections with Σ form a monotone sequence converging to p. Combined with the Jordan curve theorem (a closed orbit Γ separates ℝ² into bounded interior and unbounded exterior, and trajectories cannot escape across Γ), this forces the ω-limit set to be exactly the range of a periodic integral curve through p. The non-degeneracy F (β 0) ≠ 0 follows from p being a regular point.

theorem declaration uses `sorry`poincare_bendixson (F : LeanEval.Dynamics.Plane → LeanEval.Dynamics.Plane) (_hF : ContDiff ℝ 1 F)
    (γ : ℝ → LeanEval.Dynamics.Plane)
    (_hγ : IsIntegralCurveOn γ (fun _ x => F x) (Set.Ici 0)) :
    ¬ Bornology.IsBounded (γ '' Set.Ici 0)
    ∨ (∃ x₀, F x₀ = 0 ∧ x₀ ∈ ⋂ s : ℝ, closure (γ '' Set.Ici s))
    ∨ (∃ T : ℝ, 0 < T ∧ ∃ β : ℝ → LeanEval.Dynamics.Plane,
        IsIntegralCurve β (fun _ x => F x) ∧
        (∀ t, β (t + T) = β t) ∧
        F (β 0) ≠ 0 ∧
        (⋂ s : ℝ, closure (γ '' Set.Ici s)) = Set.range β) := byF:Plane → Plane_hF:ContDiff ℝ 1 Fγ:ℝ → Plane_hγ:IsIntegralCurveOn γ (fun x x_1 => F x_1) (Ici 0)⊢ ¬Bornology.IsBounded (γ '' Ici 0) ∨
  (∃ x₀, F x₀ = 0 ∧ x₀ ∈ ⋂ s, closure (γ '' Ici s)) ∨
    ∃ T,
      0 < T ∧
        ∃ β,
          (IsIntegralCurve β fun x x_1 => F x_1) ∧
            (∀ (t : ℝ), β (t + T) = β t) ∧ F (β 0) ≠ 0 ∧ ⋂ s, closure (γ '' Ici s) = range β
  sorryAll goals completed! 🐙

Generalized topological Poincaré conjecture in dimensions ≥ 5 (Smale)

poincare_high_dim_topological

Submitter: Kim Morrison.

Notes: For n ≥ 5, every Hausdorff n-manifold homotopy-equivalent to 𝕊ⁿ is homeomorphic to 𝕊ⁿ. Specialization to n ≥ 5 of mathlib's generalized `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Stephen Smale 1961 (Bull. AMS 66, Ann. of Math. 74) originally for smooth M via the h-cobordism theorem; topological version completed by Newman 1966 and Connell 1967. Smale received the Fields Medal in 1966. Mathlib has the homotopy-equiv / homeo / ChartedSpace scaffolding but no h-cobordism theorem, no handle decompositions, and no Poincaré conjecture in any dimension.

Source: S. Smale, Generalized Poincaré's conjecture in dimensions greater than four, Ann. of Math. 74 (1961), 391-406. Topological case: M. H. A. Newman, The engulfing theorem for topological manifolds, Ann. of Math. 84 (1966) and E. H. Connell, A topological h-cobordism theorem for n ≥ 5, Illinois J. Math. 11 (1967). Specialization of `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in Mathlib/Geometry/Manifold/PoincareConjecture.lean.

Informal solution: Smale's smooth proof: a smooth homotopy n-sphere M (n ≥ 5) bounds a smooth contractible (n+1)-manifold W via Whitehead's theorem and a Mayer-Vietoris computation; apply the h-cobordism theorem (Smale's main contribution) to W minus two small balls to conclude W ≃ D^{n+1}, hence M = ∂W ≃ S^n smoothly. The topological version (Newman/Connell) replaces the h-cobordism step with the topological engulfing theorem and a topological h-cobordism theorem, proving the same conclusion without the smoothness hypothesis. The dim ≥ 5 hypothesis is crucial: it allows the Whitney trick to remove pairs of intersections, which fails in dim 4 (requiring Casson handles, Freedman 1982) and below.

theorem declaration uses `sorry`poincare_high_dim_topological {n : ℕ} (_h5 : 5 ≤ n)
    {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) M]
    (_h : M ≃ₕ sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) :
    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) := byn:ℕ_h5:5 ≤ nM:Type u_1inst✝²:TopologicalSpace Minst✝¹:T2Space Minst✝:ChartedSpace (EuclideanSpace ℝ (Fin n)) M_h:M ≃ₕ ↑(sphere 0 1)⊢ Nonempty (M ≃ₜ ↑(sphere 0 1))
  sorryAll goals completed! 🐙

Poincaré–Siegel linearisation theorem

poincare_siegel_linearisation

Submitter: Kim Morrison.

Notes: Siegel 1942: a holomorphic germ f near 0 with f 0 = 0 and multiplier λ = e^{2πiα} (α Diophantine) is locally analytically conjugate to z ↦ λz. The conjugating germ u satisfies u 0 = 0, u'(0) = 1, and f(u z) = u(λ z) near 0 (Schröder equation). The file ships an IsDiophantine predicate parameterised by an arbitrary exponent τ (∃ C, ∃ τ, ∀ p q ≠ 0, C / |q|^τ ≤ |α − p/q|); the constant-type / exponent-2 condition is the special case fixing τ = 2.

Source: C. L. Siegel, *Iteration of analytic functions*, Annals of Math. 43 (1942), 607-612. Earlier formal-power-series version: H. Poincaré thèse (1879). Listed as §83 (additional statement 1) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Construct the formal Schröder series u(z) = ∑ uₙ zⁿ from the conjugacy equation f(u z) = u(λ z), giving the recursion (λⁿ − λ) uₙ = (lower-order polynomial in u_{<n} and f_{≥2}). An arithmetic condition on the rotation number is essential to control the small divisors (λⁿ − 1); the Diophantine hypothesis gives a polynomial lower bound |λⁿ − 1| ≥ c n^{-(τ−1)} that is summable against Cauchy estimates. Siegel's geometric majorant-series argument bounds u by an explicit analytic envelope of positive radius of convergence.

theorem declaration uses `sorry`poincare_siegel (α : ℝ) (_hα : LeanEval.ComplexAnalysis.IsDiophantine α)
    (lam : ℂ) (_hlam : lam = Complex.exp (2 * Real.pi * Complex.I * (α : ℂ)))
    (f : ℂ → ℂ) (_hf : AnalyticAt ℂ f 0) (_hf0 : f 0 = 0)
    (_hmult : deriv f 0 = lam) :
    ∃ u : ℂ → ℂ, AnalyticAt ℂ u 0 ∧ u 0 = 0 ∧ deriv u 0 = 1 ∧
      ∀ᶠ z in nhds (0 : ℂ), f (u z) = u (lam * z) := byα:ℝ_hα:IsDiophantine αlam:ℂ_hlam:lam = Complex.exp (2 * ↑Real.pi * Complex.I * ↑α)f:ℂ → ℂ_hf:AnalyticAt ℂ f 0_hf0:f 0 = 0_hmult:deriv f 0 = lam⊢ ∃ u, AnalyticAt ℂ u 0 ∧ u 0 = 0 ∧ deriv u 0 = 1 ∧ ∀ᶠ (z : ℂ) in nhds 0, f (u z) = u (lam * z)
  sorryAll goals completed! 🐙

Entrywise exponential of a PSD matrix is PSD

posSemidef_map_exp

Submitter: Kim Morrison.

Notes: Part of the Schur-Polya-Loewner theory of entrywise functions preserving PSD. The proof uses the Schur product theorem iteratively: exp_⊙(A) = ∑ A^{⊙k}/k!, each Hadamard power is PSD, and the convergent series of PSD matrices is PSD.

Source: I.J. Schoenberg, Positive definite functions on spheres, 1942.

Informal solution: Write exp(a_{ij}) as the convergent series ∑ (a_{ij})^k / k!. The matrix with entries (a_{ij})^k is the k-fold Hadamard product A^{⊙k}, which is PSD by iterated Schur product. The partial sums are nonneg combinations of PSD matrices, hence PSD. PSD is a closed condition, so the limit is PSD.

theorem declaration uses `sorry`posSemidef_map_exp {n : Type*} [Fintype n] [DecidableEq n]
    {A : Matrix n n ℝ} (hA : A.PosSemidef) :
    (A.map Real.exp).PosSemidef := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef
  sorryAll goals completed! 🐙

Radó's theorem on Riemann surfaces

rado_riemannSurface

Submitter: Junyan Xu.

Notes: Unavailable.

Source: John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, §1.3.

Informal solution: Unavailable.

theorem declaration uses `sorry`rado_riemannSurface {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] :
    SecondCountableTopology X := byX:Type u_1inst✝⁴:TopologicalSpace Xinst✝³:T2Space Xinst✝²:ConnectedSpace Xinst✝¹:ChartedSpace ℂ Xinst✝:IsManifold (modelWithCornersSelf ℂ ℂ) 1 X⊢ SecondCountableTopology X
  sorryAll goals completed! 🐙

Lagarias criterion is equivalent to RH

riemann_hypothesis_iff_lagarias_elementary_criterion

Submitter: Kim Morrison.

Notes: Lagarias' elementary divisor-sum criterion stated using Mathlib's RiemannHypothesis, harmonic numbers, and sigma notation.

Source: https://arxiv.org/abs/math/0008177

Informal solution: Prove that the Riemann hypothesis is equivalent to the inequality σ(n) ≤ H_n + exp(H_n) log(H_n) for all positive integers n.

theorem declaration uses `sorry`riemann_hypothesis_iff_lagarias_elementary_criterion :
    RiemannHypothesis ↔ LeanEval.NumberTheory.LagariasElementaryCriterion := by⊢ RiemannHypothesis ↔ LagariasElementaryCriterion
  sorryAll goals completed! 🐙

Rokhlin lemma

rokhlin_lemma

Submitter: Kim Morrison.

Notes: §109 of Knill's 'Some Fundamental Theorems in Mathematics'. Every aperiodic measure-preserving automorphism of a standard Borel probability space admits, for every height n and every ε > 0, a measurable tower base B such that B, T B, …, T^{n-1} B are pairwise disjoint with total measure ≥ 1 - ε. The [StandardBorelSpace Ω] hypothesis is essential: the countable-cocountable σ-algebra on ℝ with the integer-shift map x ↦ x + 1 is aperiodic and measure-preserving but admits no nontrivial Rokhlin towers (every cocountable base intersects its own shift; every countable base has zero-measure tower). Mathlib has MeasurePreserving, IsProbabilityMeasure, Function.periodicPts, Set.PairwiseDisjoint, and StandardBorelSpace, but no Rokhlin lemma. The Challenge ships four small helper defs (IsAperiodic, towerFloor, towerUnion, IsRokhlinTower).

Source: V. A. Rokhlin, *A general measure-preserving transformation is not mixing*, Doklady Akademii Nauk SSSR 60 (1948), 349-351 (original Russian; English translation later); S. Kakutani, *Induced measure-preserving transformations*, Proc. Imp. Acad. Tokyo 19 (1943), 635-641 (independent discovery). Listed as §109 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover.

Informal solution: Standard proof: pick a measurable set A of small measure ε/n with positive density relative to T's orbit structure (the Halmos–Kakutani skyscraper). The first-return time r : A → ℕ is a.e. finite by aperiodicity; partition A by level sets {r = k}. Reassemble disjoint level-k floors T^j ({r = k}) for j < k into a height-n tower by horizontal cuts; the remaining 'roof' has measure at most ε.

theorem declaration uses `sorry`rokhlin_lemma {Ω : Type*} [MeasurableSpace Ω]
    [StandardBorelSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (T : Ω → Ω)
    (_hT : MeasurePreserving T μ μ) (_hap : LeanEval.Dynamics.IsAperiodic T μ)
    (n : ℕ) (_hn : 1 ≤ n) {ε : ENNReal} (_hε : 0 < ε) :
    ∃ B : Set Ω, LeanEval.Dynamics.IsRokhlinTower T B n ∧
      μ (LeanEval.Dynamics.towerUnion T B n) ≥ 1 - ε := byΩ:Type u_1inst✝²:MeasurableSpace Ωinst✝¹:StandardBorelSpace Ωμ:Measure Ωinst✝:IsProbabilityMeasure μT:Ω → Ω_hT:MeasurePreserving T μ μ_hap:IsAperiodic T μn:ℕ_hn:1 ≤ nε:ENNReal_hε:0 < ε⊢ ∃ B, IsRokhlinTower T B n ∧ μ (towerUnion T B n) ≥ 1 - ε
  sorryAll goals completed! 🐙

Rouche theorem via zero counting

rouche_zero_count_eq

Submitter: Kim Morrison.

Notes: Phrases Rouché's theorem as equality of multiplicity-counted zero counts for f and f + g on the closed disk of radius R.

Source: Classical theorem in complex analysis.

Informal solution: Assuming f is meromorphic in normal form on ℂ and |g| < |f| on the boundary circle, f and f + g have the same number of zeros inside the disk, counted with multiplicity.

theorem declaration uses `sorry`rouche_zero_count_eq {f g : ℂ → ℂ} {R : ℝ}
    (hR : 0 < R)
    (hf : MeromorphicNFOn f Set.univ)
    (hg : AnalyticOn ℂ g Set.univ)
    (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) :
    (∑ᶠ z, ((divisor (f + g) (Metric.closedBall 0 R))⁺) z) =
      (∑ᶠ z, ((divisor f (Metric.closedBall 0 R))⁺) z) := byf:ℂ → ℂg:ℂ → ℂR:ℝhR:0 < Rhf:MeromorphicNFOn f Set.univhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ ∑ᶠ (z : ℂ), (divisor (f + g) (Metric.closedBall 0 R))⁺ z = ∑ᶠ (z : ℂ), (divisor f (Metric.closedBall 0 R))⁺ z
  sorryAll goals completed! 🐙

Runge's theorem

runge_theorem

Submitter: Kim Morrison.

Notes: Basic Runge approximation theorem for compact subsets of ℂ. The statement uses polynomials p q : ℂ[X] and requires q to be nonvanishing on K, expressing rational functions with no poles on K. This does not include the standard pole-control refinement (one pole per connected component of ℂ \ K).

Source: C. Runge, *Zur Theorie der eindeutigen analytischen Funktionen*, Acta Math. 6 (1885), 229-244. Listed as §64 (additional statement 3) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Show that rational functions with poles outside K are dense in the algebra of functions holomorphic on a neighbourhood of K, with respect to the uniform norm on K. Classical proofs go via Cauchy integral approximation or via Hahn–Banach / Riesz duality.

theorem declaration uses `sorry`runge (K : Set ℂ) (_hK : IsCompact K) (U : Set ℂ) (_hU : IsOpen U)
    (_hKU : K ⊆ U) (f : ℂ → ℂ) (_hf : AnalyticOnNhd ℂ f U)
    (ε : ℝ) (_hε : 0 < ε) :
    ∃ p q : ℂ[X], (∀ z ∈ K, q.eval z ≠ 0) ∧
      (∀ z ∈ K, ‖f z - p.eval z / q.eval z‖ < ε) := byK:Set ℂ_hK:IsCompact KU:Set ℂ_hU:IsOpen U_hKU:K ⊆ Uf:ℂ → ℂ_hf:AnalyticOnNhd ℂ f Uε:ℝ_hε:0 < ε⊢ ∃ p q, (∀ z ∈ K, Polynomial.eval z q ≠ 0) ∧ ∀ z ∈ K, ‖f z - Polynomial.eval z p / Polynomial.eval z q‖ < ε
  sorryAll goals completed! 🐙

Schauder fixed-point theorem

schauder_fixed_point

Submitter: Kim Morrison.

Notes: §60 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement). The Banach-space generalization of Brouwer: every continuous self-map of a nonempty compact convex subset of a real Banach space has a fixed point. Mathlib has NormedAddCommGroup / NormedSpace / CompleteSpace and the Banach contraction principle (ContractingWith.exists_fixedPoint, strictly weaker), but no Schauder fixed-point theorem. SchauderBasis / GeneralSchauderBasis in mathlib are unrelated (about sequences spanning a Banach space, not fixed points). No open mathlib PR; the Sperner → Brouwer → Schauder dependency chain is partially in motion (Sperner partially landed, Brouwer in flight in #36770). Active downstream demand from the PDE community for Schauder / Schaefer / Leray–Schauder machinery (cf. Nelson Spence's 2026-03-06 Zulip thread). Stateable with zero new definitions.

Source: J. Schauder, *Der Fixpunktsatz in Funktionalräumen*, Studia Mathematica 2 (1930), 171-180. Listed as §60 (additional statement 2) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in mathlib4 or any open mathlib PR; Brouwer is in flight via https://github.com/leanprover-community/mathlib4/pull/36770.

Informal solution: Standard proof: approximate the compact convex K by finite-dimensional convex polytopes K_n via ε-nets and the convex-hull construction; on each K_n apply Brouwer fixed-point to a continuous projection of f to get a fixed point x_n ∈ K_n; pass to a subsequence x_n → x (compactness of K), and verify f x = x using uniform continuity of f on the compact set K. The full argument depends on Brouwer's fixed-point theorem (the main classical input) and Mazur's theorem (the closed convex hull of a compact subset of a Banach space is compact, which uses completeness).

theorem declaration uses `sorry`schauder_fixed_point {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {K : Set E}
    (_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
    (_hK_nonempty : K.Nonempty)
    (f : E → E)
    (_hf_cont : ContinuousOn f K) (_hf_maps : Set.MapsTo f K K) :
    ∃ x ∈ K, f x = x := byE:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EK:Set E_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.Nonemptyf:E → E_hf_cont:ContinuousOn f K_hf_maps:Set.MapsTo f K K⊢ ∃ x ∈ K, f x = x
  sorryAll goals completed! 🐙

Schläfli classification of regular polytopes

schlafli_classification

Submitter: Kim Morrison.

Notes: §42 of Knill's 'Some Fundamental Theorems in Mathematics'. Schläfli's dimension-by-dimension enumeration of the regular convex polytopes: p_3 = 5 (Euclid XIII — the five Platonic solids), p_4 = 6 (Schläfli's six regular 4-polytopes), and p_d = 3 for every d ≥ 5 (regular simplex, hypercube, cross-polytope). Companion to the broader Platonic classification problem, which additionally records p_2 = ∞. Mathlib has convexHull, extremePoints, IsExposed, vectorSpan, AffineIsometryEquiv, Set.encard but no convex-polytope datatype, no face lattice, no regular-polytope concept, and none of the classification counts. The Challenge ships ~1.5 pages of helper defs (ConvexPolytope, dim, IsFace, Flag, isSymmetry, IsRegular, Similar, regularPolytopes, regularSimilar, platonicCount).

Source: L. Schläfli, *Theorie der vielfachen Kontinuität* (1852, posthumously published 1901; first proof that p_3 = 5, p_4 = 6, and p_d = 3 for d ≥ 5). Listed as §42 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: p_3 = 5: any regular 3-polytope has Schläfli symbol {p, q} with p, q ≥ 3 and 1/p + 1/q > 1/2 (the spherical-angle-sum constraint at each vertex), giving exactly (3,3), (4,3), (3,4), (5,3), (3,5) — the five Platonic solids. p_4 = 6: any regular 4-polytope {p, q, r} satisfies the analogous spherical inequality, giving (3,3,3), (4,3,3), (3,3,4), (3,4,3), (5,3,3), (3,3,5) — Schläfli's six. p_d ≥ 5 = 3: in dim ≥ 5 the only solutions to the iterated angle constraint are the regular simplex {3, …, 3, 3}, hypercube {4, 3, …, 3}, and cross-polytope {3, …, 3, 4}. Existence of each candidate is by explicit construction (vertex coordinates); uniqueness within Schläfli class is by induction on dimension via vertex figures.

theorem declaration uses `sorry`schlafli_classification :
    platonicCount 3 = 5 ∧
      platonicCount 4 = 6 ∧
        ∀ d, 5 ≤ d → platonicCount d = 3 := by⊢ platonicCount 3 = 5 ∧ platonicCount 4 = 6 ∧ ∀ (d : ℕ), 5 ≤ d → platonicCount d = 3
  sorryAll goals completed! 🐙

Schoenflies theorem

schoenflies

Submitter: Kim Morrison.

Notes: §48 of Knill's 'Some Fundamental Theorems in Mathematics'. Strong form: every Jordan curve in the plane is the image of the unit circle under some self-homeomorphism of ℝ². This is the faithful encoding of Knill's prose statement 'each complementary region is homeomorphic to the open disk' — which as literally written is false for the unbounded region (homeomorphic to ℝ² ∖ closedBall 0 1, fundamental group ℤ, not simply connected). The strong form implies the bounded region is homeomorphic to the open disk. Mathlib has Metric.sphere, EuclideanSpace, and Homeomorph, but no Schoenflies theorem (`grep -ri 'schoenflies' Mathlib/`: no hits), no Jordan curve theorem, no invariance-of-domain machinery in a form that would discharge it. Stateable with zero new definitions.

Source: A. M. Schoenflies, *Beiträge zur Theorie der Punktmengen III*, Math. Annalen 62 (1906) (first proof, with gaps); rigorous proofs by L. Antoine (1921), L. E. J. Brouwer (1909–10). Listed as §48 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover.

Informal solution: Classical proof: (i) the Jordan curve theorem gives the inside and outside regions; (ii) Riemann mapping for the bounded inside extends to a homeomorphism of the closed disk by Carathéodory's theorem on prime ends; (iii) a parallel construction handles the outside; (iv) the two homeomorphisms patch along the curve to a homeomorphism of ℝ².

theorem declaration uses `sorry`schoenflies (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 → EuclideanSpace ℝ (Fin 2))
    (_hcont : Continuous r) (_hinj : Function.Injective r) :
    ∃ h : EuclideanSpace ℝ (Fin 2) ≃ₜ EuclideanSpace ℝ (Fin 2),
      h '' Set.range r = Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := byr:↑(Metric.sphere 0 1) → EuclideanSpace ℝ (Fin 2)_hcont:Continuous r_hinj:Function.Injective r⊢ ∃ h, ⇑h '' Set.range r = Metric.sphere 0 1
  sorryAll goals completed! 🐙

Schreier's conjecture: outer automorphism group of a finite simple group is solvable

schreier_conjecture

Submitter: Kim Morrison.

Notes: For every finite non-abelian simple group S, Out(S) := Aut(S)/Inn(S) is solvable. The statement requires the normality of Inn(S) ⊴ Aut(S), which is supplied by a local instance with a one-line proof (the conjugate of conj(s) by α equals conj(α(s))). Verified case-by-case via CFSG; no CFSG-free proof is known.

Source: O. Schreier, Über die Erweiterung von Gruppen II, Abh. Math. Sem. Univ. Hamburg 4 (1926); CFSG, completed c. 2004.

Informal solution: Use the classification of finite simple groups. For each family — alternating Aₙ, classical Lie type, exceptional Lie type, sporadic — inspect the known Out(S) and verify it is solvable. For Aₙ (n ≥ 5, n ≠ 6), Out = ℤ/2; for A₆, Out = (ℤ/2)²; for groups of Lie type, Out is built from diagonal, field, and graph automorphisms (each step solvable); for sporadics, Out is trivial or ℤ/2.

theorem declaration uses `sorry`schreier_conjecture (S : Type) [Group S] [Fintype S] [IsSimpleGroup S]
    (hS : ∃ a b : S, ¬ Commute a b) :
    IsSolvable (MulAut S ⧸ (MulAut.conj : S →* MulAut S).range) := byS:Typeinst✝²:Group Sinst✝¹:Fintype Sinst✝:IsSimpleGroup ShS:∃ a b, ¬Commute a b⊢ IsSolvable (MulAut S ⧸ MulAut.conj.range)
  sorryAll goals completed! 🐙

Smale conjecture (Hatcher) in relative parameterized form

smale_conjecture

Submitter: Kim Morrison.

Notes: Hatcher's 1983 theorem that Diff(S3) is homotopy equivalent to O(4), stated in the relative-parameterized-family form (families on a compact manifold-with-boundary X whose boundary already factors through O(4) deform rel boundary to a family fully factoring through O(4)). Mathlib does not yet carry the C-infinity topology on Diffeomorph, which would be needed for the direct homotopy-equivalence formulation.

Source: A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983).

Informal solution: Hatcher proves Diff(S3) is homotopy equivalent to O(4) by analyzing configurations of 2-spheres in S3 (the bigon criterion) and deducing by induction that every self-diffeomorphism is isotopic to a linear one, with all higher parameterized versions handled by the same incompressible-surface machinery.

theorem declaration uses `sorry`smale_conjecture {n : ℕ} [NeZero n]
    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
    [CompactSpace X]
    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
    (hψ_bdry_cont : Continuous ψ_bdry)
    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
                  (p : EuclideanSpace ℝ (Fin 4))) :
    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
      Continuous ψ ∧
      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
      (∀ x p, H (x, 0, p) = F (x, p)) ∧
      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
                (p : EuclideanSpace ℝ (Fin 4))) ∧
      (∀ (b : (𝓡∂ n).boundary X)
         (t : unitInterval)
         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
              H ((b : X), t, p) = F ((b : X), p)) := byn:ℕinst✝⁶:NeZero nX:Typeinst✝⁵:TopologicalSpace Xinst✝⁴:T2Space Xinst✝³:SecondCountableTopology Xinst✝²:ChartedSpace (EuclideanHalfSpace n) Xinst✝¹:IsManifold (𝓡∂ n) ∞ Xinst✝:CompactSpace XF:X × ↑(sphere 0 1) → ↑(sphere 0 1)F':X × ↑(sphere 0 1) → ↑(sphere 0 1)hF:ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ FhF':ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F'hFinv₁:∀ (x : X) (p : ↑(sphere 0 1)), F (x, F' (x, p)) = phFinv₂:∀ (x : X) (p : ↑(sphere 0 1)), F' (x, F (x, p)) = pψ_bdry:↑(ModelWithCorners.boundary X) → ↥(Matrix.orthogonalGroup (Fin 4) ℝ)hψ_bdry_cont:Continuous ψ_bdryhF_bdry:∀ (b : ↑(ModelWithCorners.boundary X)) (p : ↑(sphere 0 1)),
  (↑(F (↑b, p))).ofLp = (Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)) (↑p).ofLp⊢ ∃ ψ H H',
  Continuous ψ ∧
    (∀ (b : ↑(ModelWithCorners.boundary X)), ψ ↑b = ψ_bdry b) ∧
      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
        ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
          (∀ (x : X) (t : ↑unitInterval) (p : ↑(sphere 0 1)), H (x, t, H' (x, t, p)) = p) ∧
            (∀ (x : X) (t : ↑unitInterval) (p : ↑(sphere 0 1)), H' (x, t, H (x, t, p)) = p) ∧
              (∀ (x : X) (p : ↑(sphere 0 1)), H (x, 0, p) = F (x, p)) ∧
                (∀ (x : X) (p : ↑(sphere 0 1)),
                    (↑(H (x, 1, p))).ofLp = (Matrix.UnitaryGroup.toLinearEquiv (ψ x)) (↑p).ofLp) ∧
                  ∀ (b : ↑(ModelWithCorners.boundary X)) (t : ↑unitInterval) (p : ↑(sphere 0 1)),
                    H (↑b, t, p) = F (↑b, p)
  sorryAll goals completed! 🐙

Solvable extensions ↔ solvable groups (the missing converse in Abel–Ruffini)

solvable_by_radicals_converse

Submitter: Kim Morrison.

Notes: §58 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement). For F : Field of characteristic zero and a nonzero p : F[X], every root of p in AlgebraicClosure F lies in solvableByRad F (AlgebraicClosure F) iff p.Gal is solvable. Mathlib has the → direction via isSolvable_gal_of_irreducible / isSolvable_gal_minpoly in Mathlib/FieldTheory/AbelRuffini.lean (the file header states it proves 'one direction' of Abel–Ruffini). The ← direction is the Kummer-theory content and is the missing piece. The polynomial-level iff is stronger than the irreducible/minpoly form already in mathlib.

Source: É. Galois (1832); the iff appears in standard texts such as Stewart, *Galois Theory* (Theorem 18.10); Lang, *Algebra* (VI §7); Rotman, *Galois Theory* (Theorem 73). Listed as §58 (additional statement 2) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Classical proof of the ← direction: assume p.Gal is solvable. Adjoin to F a sufficient root of unity (a primitive n-th root for n = |p.Gal|) to obtain F' = F(ζ); the Galois group of the splitting field L of p over F' is a subgroup of Gal(p over F) hence still solvable, and F'/F is a radical extension. Take a composition series G = G₀ ▹ G₁ ▹ ⋯ ▹ Gₖ = 1 of Gal(L/F') with each factor cyclic of prime order. The corresponding tower of fixed fields is F' = L^{G₀} ⊂ L^{G₁} ⊂ ⋯ ⊂ L^{Gₖ} = L, with each step Galois cyclic of prime order over a field containing the relevant root of unity; by Kummer theory each step is a pure radical extension. The splitting field of p sits inside L, so every root of p lies in solvableByRad F (AlgebraicClosure F). The → direction follows from the existing mathlib lemma isSolvable_gal_of_irreducible applied to each irreducible factor.

theorem declaration uses `sorry`solvable_iff_solvableByRad (F : Type*) [Field F] [CharZero F]
    (p : F[X]) (_hp : p ≠ 0) :
    (∀ x : AlgebraicClosure F, aeval x p = 0 →
        x ∈ solvableByRad F (AlgebraicClosure F)) ↔ IsSolvable p.Gal := byF:Type u_1inst✝¹:Field Finst✝:CharZero Fp:F[X]_hp:p ≠ 0⊢ (∀ (x : AlgebraicClosure F), (aeval x) p = 0 → x ∈ solvableByRad F (AlgebraicClosure F)) ↔ IsSolvable p.Gal
  sorryAll goals completed! 🐙

Sturm's theorem

sturm

Submitter: Kim Morrison.

Notes: §97 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The number of distinct real roots of a squarefree real polynomial in an open interval equals the drop in the number of sign variations of its Sturm chain across the interval. The Sturm chain, the sign-variation counter, and the variation function σ are defined in the problem; mathlib has none of them. The chain uses the negated-remainder convention p_{k+1} = -(p_{k-1} mod p_k), for which the count is σ(a) - σ(b). Sturm's theorem is formalized in Isabelle/HOL (Manuel Eberl, AFP entry Sturm_Sequences) in the same distinct-root form.

Source: J. C. F. Sturm (1829). Listed as §97 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Formalized in Isabelle/HOL by Manuel Eberl (AFP entry Sturm_Sequences).

Informal solution: As x increases across a simple root of p exactly one sign variation of the Sturm chain is lost and none is gained — the standard sign analysis of consecutive chain entries at a root, using squarefreeness so that p and p' have no common root — while across a root of an interior chain entry the variation count is unchanged. Between roots σ is locally constant. Hence the number of distinct roots of p in (a, b) equals σ(a) - σ(b).

theorem declaration uses `sorry`sturm (p : ℝ[X]) (hp : Squarefree p) {a b : ℝ} (hab : a < b)
    (ha : p.eval a ≠ 0) (hb : p.eval b ≠ 0) :
    ((p.roots.toFinset).filter (fun x => a < x ∧ x < b)).card =
      sigma p a - sigma p b := byp:ℝ[X]hp:Squarefree pa:ℝb:ℝhab:a < bha:eval a p ≠ 0hb:eval b p ≠ 0⊢ {x ∈ p.roots.toFinset | a < x ∧ x < b}.card = sigma p a - sigma p b
  sorryAll goals completed! 🐙

Sturm separation theorem

sturm_separation

Submitter: Kim Morrison.

Notes: Between consecutive zeros of one solution of a second-order linear homogeneous ODE, any linearly independent solution has exactly one zero.

Source: C. Sturm, Mémoire sur les équations différentielles linéaires du second ordre, 1836.

Informal solution: On (a, b), y_1 has constant sign and never vanishes. The Wronskian W = y_1 y_2' - y_2 y_1' satisfies W' = -p W (Liouville), so W has constant sign on J. Hence (y_2 / y_1)' = -W / y_1^2 has constant sign and y_2 / y_1 is strictly monotone on (a, b). The Wronskian also forces y_2(a), y_2(b) ≠ 0 (else W(a) or W(b) would vanish, contradicting nonvanishing of W). If y_2 had no zero in (a, b), continuity gives sign(y_2(a)) = sign(y_2(b)); then y_2 / y_1 tends to the same infinite sign at both endpoints, contradicting strict monotonicity. Thus y_2 has a zero in (a, b). Uniqueness follows because a strictly monotone function can cross 0 at most once.

theorem declaration uses `sorry`sturm_separation (p q y₁ y₂ : ℝ → ℝ) (a b : ℝ) (hab : a < b)
    (J : Set ℝ) (hJ_open : IsOpen J) (hJ_conn : IsPreconnected J)
    (hJ_sub : Set.Icc a b ⊆ J)
    (hp : ContinuousOn p J) (hq : ContinuousOn q J)
    (hy₁ : ∀ x ∈ J, HasDerivAt y₁ (deriv y₁ x) x)
    (hy₁' : ∀ x ∈ J, HasDerivAt (deriv y₁) (-(p x * deriv y₁ x + q x * y₁ x)) x)
    (hy₂ : ∀ x ∈ J, HasDerivAt y₂ (deriv y₂ x) x)
    (hy₂' : ∀ x ∈ J, HasDerivAt (deriv y₂) (-(p x * deriv y₂ x + q x * y₂ x)) x)
    (hW : ∃ x₀ ∈ J, y₁ x₀ * deriv y₂ x₀ - y₂ x₀ * deriv y₁ x₀ ≠ 0)
    (hza : y₁ a = 0) (hzb : y₁ b = 0)
    (hne : ∀ x ∈ Set.Ioo a b, y₁ x ≠ 0) :
    ∃! c, c ∈ Set.Ioo a b ∧ y₂ c = 0 := byp:ℝ → ℝq:ℝ → ℝy₁:ℝ → ℝy₂:ℝ → ℝa:ℝb:ℝhab:a < bJ:Set ℝhJ_open:IsOpen JhJ_conn:IsPreconnected JhJ_sub:Set.Icc a b ⊆ Jhp:ContinuousOn p Jhq:ContinuousOn q Jhy₁:∀ x ∈ J, HasDerivAt y₁ (deriv y₁ x) xhy₁':∀ x ∈ J, HasDerivAt (deriv y₁) (-(p x * deriv y₁ x + q x * y₁ x)) xhy₂:∀ x ∈ J, HasDerivAt y₂ (deriv y₂ x) xhy₂':∀ x ∈ J, HasDerivAt (deriv y₂) (-(p x * deriv y₂ x + q x * y₂ x)) xhW:∃ x₀ ∈ J, y₁ x₀ * deriv y₂ x₀ - y₂ x₀ * deriv y₁ x₀ ≠ 0hza:y₁ a = 0hzb:y₁ b = 0hne:∀ x ∈ Set.Ioo a b, y₁ x ≠ 0⊢ ∃! c, c ∈ Set.Ioo a b ∧ y₂ c = 0
  sorryAll goals completed! 🐙

Catalan generating function via compositional inversion

substInv_X_sub_X_sq_eq_catalan

Submitter: Kim Morrison.

Notes: The compositional inverse of X - X² is the generating function for Catalan numbers. This is a classical application of Lagrange inversion in enumerative combinatorics, connecting formal power series inversion to Dyck paths, binary trees, and triangulations.

Source: E. Catalan, Note sur une équation aux différences finies, 1838; J.-L. Lagrange, Nouvelle méthode pour résoudre les équations littérales, 1770.

Informal solution: The compositional inverse C(x) satisfies C - C² = x, giving C = (1 - √(1-4x))/2. By the binomial series, its coefficients are the Catalan numbers C_n = (2n choose n)/(n+1).

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) :
    haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := byn:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2))
      simp [coeff_X, coeff_X_pow]n:ℕ⊢ Invertible 1; exact invertibleOneAll goals completed! 🐙
    coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) =
      (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := byn:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1)
  sorryAll goals completed! 🐙

Schur-Weyl duality: S_k image equals centralizer of GL(V) image

symAction_range_eq_centralizer_glAction

Submitter: Kim Morrison.

Notes: One direction of Schur-Weyl duality: the subalgebra of End(V^⊗k) generated by the S_k action (permuting factors) equals the centralizer of the subalgebra generated by the diagonal GL(V) action. Hypothesis `Invertible (k! : R)` over a field is exactly the Maschke condition for R[S_k].

Source: H. Weyl, The Classical Groups, 1939; I. Schur, Über die rationalen Darstellungen der allgemeinen linearen Gruppe, 1927.

Informal solution: Classical proof: any T ∈ End(V^⊗k) commuting with GL(V) acts the same way on tensors related by g^⊗k for every g, and by polarization (which uses k! invertible) the subalgebra {g^⊗k : g ∈ GL(V)} linearly spans the image of Sym^k(End V) in End(V^⊗k). Together with the semisimplicity of R[S_k] (Maschke, from the same k! hypothesis) and double commutant for finite-dimensional semisimple algebras, T lies in the R-subalgebra generated by the S_k action.

theorem declaration uses `sorry`symAction_range_eq_centralizer_glAction {R : Type*} [Field R]
    {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M]
    {k : ℕ} [Invertible (k.factorial : R)] :
    Algebra.adjoin R (Set.range (LeanEval.RepresentationTheory.symAction R M k)) =
      Subalgebra.centralizer R (Set.range (LeanEval.RepresentationTheory.glAction R M k)) := byR:Type u_1inst✝⁴:Field RM:Type u_2inst✝³:AddCommGroup Minst✝²:Module R Minst✝¹:FiniteDimensional R Mk:ℕinst✝:Invertible ↑k.factorial⊢ Algebra.adjoin R (Set.range ⇑(symAction R M k)) = Subalgebra.centralizer R (Set.range ⇑(glAction R M k))
  sorryAll goals completed! 🐙

Symplectic matrices have determinant 1

symplectic_matrix_det

Submitter: Kim Morrison.

Notes: §39 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. For any commutative ring R and 2n × 2n symplectic matrix A over R (A * J * Aᵀ = J with J = [[0, -I], [I, 0]]), det A = 1. Taking determinants of AᵀJA = J only forces (det A)² = 1; the sign requires the Pfaffian argument. Mathlib has `Matrix.symplecticGroup` and proves `symplectic_det` (IsUnit (det A)) but the equals-1 claim is an explicit TODO in Mathlib/LinearAlgebra/SymplecticGroup.lean; no formalization of the identity was found in any other proof assistant.

Source: Folklore (Pfaffian computation). Listed as §39 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Marked as an open TODO at the head of Mathlib/LinearAlgebra/SymplecticGroup.lean (rev 5450b53e5ddc).

Informal solution: Apply the Pfaffian: for any 2n × 2n matrix M and antisymmetric 2n × 2n matrix Ω, Pf(Mᵀ Ω M) = det(M) · Pf(Ω). With Ω = J (so Pf(J) ≠ 0) and Aᵀ J A = J for A ∈ Sp_{2n}(R), one gets Pf(J) = det(A) · Pf(J), hence det A = 1. (This requires the Pfaffian for matrices over a commutative ring R; the construction is purely algebraic.)

theorem declaration uses `sorry`symplectic_matrix_det {l R : Type*} [DecidableEq l] [Fintype l] [CommRing R]
    {A : Matrix (l ⊕ l) (l ⊕ l) R} (_hA : A ∈ Matrix.symplecticGroup l R) :
    A.det = 1 := byl:Type u_1R:Type u_2inst✝²:DecidableEq linst✝¹:Fintype linst✝:CommRing RA:Matrix (l ⊕ l) (l ⊕ l) R_hA:A ∈ symplecticGroup l R⊢ A.det = 1
  sorryAll goals completed! 🐙

Szemerédi's theorem

szemeredi

Submitter: Kim Morrison.

Notes: §37 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (first additional statement of the section, generalizing Roth's theorem from 3-APs to k-APs). Every subset of ℕ of positive upper density contains arbitrarily long arithmetic progressions. Mathlib has Roth's theorem (roth_3ap_theorem_nat, the k = 3 case) but not the full Szemerédi theorem. As of 2026 it has not been formalized in any major proof assistant (a well-known open formalization target).

Source: E. Szemerédi, On sets of integers containing no k elements in arithmetic progression, Acta Arith. 27 (1975), 199-245. Listed as §37 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Szemerédi's original combinatorial proof relies on the Szemerédi regularity lemma plus a delicate density-increment argument. Furstenberg gave a measure-theoretic proof via multiple recurrence in ergodic theory (every measure-preserving system has the Multiple Recurrence Property for k commuting transformations). Gowers gave a Fourier-analytic proof introducing the Gowers uniformity norms U^k. Any of these formalisations is a major undertaking; all three structures (regularity, ergodic multiple recurrence, U^k norms) are absent from mathlib.

theorem declaration uses `sorry`szemeredi (A : Set ℕ) (h : 0 < upperDensity A) :
    LeanEval.Combinatorics.ContainsArbitraryAPs A := byA:Set ℕh:0 < upperDensity A⊢ ContainsArbitraryAPs A
  sorryAll goals completed! 🐙

Topological classification of surfaces

topological_classification_of_surfaces

Submitter: Junyan Xu.

Notes: A compact connected surface with boundary is homeomorphic to one of the representative surfaces that we formalize.

Source: Jean Gallier & Dianna Xu, *A Guide to the Classification Theorem for Compact Surfaces*, https://www.cis.upenn.edu/~jean/surfclassif-root.pdf

Informal solution: Show surfaces are triangulable and therefore homeomorphic to cell complexes, and show each cell complex is equivalent to one in normal form.

theorem declaration uses `sorry`classification_of_surfaces (S : Type*) [TopologicalSpace S]
    [T2Space S] [ConnectedSpace S] [CompactSpace S]
    [ChartedSpace (EuclideanHalfSpace 2) S]
    [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] :
    Nonempty (S ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) ∨
    ∃ p n, ((1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (LeanEval.Topology.ClassificationOfSurfaces.OrientableRel p n))) ∨
      (1 ≤ p ∧ Nonempty (S ≃ₜ Quot (LeanEval.Topology.ClassificationOfSurfaces.NonOrientableRel p n))) := byS:Type u_1inst✝⁵:TopologicalSpace Sinst✝⁴:T2Space Sinst✝³:ConnectedSpace Sinst✝²:CompactSpace Sinst✝¹:ChartedSpace (EuclideanHalfSpace 2) Sinst✝:IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S⊢ Nonempty (S ≃ₜ ↑(Metric.sphere 0 1)) ∨
  ∃ p n,
    (1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (OrientableRel p n)) ∨ 1 ≤ p ∧ Nonempty (S ≃ₜ Quot (NonOrientableRel p n))
  sorryAll goals completed! 🐙

Uniformization theorem for Riemann surfaces

uniformization

Submitter: Junyan Xu.

Notes: Unavailable.

Source: John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1.

Informal solution: Unavailable.

theorem declaration uses `sorry`uniformization {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
    [SecondCountableTopology X] [ChartedSpace ℂ X] [IsManifold mℂ 1 X]
    (hX : ¬ CompactSpace X) (x : X) [Subsingleton <| Additive (FundamentalGroup X x) →+ ℝ] :
    Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ ℂ) ∨ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ UpperHalfPlane) := byX:Type u_1inst✝⁶:TopologicalSpace Xinst✝⁵:T2Space Xinst✝⁴:ConnectedSpace Xinst✝³:SecondCountableTopology Xinst✝²:ChartedSpace ℂ Xinst✝¹:IsManifold mℂ 1 XhX:¬CompactSpace Xx:Xinst✝:Subsingleton (Additive (FundamentalGroup X x) →+ ℝ)⊢ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ ℂ) ∨ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ UpperHalfPlane)
  sorryAll goals completed! 🐙

Spencer-Szemerédi-Trotter unit-distance upper bound

unit_distance_upper_bound

Submitter: Kim Morrison.

Notes: For a finite set P ⊆ ℝ² write ν(P) for the number of unordered pairs at Euclidean distance 1, and ν(n) = max over n-point sets. Erdős posed the unit-distance problem in 1946 alongside the dual distinct-distances problem (resolved up to log factors by Guth-Katz, 2015). The first nontrivial upper bound ν(n) = O(n^{3/2}) follows from the Kővári-Sós-Turán theorem applied to the K_{2,3}-free unit-distance graph. Spencer-Szemerédi-Trotter (1984) sharpened this to ν(n) = O(n^{4/3}) using the Szemerédi-Trotter incidence bound for points and lines; Székely later gave a short crossing-number proof of the same exponent. The exponent 4/3 has stood since 1984 with only constant-factor improvements (Ágoston-Pálvölgyi, 2022). The matching lower bound is widely conjectured to lie much closer to the upper bound — see the companion problem `erdos_unit_distance_conjecture_false`.

Source: J. Spencer, E. Szemerédi, W. T. Trotter Jr., *Unit distances in the Euclidean plane*, in Graph Theory and Combinatorics (Cambridge 1983), Academic Press, 1984. Short crossing-number proof: L. A. Székely, *Crossing numbers and hard Erdős problems in discrete geometry*, Combin. Probab. Comput. 6 (1997). Best constant: P. Ágoston, D. Pálvölgyi, *An improved constant factor for the unit distance problem*, Studia Sci. Math. Hungar. 59 (2022).

Informal solution: Build the bipartite incidence structure of P with the family of unit circles centred at points of P: each unit-distance pair (x, y) corresponds to the incidence (y, C_x), where C_x is the unit circle centred at x. Two unit circles intersect in at most two points, so the incidence graph is K_{2,3}-free. Apply the Szemerédi-Trotter theorem (any n points and n curves with bounded pairwise intersection number have O(n^{4/3}) incidences) — or equivalently, Székely's crossing-number argument: draw the unit-distance graph with circular arcs, count crossings two ways, and conclude via the crossing-number inequality. Either route gives ν(n) ≤ C · n^{4/3}.

theorem declaration uses `sorry`unit_distance_upper_bound :
    ∃ C : ℝ, 0 < C ∧
      ∀ P : Finset (EuclideanSpace ℝ (Fin 2)),
        (unitDist P : ℝ) ≤ C * (P.card : ℝ) ^ ((4 : ℝ) / 3) := by⊢ ∃ C, 0 < C ∧ ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))), ↑(unitDist P) ≤ C * ↑P.card ^ (4 / 3)
  sorryAll goals completed! 🐙

von Neumann double commutant theorem

vonNeumann_doubleCommutant_tfae

Submitter: Kim Morrison.

Notes: The classical double commutant theorem: for a unital *-subalgebra of bounded operators on a complex Hilbert space, equality with the double commutant is equivalent to closedness in the weak operator topology and to closedness in the strong operator topology. WOT and SOT live on Mathlib's irreducible type copies of H →L[ℂ] H (`ContinuousLinearMapWOT` and `PointwiseConvergenceCLM`), so each closure condition is phrased on the image of the carrier under the canonical inclusion.

Source: J. von Neumann, Zur Algebra der Funktionaloperationen und Theorie der normalen Operatoren, Math. Ann. 102 (1930), 370-427.

Informal solution: One direction: centralizers are WOT-closed, so any set equal to its double commutant is WOT-closed; norm topology refines WOT refines SOT for continuity of evaluation, and closedness under a finer convex topology is implied by closedness under a coarser one (via Hahn-Banach for convex sets). Hard direction: given a unital *-subalgebra S that is SOT-closed, for any T in S'' and any finite family of vectors use the amplification S ⊗ 1_n acting diagonally on H^n together with the projection onto the closure of (S ⊗ 1_n) applied to the vector to produce a net in S converging SOT to T.

theorem declaration uses `sorry`vonNeumann_doubleCommutant_tfae {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) :
    List.TFAE
      [ Set.centralizer (Set.centralizer (S : Set (H →L[ℂ] H))) = S
      , IsClosed
          (ContinuousLinearMap.toWOT (RingHom.id ℂ) H H '' (S : Set (H →L[ℂ] H)))
      , IsClosed
          (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H ''
            (S : Set (H →L[ℂ] H))) ] := byH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HS:StarSubalgebra ℂ (H →L[ℂ] H)⊢ [(↑S).centralizer.centralizer = ↑S, IsClosed (⇑(ContinuousLinearMap.toWOT (RingHom.id ℂ) H H) '' ↑S),
    IsClosed (⇑(ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H) '' ↑S)].TFAE
  sorryAll goals completed! 🐙

Weak Morse inequalities

weak_morse_inequality

Submitter: Kim Morrison.

Notes: §40 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement; the boxed main theorem is the strong Morse inequality). For a Morse function f on a closed smooth finite-dimensional manifold M, b_k(M) ≤ c_k(f) for every k. Follows from the strong Morse inequality but is often proved directly via the Morse-Smale CW structure. Mathlib has the smooth-manifold framework, mfderiv, higher Fréchet derivatives, and singularHomologyFunctor but no Morse functions, Morse index, critical-point counts, Betti numbers as a named definition, or the weak Morse inequality. The Challenge ships seven helper definitions.

Source: M. Morse, The Calculus of Variations in the Large, AMS Colloq. Publ. 18 (1934). Listed as §40 additional statement in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Direct corollary of the strong Morse inequality: the alternating partial sums of c_k(f) dominate those of b_k(M); take the difference of consecutive partial sums and use that successive partial sums differ by 2·b_k − 2·c_k (with signs), to extract b_k ≤ c_k. Alternatively, prove directly via the Morse-Smale CW structure: the cellular boundary maps ∂_k : ℤ^{c_k} → ℤ^{c_{k−1}} give H_k = ker ∂_k / im ∂_{k+1}, and dim H_k ≤ c_k − rank ∂_k − rank ∂_{k+1} ≤ c_k. The weak inequality is sharper than counting: it asserts the Betti number bound for each k independently, not just the alternating sum.

theorem declaration uses `sorry`weak_morse_inequality {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless]
    {M : Type} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
    [CompactSpace M] (f : M → ℝ) (_hf : LeanEval.Geometry.WeakMorseInequality.IsMorseFunction I f) (k : ℕ) :
    bettiNumber M k ≤ morseCount I f k := byE:Type u_1inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace ℝ Einst✝⁶:FiniteDimensional ℝ EH:Type u_2inst✝⁵:TopologicalSpace HI:ModelWithCorners ℝ E Hinst✝⁴:I.BoundarylessM:Typeinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:IsManifold I ∞ Minst✝:CompactSpace Mf:M → ℝ_hf:IsMorseFunction I fk:ℕ⊢ bettiNumber M k ≤ morseCount I f k
  sorryAll goals completed! 🐙

Test problems

CI regenerate-main check

ci_regenerate_main_check

Submitter: Kim Morrison.

Notes: Internal trivial problem used to exercise the regenerate-main workflow end-to-end.

Source: Internal CI check.

Informal solution: True is true.

theorem declaration uses `sorry`ci_regenerate_main_check : True := by⊢ True
  sorryAll goals completed! 🐙

def-hole minimal example

def_hole_example

Submitter: Kim Morrison.

Notes: Minimal example exercising def + theorem holes through the comparator def-hole pipeline.

Source: Unavailable.

Informal solution: Unavailable.

def declaration uses `sorry`foo : Nat := sorry

theorem declaration uses `sorry`foo_def : foo = 37 := sorry

instance-hole minimal example

instance_hole_example

Submitter: Kim Morrison.

Notes: Minimal example exercising instance + theorem holes; instances must be named so the comparator can address them.

Source: Unavailable.

Informal solution: Unavailable.

def declaration uses `sorry`WidgetCarrier : Type := sorry

instance declaration uses `sorry`instInhabitedWidget : Inhabited WidgetCarrier := sorry

Appending a singleton increases the list length

list_append_singleton_length

Submitter: Kim Morrison.

Notes: A simple list problem that exercises notation in generated files.

Source: Internal starter problem.

Informal solution: Compute the length after append.

theorem declaration uses `sorry`list_append_singleton_length :
    (([1, 2] : List Nat).append [3]).length = 3 := by⊢ ([1, 2].append [3]).length = 3
  sorryAll goals completed! 🐙

multi-hole-with-helpers regression example

multi_hole_helpers_example

Submitter: Kim Morrison.

Notes: Regression test for trusted-helper support in multi-hole problems. Exercises three failure modes the generator used to have: (1) helpers at root namespace (`rootHelper`) must not get a spurious `open`; (2) the helper namespace `Helpers` differs from the module's last path component `MultiHoleHelpersExample`, so the injected `open` must be derived from the helper names rather than the module name; (3) the helper `Helpers.postHole` appears in source order *between* two holes, exercising the right-to-left edit pass against a layout where a sequential strip-then-replace pipeline (with helper ranges taken from `.ilean` and applied after hole-body replacement) would have shifted offsets. A submission that defines `Submission.Helpers.first := 1`, `Submission.Helpers.second_eq := rfl`, and `Submission.Helpers.third_eq := rfl` should be accepted.

Source: Unavailable.

Informal solution: Unavailable.

def declaration uses `sorry`first : Nat := sorry

theorem declaration uses `sorry`second_eq : first + rootHelper + preHole = first + 141 := sorry

theorem declaration uses `sorry`third_eq : postHole = 1000 := sorry

2 + 2 = 4

two_plus_two

Submitter: Kim Morrison.

Notes: An easy problem to get you on the leaderboard.

Source: Internal starter problem.

Informal solution: By computation.

theorem declaration uses `sorry`two_plus_two_eq_four : (2 : Nat) + 2 = 4 := by⊢ 2 + 2 = 4
  sorryAll goals completed! 🐙

variable-binder minimal example

variable_binder_example

Submitter: Kim Morrison.

Notes: Regression for https://github.com/leanprover/lean-eval/issues/276. The theorem inherits implicit binders from a preceding `variable` declaration, which the extractor must re-emit in the generated workspace.

Source: Unavailable.

Informal solution: Unavailable.

theorem declaration uses `sorry`variable_binder_example (A : Matrix n n ℚ) (hA : A.IsHermitian) :
    A.trace = ∑ i, A i i := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℚhA:A.IsHermitian⊢ A.trace = ∑ i, A i i
  sorryAll goals completed! 🐙