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

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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 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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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

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

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 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 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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

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! 🐙

Test problems

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! 🐙

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! 🐙

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! 🐙

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