diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean
new file mode 100644
index 00000000..a49374c8
--- /dev/null
+++ b/LeanEval/Geometry/MostowRigidity.lean
@@ -0,0 +1,131 @@
+import Mathlib.Algebra.Star.Unitary
+import Mathlib.Data.Real.Star
+import Mathlib.LinearAlgebra.Matrix.ConjTranspose
+import Mathlib.MeasureTheory.Group.FundamentalDomain
+import Mathlib.MeasureTheory.Measure.Haar.Basic
+import Mathlib.Topology.Instances.Matrix
+import Mathlib.Topology.MetricSpace.Pseudo.Defs
+import EvalTools.Markers
+
+/-!
+# Mostow rigidity
+
+A common form of Mostow's rigidity theorem says that two complete, finite-volume hyperbolic
+manifolds of dimension at least three must be isometric if they have isomorphic fundamental
+groups. Since the group of isometries of the hyperbolic space ℍⁿ is isomorphic to the
+projective orthogonal group PO(n,1), this can be shown to be equivalent to the following
+algebraic statement: two lattices (subgroups of finite covolume) in PO(n,1) with n ≥ 3 are
+isomorphic iff they are conjugate in PO(n,1). In this file we define the group PO(n,1) and
+state this algebraic form of Mostow rigidity. In fact, the isomorphism should agree with
+conju
+
+References:
+https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form
+Riccardo Benedetti, Carlo Petronio. *Lectures on Hyperbolic Geometry*, Chapter C
+(proof of geometric form in compact case in 50 pages).
+-/
+
+namespace LeanEval.Geometry
+
+universe u
+
+variable (p q : Type u) (α : Type*)
+
+def MatrixSum : Type _ := Matrix (p ⊕ q) (p ⊕ q) α
+
+variable [Fintype p] [Fintype q] [DecidableEq p] [DecidableEq q] [Ring α]
+
+instance : Ring (MatrixSum p q α) := inferInstanceAs (Ring (Matrix ..))
+
+variable {p q α} in
+def MatrixSum.ofMatrix : Matrix (p ⊕ q) (p ⊕ q) α ≃+* MatrixSum p q α := .refl _
+
+variable {p q α} in
+def pmOneMat : Matrix (p ⊕ q) (p ⊕ q) α := .fromBlocks 1 0 0 (-1)
+
+theorem pmOneMat_mul_pmOneMat : pmOneMat * pmOneMat = (1 : Matrix (p ⊕ q) _ α) := by
+  simp [pmOneMat, Matrix.fromBlocks_multiply]
+
+open MatrixSum Matrix
+
+section Star
+
+variable [StarRing α]
+
+omit [Fintype p] [Fintype q] in
+@[simp] theorem conjTranspose_pmOneMat : (pmOneMat : Matrix (p ⊕ q) _ α)ᴴ = pmOneMat := by
+  simp_rw [pmOneMat, conjTranspose, fromBlocks_transpose, fromBlocks_map]
+  simp [Matrix.map_neg]
+
+instance : StarRing (MatrixSum p q α) where
+  star A := .ofMatrix (pmOneMat * (ofMatrix.symm A).conjTranspose * pmOneMat)
+  star_involutive A := by
+    simp [← mul_assoc pmOneMat, mul_assoc (ofMatrix.symm A), pmOneMat_mul_pmOneMat]
+  star_mul A B := by
+    conv_lhs => rw [map_mul _ A, conjTranspose_mul, ← mul_one _ᴴ, ← pmOneMat_mul_pmOneMat]
+    simp [mul_assoc]
+  star_add A B := by simp [add_mul, mul_add]
+
+end Star
+
+section Topology
+
+variable [TopologicalSpace α]
+
+instance : TopologicalSpace (MatrixSum p q α) := inferInstanceAs (TopologicalSpace (Matrix ..))
+
+instance [T1Space α] : T1Space (MatrixSum p q α) := inferInstanceAs (T1Space (_ → _))
+
+instance [LocallyCompactSpace α] : LocallyCompactSpace (MatrixSum p q α) :=
+  inferInstanceAs (LocallyCompactSpace (_ → _))
+
+@[fun_prop] theorem MatrixSum.continuous_ofMatrix : Continuous (@ofMatrix p q α _ _ _ _ _) :=
+  continuous_id
+
+@[fun_prop] theorem MatrixSum.continuous_ofMatrix_symm : Continuous (@ofMatrix p q α ..).symm :=
+  continuous_id
+
+variable [IsTopologicalRing α]
+
+instance [Star α] [ContinuousStar α] : IsTopologicalRing (MatrixSum p q α) :=
+  inferInstanceAs (IsTopologicalRing (Matrix ..))
+
+variable [StarRing α] [ContinuousStar α]
+
+instance : ContinuousStar (MatrixSum p q α) where
+  continuous_star := by rw [star]; fun_prop
+
+theorem MatrixSum.isClosed_unitary [T1Space α] :
+    IsClosed (SetLike.coe <| unitary (MatrixSum p q α)) :=
+  .inter (isClosed_singleton.preimage <| by fun_prop) (isClosed_singleton.preimage <| by fun_prop)
+
+instance [T1Space α] [LocallyCompactSpace α] :
+    LocallyCompactSpace (unitary (MatrixSum p q α)) :=
+  (MatrixSum.isClosed_unitary ..).isClosedEmbedding_subtypeVal.locallyCompactSpace
+
+instance : IsTopologicalGroup (unitary (MatrixSum p q α)) where
+  continuous_inv := by simp_rw [Inv.inv, star]; fun_prop
+
+end Topology
+
+/-- `PO p q` is the projective indefinite orthogonal group PO(p,q) over the reals. -/
+abbrev PO (p q : ℕ) :=
+  HasQuotient.Quotient (unitary (MatrixSum (Fin p) (Fin q) ℝ)) (Subgroup.center _)
+
+variable (p q : ℕ)
+
+instance : MeasurableSpace (PO p q) := borel _
+instance : BorelSpace (PO p q) := ⟨rfl⟩
+
+open MeasureTheory
+
+noncomputable instance : MeasureSpace (PO p q) := ⟨.haar⟩
+
+@[eval_problem]
+theorem mostow_rigidity (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (PO n 1))
+    (disc_Γ : IsDiscrete (SetLike.coe Γ)) (covol_Γ : covolume Γ (PO n 1) ≠ ⊤)
+    (disc_Λ : IsDiscrete (SetLike.coe Λ)) (covol_Λ : covolume Λ (PO n 1) ≠ ⊤)
+    (f : Γ ≃* Λ) : ∃ g : PO n 1, Γ.map (MulAut.conj g) = Λ := by
+  sorry
+
+end LeanEval.Geometry
diff --git a/manifests/problems.toml b/manifests/problems.toml
deleted file mode 100644
index 0bc46648..00000000
--- a/manifests/problems.toml
+++ /dev/null
@@ -1,647 +0,0 @@
-version = 1
-
-[[problem]]
-id = "two_plus_two"
-title = "2 + 2 = 4"
-test = true
-module = "LeanEval.EasyProblems"
-holes = ["two_plus_two_eq_four"]
-submitter = "Kim Morrison"
-notes = "An easy problem to get you on the leaderboard."
-source = "Internal starter problem."
-informal_solution = "By computation."
-
-[[problem]]
-id = "ci_regenerate_main_check"
-title = "CI regenerate-main check"
-test = true
-module = "LeanEval.EasyProblems"
-holes = ["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."
-
-[[problem]]
-id = "list_append_singleton_length"
-title = "Appending a singleton increases the list length"
-test = true
-module = "LeanEval.EasyProblems"
-holes = ["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."
-
-[[problem]]
-id = "chudnovsky_formula_for_pi_inv"
-title = "Chudnovsky formula for pi inverse"
-test = false
-module = "LeanEval.Analysis.Chudnovsky"
-holes = ["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."
-
-[[problem]]
-id = "pi1_circle_mulEquiv_int"
-title = "pi_1 of the circle is Z"
-test = false
-module = "LeanEval.Topology.HomotopyGroups"
-holes = ["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."
-
-[[problem]]
-id = "finite_graph_ramsey_theorem"
-title = "Finite Ramsey theorem for graphs"
-test = false
-module = "LeanEval.Combinatorics.Ramsey"
-holes = ["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."
-
-[[problem]]
-id = "substInv_X_sub_X_sq_eq_catalan"
-title = "Catalan generating function via compositional inversion"
-test = false
-module = "LeanEval.Combinatorics.CatalanSubstInv"
-holes = ["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)."
-
-[[problem]]
-id = "riemann_hypothesis_iff_lagarias_elementary_criterion"
-title = "Lagarias criterion is equivalent to RH"
-test = false
-module = "LeanEval.NumberTheory.Lagarias"
-holes = ["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."
-
-[[problem]]
-id = "dvd_card_connectedComponent_markoffGraph"
-title = "Chen theorem for Markoff graphs"
-test = false
-module = "LeanEval.Combinatorics.MarkoffGraph"
-holes = ["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."
-
-[[problem]]
-id = "mulCayley_connected_iff_closure_eq_top"
-title = "Cayley graph connected iff generators generate the group"
-test = false
-module = "LeanEval.Combinatorics.CayleyConnected"
-holes = ["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."
-
-[[problem]]
-id = "pi3_sphere_two_mulEquiv_int"
-title = "pi_3 of the 2-sphere is Z"
-test = false
-module = "LeanEval.Topology.HomotopyGroups"
-holes = ["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."
-
-[[problem]]
-id = "pin_sphere_n_mulEquiv_int"
-title = "pi_n of the n-sphere is Z"
-test = false
-module = "LeanEval.Topology.HomotopyGroups"
-holes = ["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."
-
-[[problem]]
-id = "pi_succ_sphere_n_mulEquiv_zmod_two"
-title = "pi_(n+1) of S^n is Z/2 for n at least 3"
-test = false
-module = "LeanEval.Topology.HomotopyGroups"
-holes = ["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."
-
-[[problem]]
-id = "finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow"
-title = "Burnside p^a q^b theorem"
-test = false
-module = "LeanEval.GroupTheory.Burnside"
-holes = ["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."
-
-[[problem]]
-id = "rouche_zero_count_eq"
-title = "Rouche theorem via zero counting"
-test = false
-module = "LeanEval.ComplexAnalysis.Rouche"
-holes = ["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 = "If |g| < |f| on the boundary circle, then f and f + g have the same number of zeros inside, counted with multiplicity."
-
-[[problem]]
-id = "mem_convexHull_finset_extremePoints_of_mem_compact_convex"
-title = "Minkowski-Caratheodory theorem"
-test = false
-module = "LeanEval.ConvexGeometry.MinkowskiCaratheodory"
-holes = ["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."
-
-[[problem]]
-id = "irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius"
-title = "Perron-Frobenius for irreducible nonnegative matrices"
-test = false
-module = "LeanEval.LinearAlgebra.PerronFrobenius"
-holes = ["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."
-
-[[problem]]
-id = "exists_complementary_polynomial_on_unit_circle"
-title = "Complementary polynomial on the unit circle"
-test = false
-module = "LeanEval.ComplexAnalysis.ComplementaryPolynomials"
-holes = ["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."
-
-[[problem]]
-id = "posSemidef_map_exp"
-title = "Entrywise exponential of a PSD matrix is PSD"
-test = false
-module = "LeanEval.LinearAlgebra.EntrywiseExpPSD"
-holes = ["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."
-
-[[problem]]
-id = "oppenheim_inequality"
-title = "Oppenheim's inequality for Hadamard products"
-test = false
-module = "LeanEval.LinearAlgebra.Oppenheim"
-holes = ["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."
-
-[[problem]]
-id = "vonNeumann_doubleCommutant_tfae"
-title = "von Neumann double commutant theorem"
-test = false
-module = "LeanEval.Analysis.VonNeumannDoubleCommutant"
-holes = ["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."
-
-[[problem]]
-id = "symAction_range_eq_centralizer_glAction"
-title = "Schur-Weyl duality: S_k image equals centralizer of GL(V) image"
-test = false
-module = "LeanEval.RepresentationTheory.SchurWeyl"
-holes = ["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."
-
-[[problem]]
-id = "glAction_range_eq_centralizer_symAction"
-title = "Schur-Weyl duality: GL(V) image equals centralizer of S_k image"
-test = false
-module = "LeanEval.RepresentationTheory.SchurWeyl"
-holes = ["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."
-
-[[problem]]
-id = "g2_irrep_tensor_square_decomp"
-title = "Existence of a 64-dim irreducible g₂-representation with 14 tensor-square isotypic components"
-test = false
-module = "LeanEval.RepresentationTheory.ExceptionalLieTensorSquare"
-holes = ["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."
-
-[[problem]]
-id = "e8_irrep_tensor_square_decomp"
-title = "Existence of a 779247-dim irreducible e₈-representation with 40 tensor-square isotypic components"
-test = false
-module = "LeanEval.RepresentationTheory.ExceptionalLieTensorSquare"
-holes = ["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."
-
-[[problem]]
-id = "cerf_gamma_four"
-title = "Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometry"
-test = false
-module = "LeanEval.Topology.CerfGammaFour"
-holes = ["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."
-
-[[problem]]
-id = "smale_conjecture"
-title = "Smale conjecture (Hatcher) in relative parameterized form"
-test = false
-module = "LeanEval.Topology.SmaleConjecture"
-holes = ["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."
-
-[[problem]]
-id = "cyclotomic_integer_house_le_two"
-title = "Real cyclotomic integer with house at most 2"
-test = false
-module = "LeanEval.NumberTheory.SmallHouse"
-holes = ["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."
-
-[[problem]]
-id = "cyclotomic_integer_house_between_two_and_76_33"
-title = "Real cyclotomic integer with house in (2, 76/33)"
-test = false
-module = "LeanEval.NumberTheory.SmallHouse"
-holes = ["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."
-
-[[problem]]
-id = "gleason_theorem_finite"
-title = "Gleason's theorem (finite-dimensional)"
-test = false
-module = "LeanEval.Analysis.Gleason"
-holes = ["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."
-
-[[problem]]
-id = "gleason_theorem_separable"
-title = "Gleason's theorem (separable Hilbert space)"
-test = false
-module = "LeanEval.Analysis.Gleason"
-holes = ["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."
-[[problem]]
-id = "jacobian_challenge_diffgeo"
-title = "Jacobian of a compact Riemann surface (Buzzard challenge)"
-test = false
-module = "LeanEval.Geometry.JacobianChallenge"
-holes = [
-  "JacobianChallenge.genus",
-  "JacobianChallenge.genus_eq_zero_iff_homeo",
-  "JacobianChallenge.Jacobian",
-  "JacobianChallenge.Jacobian.instAddCommGroup",
-  "JacobianChallenge.Jacobian.instTopologicalSpace",
-  "JacobianChallenge.Jacobian.instT2Space",
-  "JacobianChallenge.Jacobian.instCompactSpace",
-  "JacobianChallenge.Jacobian.instChartedSpace",
-  "JacobianChallenge.Jacobian.instIsManifold",
-  "JacobianChallenge.Jacobian.instLieAddGroup",
-  "JacobianChallenge.Jacobian.ofCurve",
-  "JacobianChallenge.Jacobian.ofCurve_contMDiff",
-  "JacobianChallenge.Jacobian.ofCurve_self",
-  "JacobianChallenge.Jacobian.ofCurve_inj",
-  "JacobianChallenge.Jacobian.pushforward",
-  "JacobianChallenge.Jacobian.pushforward_contMDiff",
-  "JacobianChallenge.Jacobian.pushforward_id_apply",
-  "JacobianChallenge.Jacobian.pushforward_comp_apply",
-  "JacobianChallenge.Jacobian.pullback",
-  "JacobianChallenge.Jacobian.pullback_contMDiff",
-  "JacobianChallenge.Jacobian.pullback_id_apply",
-  "JacobianChallenge.Jacobian.pullback_comp_apply",
-  "JacobianChallenge.Jacobian.degree",
-  "JacobianChallenge.Jacobian.pushforward_pullback",
-]
-submitter = "Kevin Buzzard"
-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."
-
-[[problem]]
-id = "jacobian_challenge_alggeo"
-title = "Jacobian of a smooth proper curve (Merten challenge)"
-test = false
-module = "LeanEval.AlgebraicGeometry.JacobianChallenge"
-holes = [
-  "AlgebraicGeometry.JacobianChallenge.genus",
-  "AlgebraicGeometry.JacobianChallenge.Jacobian",
-  "AlgebraicGeometry.JacobianChallenge.Jacobian.instGrpObj",
-  "AlgebraicGeometry.JacobianChallenge.Jacobian.smoothOfRelativeDimension_genus",
-  "AlgebraicGeometry.JacobianChallenge.Jacobian.instIsProper",
-  "AlgebraicGeometry.JacobianChallenge.Jacobian.instGeometricallyIrreducible",
-  "AlgebraicGeometry.JacobianChallenge.Jacobian.ofCurve",
-  "AlgebraicGeometry.JacobianChallenge.Jacobian.comp_ofCurve",
-  "AlgebraicGeometry.JacobianChallenge.Jacobian.exists_unique_ofCurve_comp",
-]
-submitter = "Christian Merten"
-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."
-
-[[problem]]
-id = "def_hole_example"
-title = "def-hole minimal example"
-test = true
-module = "LeanEval.Sandbox.DefHoleExample"
-holes = ["foo", "foo_def"]
-submitter = "Kim Morrison"
-notes = "Minimal example exercising def + theorem holes through the comparator def-hole pipeline."
-
-[[problem]]
-id = "instance_hole_example"
-title = "instance-hole minimal example"
-test = true
-module = "LeanEval.Sandbox.InstanceHoleExample"
-holes = ["WidgetCarrier", "instInhabitedWidget"]
-submitter = "Kim Morrison"
-notes = "Minimal example exercising instance + theorem holes; instances must be named so the comparator can address them."
-
-[[problem]]
-id = "exists_nonisotopic_link"
-title = "Existence of a non-isotopic pair of oriented two-component links"
-test = false
-module = "LeanEval.KnotTheory.Linking"
-holes = ["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."
-
-[[problem]]
-id = "exists_nonisotopic_knots"
-title = "Existence of a non-isotopic pair of oriented knots"
-test = false
-module = "LeanEval.KnotTheory.NonIsotopicKnots"
-holes = ["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."
-
-[[problem]]
-id = "exists_chiral_knot"
-title = "Existence of a chiral oriented knot"
-test = false
-module = "LeanEval.KnotTheory.Chiral"
-holes = ["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}.)"
-
-[[problem]]
-id = "brauer_character_in_cyclotomic"
-title = "Character values of finite groups lie in cyclotomic fields"
-test = false
-module = "LeanEval.RepresentationTheory.BrauerSplittingField"
-holes = ["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."
-
-[[problem]]
-id = "m23_irrep_tensor_square_decomp"
-title = "Existence of an order-10200960 group with a 22-dim irrep whose tensor square has 4 isotypic components"
-test = false
-module = "LeanEval.RepresentationTheory.M23TensorSquare"
-holes = ["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."
-
-[[problem]]
-id = "frobenius_kernel_isNormal"
-title = "Frobenius's theorem: the Frobenius kernel is normal"
-test = false
-module = "LeanEval.GroupTheory.Frobenius"
-holes = ["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."
-
-[[problem]]
-id = "glauberman_zStar"
-title = "Glauberman's Z* theorem for isolated involutions"
-test = false
-module = "LeanEval.GroupTheory.GlaubermanZStar"
-holes = ["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."
-
-[[problem]]
-id = "schreier_conjecture"
-title = "Schreier's conjecture: outer automorphism group of a finite simple group is solvable"
-test = false
-module = "LeanEval.GroupTheory.SchreierConjecture"
-holes = ["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."
-
-[[problem]]
-id = "five_transitive_card_classification"
-title = "Possible orders of 5-transitive finite permutation groups"
-test = false
-module = "LeanEval.GroupTheory.MultiplyTransitive"
-holes = ["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."
-
-[[problem]]
-id = "topological_classification_of_surfaces"
-title = "Topological classification of surfaces"
-test = false
-module = "LeanEval.Topology.ClassificationOfSurfaces"
-holes = ["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."
-
-[[problem]]
-id = "deBranges_theorem"
-title = "De Branges's theorem (Bieberbach conjecture)"
-test = false
-module = "LeanEval.ComplexAnalysis.DeBranges"
-holes = ["deBranges"]
-submitter = "Junyan Xu"
-source = "John B. Conway, *Functions of One Complex Variable II*, Chapter 17."
-
-[[problem]]
-id = "cubic_decay_asymptotic"
-title = "Polynomial decay rate of y' = -y^3"
-test = false
-module = "LeanEval.Analysis.ODE.CubicDecay"
-holes = ["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."
-
-[[problem]]
-id = "bakerWustholz_linearForms_logs"
-title = "Baker-Wüstholz theorem on linear forms in logarithms"
-test = false
-module = "LeanEval.NumberTheory.BakerWustholz"
-holes = ["bakerWustholz_linearForms_logs"]
-submitter = "Ralf Stephan"
-source = "A. Baker, G. Wüstholz, Logarithmic forms and group varieties, J. reine angew. Math. 442 (1993), 19-62."
-
-[[problem]]
-id = "sturm_separation"
-title = "Sturm separation theorem"
-test = false
-module = "LeanEval.Analysis.ODE.SturmSeparation"
-holes = ["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."
-
-[[problem]]
-id = "dirichlet_eigenvalues_eq_nat_sq"
-title = "Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2"
-test = false
-module = "LeanEval.Analysis.ODE.DirichletEigenvalues"
-holes = ["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."
-
-[[problem]]
-id = "linear_ode_asymptotic_stability"
-title = "Linear ODE with negative-real-part eigenvalues is asymptotically stable"
-test = false
-module = "LeanEval.Analysis.ODE.LinearStability"
-holes = ["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."
-
-[[problem]]
-id = "bvp_comparison"
-title = "Comparison principle for the Dirichlet BVP"
-test = false
-module = "LeanEval.Analysis.ODE.BVPComparison"
-holes = ["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+."
-
-[[problem]]
-id = "heat_kernel_solves_heat_equation"
-title = "Gaussian heat kernel solves the 1D heat equation"
-test = false
-module = "LeanEval.Analysis.ODE.HeatKernel"
-holes = ["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."
-
-[[problem]]
-id = "contractibleSpace_houseWithTwoRooms"
-title = "Bing's house with two rooms is contractible"
-test = false
-module = "LeanEval.Topology.HouseWithTwoRooms"
-holes = ["contractibleSpace_houseWithTwoRooms"]
-submitter = "Junyan Xu"
-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."
-
-[[problem]]
-id = "fermat_last_theorem"
-title = "Fermat's Last Theorem"
-test = false
-module = "LeanEval.NumberTheory.FermatLastTheorem"
-holes = ["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"
-
-[[problem]]
-id = "rado_riemannSurface"
-title = "Radó's theorem on Riemann surfaces"
-test = false
-module = "LeanEval.Geometry.RadoTheorem"
-holes = ["rado_riemannSurface"]
-submitter = "Junyan Xu"
-source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, §1.3."
-
-[[problem]]
-id = "neukirch_uchida"
-title = "Neukirch–Uchida theorem"
-test = false
-module = "LeanEval.NumberTheory.NeukirchUchida"
-holes = ["neukirch_uchida"]
-submitter = "Junyan Xu"
-source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1."