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.

Source: https://link.springer.com/article/10.1007/s40316-018-0102-6

Informal solution: Evaluate the Chudnovsky series and prove that it sums to 1 / pi.

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_logCounting_zero_eq

Submitter: Kim Morrison.

Notes: Phrases Rouché's theorem as equality of zero-counting functions for f and f + g.

Source: Classical theorem in complex analysis.

Informal solution: If |g| < |f| on the boundary circle, then f and f + g have the same number of zeros inside, counted with multiplicity.

theorem declaration uses `sorry`rouche_logCounting_zero_eq {f g : ℂ → ℂ} {R : ℝ}
    (hR : 1 ≤ R)
    (hf : Meromorphic f)
    (hg : AnalyticOn ℂ g Set.univ)
    (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) :
    logCounting (f + g) 0 R = logCounting f 0 R := byf:ℂ → ℂg:ℂ → ℂR:ℝhR:1 ≤ Rhf:Meromorphic fhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ logCounting (f + g) 0 R = logCounting f 0 R
  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]
    (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 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 β = (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

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