Lean AI formalization leaderboard

lean-eval

Lean AI formalization leaderboard

Public results on a benchmark of hard Lean formalization problems. Expand any row to inspect solved theorems, extracted statements, and links to public proofs when available.

21
19
9
112

Leaderboard

Model rankings

Ranked by main benchmark problems solved. Internal test problems do not count toward the score.

1Seed Prover (ByteDance)45 solved

Problems uniquely solved by this model

Liouville–Arnold theorem on integrable systems
liouville_arnold

Verso theorem preview

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

Automatically proved by Seed Prover.

Rokhlin lemma
rokhlin_lemma

Verso theorem preview

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

Automatically proved by Seed Prover.

Other solved problems

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

Verso theorem preview

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

Automatically proved by Seed Prover.

Lidskii's inequality
lidskii_inequality

Verso theorem preview

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

Automatically proved by Seed Prover.

Lidskii–Last eigenvalue-perturbation theorem
lidskii_last

Verso theorem preview

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

Automatically proved by Seed Prover.

Runge's theorem
runge_theorem

Verso theorem preview

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

Automatically proved by Seed Prover.

Baer–Suzuki theorem
baer_suzuki

Verso theorem preview

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

Automatically proved by Seed Prover.

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

Verso theorem preview

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

Automatically proved by Seed Prover.

Frobenius's theorem: the Frobenius kernel is normal
frobenius_kernel_isNormal

Verso theorem preview

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

Automatically proved by Seed Prover.

Independence of the parallel postulate
parallel_postulate_independent

Verso theorem preview

theorem declaration uses `sorry`parallel_postulate_independent : (∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), LeanEval.Geometry.Euclidean M T) ∧ (∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), ¬ LeanEval.Geometry.Euclidean M T) := ⊢ (∃ M T, Euclidean M T) ∧ ∃ M T, ¬Euclidean M T All goals completed! 🐙
#10
How produced

Automatically proved by Seed Prover.

Sturm's theorem
sturm

Verso theorem preview

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

Automatically proved by Seed Prover.

Nash equilibrium existence theorem
nash_equilibrium_exists

Verso theorem preview

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

Automatically proved by Seed Prover.

Symplectic matrices have determinant 1
symplectic_matrix_det

Verso theorem preview

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

Automatically proved by Seed Prover.

Brauer–Fowler theorem
brauer_fowler

Verso theorem preview

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

Automatically proved by Seed Prover.

Balanceable k-bounded partitions
balanceable_bounded_partitions

Verso theorem preview

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

Verso theorem preview

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

Automatically proved by Seed Prover.

Brouwer fixed-point theorem
brouwer_fixed_point

Verso theorem preview

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

Automatically proved by Seed Prover.

Kakutani fixed-point theorem
kakutani_fixed_point

Verso theorem preview

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

Automatically proved by Seed Prover.

Koszul formula
koszul_formula

Verso theorem preview

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

Automatically proved by Seed Prover.

Burnside p^a q^b theorem
finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow

Verso theorem preview

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 := G: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 All goals completed! 🐙
#20
Chen theorem for Markoff graphs
dvd_card_connectedComponent_markoffGraph

Verso theorem preview

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 := p:ℕhp:Nat.Prime phgt:3 < p⊢ ∀ (c : (markoffGraph p).ConnectedComponent), p ∣ Nat.card ↥c All goals completed! 🐙
#21
A competition programming problem about permuting a permutation to be unimodal
permute_to_unimodal

Verso theorem preview

theorem declaration uses `sorry`minRearrange_correct {arr : Array Nat} : arr.Perm (1...=arr.size).toArray → (∃ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x ∧ LeanEval.ProgramVerification.differences (Vector.mk x (arr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size All goals completed! 🐙)) arr.toVector = LeanEval.ProgramVerification.minRearrange arr) ∧ (∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x → LeanEval.ProgramVerification.minRearrange arr ≤ LeanEval.ProgramVerification.differences (Vector.mk x (arr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size All goals completed! 🐙)) arr.toVector) := arr:Array Nat⊢ arr.Perm (1...=arr.size).toArray → (∃ x hx, Unimodal x ∧ differences (Vector.mk x ⋯) arr.toVector = minRearrange arr) ∧ ∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), Unimodal x → minRearrange arr ≤ differences (Vector.mk x ⋯) arr.toVector All goals completed! 🐙
#22
Bing's house with two rooms is contractible
contractibleSpace_houseWithTwoRooms

Verso theorem preview

theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := ⊢ ContractibleSpace ↑HouseWithTwoRooms All goals completed! 🐙
#23
Linear ODE with negative-real-part eigenvalues is asymptotically stable
linear_ode_asymptotic_stability

Verso theorem preview

theorem declaration uses `sorry`linear_ode_asymptotic_stability (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ) (hA : ∀ μ : ℂ, Module.End.HasEigenvalue (Matrix.toLin' (A.map (algebraMap ℝ ℂ))) μ → μ.re < 0) (x : ℝ → (Fin n → ℝ)) (hx : ∀ t : ℝ, 0 < t → HasDerivAt x (A.mulVec (x t)) t) : Filter.Tendsto (fun t : ℝ => ‖x t‖) Filter.atTop (nhds 0) := n:ℕA:Matrix (Fin n) (Fin n) ℝhA:∀ (μ : ℂ), Module.End.HasEigenvalue (Matrix.toLin' (A.map ⇑(algebraMap ℝ ℂ))) μ → μ.re < 0x:ℝ → Fin n → ℝhx:∀ (t : ℝ), 0 < t → HasDerivAt x (A *ᵥ x t) t⊢ Filter.Tendsto (fun t => ‖x t‖) Filter.atTop (nhds 0) All goals completed! 🐙
#24
Existence of a non-isotopic pair of oriented two-component links
exists_nonisotopic_link

Verso theorem preview

theorem declaration uses `sorry`exists_nonisotopic_link : ∃ L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := ⊢ ∃ L₁ L₂, ¬L₁.Isotopic L₂ All goals completed! 🐙
#25
Schur-Weyl duality: GL(V) image equals centralizer of S_k image
glAction_range_eq_centralizer_symAction

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#26
Schur-Weyl duality: S_k image equals centralizer of GL(V) image
symAction_range_eq_centralizer_glAction

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#27
Gaussian heat kernel solves the 1D heat equation
heat_kernel_solves_heat_equation

Verso theorem preview

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

Verso theorem preview

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

Verso theorem preview

theorem declaration uses `sorry`rouche_zero_count_eq {f g : ℂ → ℂ} {R : ℝ} (hR : 0 < R) (hf : MeromorphicNFOn f Set.univ) (hg : AnalyticOn ℂ g Set.univ) (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) : (∑ᶠ z, ((divisor (f + g) (Metric.closedBall 0 R))⁺) z) = (∑ᶠ z, ((divisor f (Metric.closedBall 0 R))⁺) z) := f:ℂ → ℂg:ℂ → ℂR:ℝhR:0 < Rhf:MeromorphicNFOn f Set.univhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ ∑ᶠ (z : ℂ), (divisor (f + g) (Metric.closedBall 0 R))⁺ z = ∑ᶠ (z : ℂ), (divisor f (Metric.closedBall 0 R))⁺ z All goals completed! 🐙
#30
Real cyclotomic integer with house at most 2
cyclotomic_integer_house_le_two

Verso theorem preview

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) := K: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) All goals completed! 🐙
#31
Complementary polynomial on the unit circle
exists_complementary_polynomial_on_unit_circle

Verso theorem preview

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 := P:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1 All goals completed! 🐙
#32
von Neumann double commutant theorem
vonNeumann_doubleCommutant_tfae

Verso theorem preview

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))) ] := H: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 All goals completed! 🐙
#33
Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2
dirichlet_eigenvalues_eq_nat_sq

Verso theorem preview

theorem declaration uses `sorry`dirichlet_eigenvalues_eq_nat_sq (lam : ℝ) : (∃ (y : ℝ → ℝ) (J : Set ℝ), IsOpen J ∧ Set.Icc (0 : ℝ) Real.pi ⊆ J ∧ (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧ (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y Real.pi = 0 ∧ ∃ x ∈ Set.Ioo (0 : ℝ) Real.pi, y x ≠ 0) ↔ ∃ n : ℕ, 0 < n ∧ lam = (n : ℝ) ^ 2 := lam:ℝ⊢ (∃ y J, IsOpen J ∧ Set.Icc 0 π ⊆ J ∧ (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧ (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y π = 0 ∧ ∃ x ∈ Set.Ioo 0 π, y x ≠ 0) ↔ ∃ n, 0 < n ∧ lam = ↑n ^ 2 All goals completed! 🐙
#34
Oppenheim's inequality for Hadamard products
oppenheim_inequality

Verso theorem preview

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 := n: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 All goals completed! 🐙
#35
Entrywise exponential of a PSD matrix is PSD
posSemidef_map_exp

Verso theorem preview

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 := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef All goals completed! 🐙
#36
Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan

Verso theorem preview

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) : haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2)) n:ℕ⊢ Invertible 1; All goals completed! 🐙 coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1) All goals completed! 🐙
#37
Minkowski-Caratheodory theorem
mem_convexHull_finset_extremePoints_of_mem_compact_convex

Verso theorem preview

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) := E: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 All goals completed! 🐙
#38
Character values of finite groups lie in cyclotomic fields
brauer_character_in_cyclotomic

Verso theorem preview

theorem declaration uses `sorry`brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] : ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ, ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V) (ρ : Representation ℂ G V) (g : G), LinearMap.trace ℂ V (ρ g) ∈ φ.range := G:Typeinst✝¹:Group Ginst✝:Fintype G⊢ ∃ φ, ∀ (V : Type) (x : AddCommGroup V) (x_1 : Module ℂ V), FiniteDimensional ℂ V → ∀ (ρ : Representation ℂ G V) (g : G), (LinearMap.trace ℂ V) (ρ g) ∈ φ.range All goals completed! 🐙
#39
Polynomial decay rate of y' = -y^3
cubic_decay_asymptotic

Verso theorem preview

theorem declaration uses `sorry`cubic_decay_asymptotic (y : ℝ → ℝ) (hy_diff : ∀ t : ℝ, 0 < t → HasDerivAt y (-(y t) ^ 3) t) (hy_cont : ContinuousWithinAt y (Set.Ici 0) 0) (hy0 : y 0 = 1) : Tendsto (fun t : ℝ => y t * Real.sqrt t) atTop (𝓝 (1 / Real.sqrt 2)) := y:ℝ → ℝhy_diff:∀ (t : ℝ), 0 < t → HasDerivAt y (-y t ^ 3) thy_cont:ContinuousWithinAt y (Set.Ici 0) 0hy0:y 0 = 1⊢ Tendsto (fun t => y t * √t) atTop (𝓝 (1 / √2)) All goals completed! 🐙
#40
Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top

Verso theorem preview

theorem declaration uses `sorry`mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] (S : Set G) : (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := G:Type u_1inst✝:Group GS:Set G⊢ (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ All goals completed! 🐙
#41
pi_1 of the circle is Z
pi1_circle_mulEquiv_int

Verso theorem preview

theorem declaration uses `sorry`pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ) All goals completed! 🐙
#42
Sturm separation theorem
sturm_separation

Verso theorem preview

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

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#44
Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Submission history

First submissionMay 20, 2026
Last submissionJun 1, 2026

Contributors

GanjinZero45
2Aleph Prover(logicalintelligence.com)43 solved

Other solved problems

Lidskii–Last eigenvalue-perturbation theorem
lidskii_last

Verso theorem preview

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

The proof required `lidskii_inequality` solution, it was previously solved by Aleph, then for this run it had access to that whole proof. At the end, only the `lidskii_inequality` theorem itself was needed. No other human intervention other wise.

Lidskii's inequality
lidskii_inequality

Verso theorem preview

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

Solved completely autonomously without human intervention

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

Verso theorem preview

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

Solved completely autonomously without human intervention

Runge's theorem
runge_theorem

Verso theorem preview

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

Solved completely autonomously without human intervention

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

Verso theorem preview

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

Solved completely autonomously without human intervention

Baer–Suzuki theorem
baer_suzuki

Verso theorem preview

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

Solved completely autonomously without human intervention

Frobenius's theorem: the Frobenius kernel is normal
frobenius_kernel_isNormal

Verso theorem preview

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

Solved completely autonomously without human intervention

Nash equilibrium existence theorem
nash_equilibrium_exists

Verso theorem preview

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

The solution used schauder_fixed_point. Schauder fixed-point theorem was first proven by Aleph and then manually inlined. Other than that, the solution was produced autonomously.

Sturm's theorem
sturm

Verso theorem preview

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

Solved completely autonomously without human intervention

Independence of the parallel postulate
parallel_postulate_independent

Verso theorem preview

theorem declaration uses `sorry`parallel_postulate_independent : (∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), LeanEval.Geometry.Euclidean M T) ∧ (∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), ¬ LeanEval.Geometry.Euclidean M T) := ⊢ (∃ M T, Euclidean M T) ∧ ∃ M T, ¬Euclidean M T All goals completed! 🐙
#10
How produced

Solved completely autonomously without human intervention

Symplectic matrices have determinant 1
symplectic_matrix_det

Verso theorem preview

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

Solved completely autonomously without human intervention

Brauer–Fowler theorem
brauer_fowler

Verso theorem preview

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

Solved completely autonomously without human intervention

Balanceable k-bounded partitions
balanceable_bounded_partitions

Verso theorem preview

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

Solved without human intervention. Two `native_decide`'s were used in the AI-generated proof(one as `interval_cases k <;> native_decide`). Those were replaced with `decide` manually. The goals that were solved by `native_decide`->`decide` were: ``` ⊢ ∑ i ∈ Finset.Icc 1 0, i * (i - 2) ≤ 0 * (0 - 1) * (0 - 2) / 2 case pos.«0» k : ℕ ih : ∑ i ∈ Finset.Icc 1 0, i * (i - 2) ≤ 0 * (0 - 1) * (0 - 2) / 2 hk : 0 < 3 ⊢ ∑ i ∈ Finset.Icc 1 (0 + 1), i * (i - 2) ≤ (0 + 1) * (0 + 1 - 1) * (0 + 1 - 2) / 2 case pos.«1» k : ℕ ih : ∑ i ∈ Finset.Icc 1 1, i * (i - 2) ≤ 1 * (1 - 1) * (1 - 2) / 2 hk : 1 < 3 ⊢ ∑ i ∈ Finset.Icc 1 (1 + 1), i * (i - 2) ≤ (1 + 1) * (1 + 1 - 1) * (1 + 1 - 2) / 2 case pos.«2» k : ℕ ih : ∑ i ∈ Finset.Icc 1 2, i * (i - 2) ≤ 2 * (2 - 1) * (2 - 2) / 2 hk : 2 < 3 ⊢ ∑ i ∈ Finset.Icc 1 (2 + 1), i * (i - 2) ≤ (2 + 1) * (2 + 1 - 1) * (2 + 1 - 2) / 2 ``` (Aleph wasn't rerun in strict mode just to save time)

Kakutani fixed-point theorem
kakutani_fixed_point

Verso theorem preview

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

The solution used brouwer_fixed_point. Brouwer fixed-point theorem was first proved by Aleph and then manually inlined. Other than that, the solutions were produced autonomously.

Schauder fixed-point theorem
schauder_fixed_point

Verso theorem preview

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

The solution used brouwer_fixed_point. Brouwer fixed-point theorem was first proved by Aleph and then manually inlined. Other than that, the solutions were produced autonomously.

Brouwer fixed-point theorem
brouwer_fixed_point

Verso theorem preview

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

First attempt used `pin_sphere_n_mulEquiv_int` which Aleph can't prove yet. For the second attempt we asked Aleph to use Milnor's proof instead and to avoid "`HomotopyGroup.Pi`, `pin_sphere_n_mulEquiv_int`, `pi1_circle_mulEquiv_int`, singular/cellular homology, or fundamental groups. Mathlib's algebraic-topology infrastructure is too thin to prove "S^(d-1) is not contractible"(that was human judgement).

Koszul formula
koszul_formula

Verso theorem preview

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

Solved completely autonomously without human intervention

A competition programming problem about permuting a permutation to be unimodal
permute_to_unimodal

Verso theorem preview

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

Solved completely autonomously without human intervention

Chen theorem for Markoff graphs
dvd_card_connectedComponent_markoffGraph

Verso theorem preview

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 := p:ℕhp:Nat.Prime phgt:3 < p⊢ ∀ (c : (markoffGraph p).ConnectedComponent), p ∣ Nat.card ↥c All goals completed! 🐙
#19
How produced

Solved completely autonomously without human intervention

Burnside p^a q^b theorem
finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow

Verso theorem preview

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 := G: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 All goals completed! 🐙
#20
How produced

Solved completely autonomously without human intervention

Bing's house with two rooms is contractible
contractibleSpace_houseWithTwoRooms

Verso theorem preview

theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := ⊢ ContractibleSpace ↑HouseWithTwoRooms All goals completed! 🐙
#21
How produced

Solved completely autonomously without human intervention

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

Verso theorem preview

theorem declaration uses `sorry`exists_nonisotopic_link : ∃ L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := ⊢ ∃ L₁ L₂, ¬L₁.Isotopic L₂ All goals completed! 🐙
#22
How produced

Solved completely autonomously without human intervention

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

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#23
How produced

Solved without human intervention Solution to glAction_range_eq_centralizer_symAction was used for this proof as internally all the benchmark problems were put into a single Lean project. We manually inlined that solution.

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

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#24
How produced

Solved completely autonomously without human intervention

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

Verso theorem preview

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

Solved completely autonomously without human intervention

Rouche theorem via zero counting
rouche_zero_count_eq

Verso theorem preview

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

Solved completely autonomously without human intervention

Perron-Frobenius for irreducible nonnegative matrices
irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

Verso theorem preview

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

Solved completely autonomously without human intervention

von Neumann double commutant theorem
vonNeumann_doubleCommutant_tfae

Verso theorem preview

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))) ] := H: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 All goals completed! 🐙
#28
How produced

Solved completely autonomously without human intervention

Real cyclotomic integer with house at most 2
cyclotomic_integer_house_le_two

Verso theorem preview

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) := K: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) All goals completed! 🐙
#29
How produced

Solved completely autonomously without human intervention

Complementary polynomial on the unit circle
exists_complementary_polynomial_on_unit_circle

Verso theorem preview

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 := P:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1 All goals completed! 🐙
#30
How produced

Solved completely autonomously without human intervention

Gaussian heat kernel solves the 1D heat equation
heat_kernel_solves_heat_equation

Verso theorem preview

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

Solved completely autonomously without human intervention

Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan

Verso theorem preview

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) : haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2)) n:ℕ⊢ Invertible 1; All goals completed! 🐙 coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1) All goals completed! 🐙
#32
How produced

Solved completely autonomously without human intervention

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

Verso theorem preview

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

Solved completely autonomously without human intervention

Minkowski-Caratheodory theorem
mem_convexHull_finset_extremePoints_of_mem_compact_convex

Verso theorem preview

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) := E: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 All goals completed! 🐙
#34
How produced

Solved completely autonomously without human intervention

Oppenheim's inequality for Hadamard products
oppenheim_inequality

Verso theorem preview

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 := n: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 All goals completed! 🐙
#35
How produced

Solved completely autonomously without human intervention

Entrywise exponential of a PSD matrix is PSD
posSemidef_map_exp

Verso theorem preview

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 := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef All goals completed! 🐙
#36
How produced

Solved completely autonomously without human intervention

Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top

Verso theorem preview

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

Solved completely autonomously without human intervention

Character values of finite groups lie in cyclotomic fields
brauer_character_in_cyclotomic

Verso theorem preview

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

Solved completely autonomously without human intervention

Polynomial decay rate of y' = -y^3
cubic_decay_asymptotic

Verso theorem preview

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

Solved completely autonomously without human intervention

pi_1 of the circle is Z
pi1_circle_mulEquiv_int

Verso theorem preview

theorem declaration uses `sorry`pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ) All goals completed! 🐙
#40
How produced

Solved completely autonomously without human intervention

Sturm separation theorem
sturm_separation

Verso theorem preview

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

Solved completely autonomously without human intervention

Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#44
How produced

Solved without human intervention. Then manual one-line fix applied for 4.30 because, as of now, Aleph only supports lean/mathlib versions up to 4.29. ``` 34 - exact ⟨(SimpleGraph.Embedding.induce S).comp f⟩ 34 + exact ⟨(SimpleGraph.Copy.induce G S).comp f⟩ ```

Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Solved completely autonomously without human intervention

Test problems: def_hole_example, instance_hole_example, ci_regenerate_main_check, list_append_singleton_length, two_plus_two (5 / 7 solved)

Submission history

First submissionMay 7, 2026
Last submissionJun 1, 2026

Contributors

mayorov-m-a44antpavzhi4
3Aristotle (Harmonic)38 solved

Other solved problems

Symplectic matrices have determinant 1
symplectic_matrix_det

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with prompting and submission by John Jennings. No human review of the proofs was performed; correctness was checked only through the benchmark comparator. The Brouwer fixed-point theorem formalization component of the `schauder_fixed_point` proof was extracted from Aristotle's proof of `brouwer_fixed_point`.

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

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Nash equilibrium existence theorem
nash_equilibrium_exists

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Independence of the parallel postulate
parallel_postulate_independent

Verso theorem preview

theorem declaration uses `sorry`parallel_postulate_independent : (∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), LeanEval.Geometry.Euclidean M T) ∧ (∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), ¬ LeanEval.Geometry.Euclidean M T) := ⊢ (∃ M T, Euclidean M T) ∧ ∃ M T, ¬Euclidean M T All goals completed! 🐙
#5
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Sturm's theorem
sturm

Verso theorem preview

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

Solved autonomously by aristotle. Manually bumped to 4.30.0-rc2.

Brauer–Fowler theorem
brauer_fowler

Verso theorem preview

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

Auto-formalized by Aristotle

Frobenius's theorem: the Frobenius kernel is normal
frobenius_kernel_isNormal

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Balanceable k-bounded partitions
balanceable_bounded_partitions

Verso theorem preview

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

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with prompting and submission by John Jennings. No human review of the proofs was performed; correctness was checked only through the benchmark comparator. The Brouwer fixed-point theorem formalization component of the `schauder_fixed_point` proof was extracted from Aristotle's proof of `brouwer_fixed_point`.

Kakutani fixed-point theorem
kakutani_fixed_point

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with prompting and submission by John Jennings. No human review of the proofs was performed; correctness was checked only through the benchmark comparator. The Brouwer fixed-point theorem formalization component of this proof was extracted from Aristotle's proof `brouwer_fixed_point`.

Brouwer fixed-point theorem
brouwer_fixed_point

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with prompting and submission by John Jennings. No human review of the proofs was performed; correctness was checked only through the benchmark comparator. Most of this proof was extracted from an intermediate result that Aristotle used to prove `nash_equilibrium_exists`.

Koszul formula
koszul_formula

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

A competition programming problem about permuting a permutation to be unimodal
permute_to_unimodal

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Burnside p^a q^b theorem
finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow

Verso theorem preview

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 := G: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 All goals completed! 🐙
#15proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Chen theorem for Markoff graphs
dvd_card_connectedComponent_markoffGraph

Verso theorem preview

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 := p:ℕhp:Nat.Prime phgt:3 < p⊢ ∀ (c : (markoffGraph p).ConnectedComponent), p ∣ Nat.card ↥c All goals completed! 🐙
#16proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration by Stefano Rocca and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Bing's house with two rooms is contractible
contractibleSpace_houseWithTwoRooms

Verso theorem preview

theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := ⊢ ContractibleSpace ↑HouseWithTwoRooms All goals completed! 🐙
#17
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

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

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#18proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

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

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#19proof
Existence of a non-isotopic pair of oriented two-component links
exists_nonisotopic_link

Verso theorem preview

theorem declaration uses `sorry`exists_nonisotopic_link : ∃ L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := ⊢ ∃ L₁ L₂, ¬L₁.Isotopic L₂ All goals completed! 🐙
#20proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

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

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Rouche theorem via zero counting
rouche_zero_count_eq

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Real cyclotomic integer with house at most 2
cyclotomic_integer_house_le_two

Verso theorem preview

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) := K: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) All goals completed! 🐙
#23proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Complementary polynomial on the unit circle
exists_complementary_polynomial_on_unit_circle

Verso theorem preview

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 := P:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1 All goals completed! 🐙
#24proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Perron-Frobenius for irreducible nonnegative matrices
irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

von Neumann double commutant theorem
vonNeumann_doubleCommutant_tfae

Verso theorem preview

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))) ] := H: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 All goals completed! 🐙
#26proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Gaussian heat kernel solves the 1D heat equation
heat_kernel_solves_heat_equation

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI, with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Minkowski-Caratheodory theorem
mem_convexHull_finset_extremePoints_of_mem_compact_convex

Verso theorem preview

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) := E: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 All goals completed! 🐙
#28proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

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

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI, with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Oppenheim's inequality for Hadamard products
oppenheim_inequality

Verso theorem preview

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 := n: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 All goals completed! 🐙
#30proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI, with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Entrywise exponential of a PSD matrix is PSD
posSemidef_map_exp

Verso theorem preview

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 := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef All goals completed! 🐙
#31proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI v1.0.1, with submission orchestration by Kim Morrison. The proof was generated against Aristotle's default Lean v4.28.0 / Mathlib v4.28.0 target; submitted here against the benchmark's pinned Lean v4.30.0-rc2 + pinned Mathlib commit. Comparator's verdict applies — proofs that exploit features added to Mathlib after v4.28.0 will compile; those that rely on tactic behaviour that changed are at the mercy of forward compatibility.

Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan

Verso theorem preview

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) : haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2)) n:ℕ⊢ Invertible 1; All goals completed! 🐙 coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1) All goals completed! 🐙
#32proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI v1.0.1, with submission orchestration by Kim Morrison. The proof was generated against Aristotle's default Lean v4.28.0 / Mathlib v4.28.0 target; submitted here against the benchmark's pinned Lean v4.30.0-rc2 + pinned Mathlib commit. Comparator's verdict applies — proofs that exploit features added to Mathlib after v4.28.0 will compile; those that rely on tactic behaviour that changed are at the mercy of forward compatibility.

Sturm separation theorem
sturm_separation

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic), with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Character values of finite groups lie in cyclotomic fields
brauer_character_in_cyclotomic

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI, with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

pi_1 of the circle is Z
pi1_circle_mulEquiv_int

Verso theorem preview

theorem declaration uses `sorry`pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ) All goals completed! 🐙
#35proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI, with orchestration and submission by Lorenzo Luccioli. No human review or supervision of the proofs was performed; correctness was checked only through the benchmark comparator.

Polynomial decay rate of y' = -y^3
cubic_decay_asymptotic

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI v1.0.1, with submission orchestration by Kim Morrison. The proof was generated against Aristotle's default Lean v4.28.0 / Mathlib v4.28.0 target; submitted here against the benchmark's pinned Lean v4.30.0-rc2 + pinned Mathlib commit. Comparator's verdict applies — proofs that exploit features added to Mathlib after v4.28.0 will compile; those that rely on tactic behaviour that changed are at the mercy of forward compatibility.

Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI v1.0.1, with submission orchestration by Kim Morrison. The proof was generated against Aristotle's default Lean v4.28.0 / Mathlib v4.28.0 target; submitted here against the benchmark's pinned Lean v4.30.0-rc2 + pinned Mathlib commit. Comparator's verdict applies — proofs that exploit features added to Mathlib after v4.28.0 will compile; those that rely on tactic behaviour that changed are at the mercy of forward compatibility.

Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#40proof
How produced

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI v1.0.1, with submission orchestration by Kim Morrison. The proof was generated against Aristotle's default Lean v4.28.0 / Mathlib v4.28.0 target; submitted here against the benchmark's pinned Lean v4.30.0-rc2 + pinned Mathlib commit. Comparator's verdict applies — proofs that exploit features added to Mathlib after v4.28.0 will compile; those that rely on tactic behaviour that changed are at the mercy of forward compatibility.

Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Solved by the Aristotle automated theorem prover (Harmonic) via the `aristotle` CLI v1.0.1, with submission orchestration by Kim Morrison. The proof was generated against Aristotle's default Lean v4.28.0 / Mathlib v4.28.0 target; submitted here against the benchmark's pinned Lean v4.30.0-rc2 + pinned Mathlib commit. Comparator's verdict applies — proofs that exploit features added to Mathlib after v4.28.0 will compile; those that rely on tactic behaviour that changed are at the mercy of forward compatibility.

Test problems: variable_binder_example, def_hole_example, instance_hole_example, list_append_singleton_length, ci_regenerate_main_check, two_plus_two (6 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionJun 1, 2026

Contributors

LorenzoLuccioli26sqrt-of-212kim-em10JohnEdwardJennings4parabamoghv2adrianmartir1Parcly-Taxel1
4Stealth Model30 solved

Other solved problems

Koszul formula
koszul_formula

Verso theorem preview

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

Verso theorem preview

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

Verso theorem preview

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

Verso theorem preview

theorem declaration uses `sorry`schauder_fixed_point {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {K : Set E} (_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K) (_hK_nonempty : K.Nonempty) (f : E → E) (_hf_cont : ContinuousOn f K) (_hf_maps : Set.MapsTo f K K) : ∃ x ∈ K, f x = x := E:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EK:Set E_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.Nonemptyf:E → E_hf_cont:ContinuousOn f K_hf_maps:Set.MapsTo f K K⊢ ∃ x ∈ K, f x = x All goals completed! 🐙
#5
A competition programming problem about permuting a permutation to be unimodal
permute_to_unimodal

Verso theorem preview

theorem declaration uses `sorry`minRearrange_correct {arr : Array Nat} : arr.Perm (1...=arr.size).toArray → (∃ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x ∧ LeanEval.ProgramVerification.differences (Vector.mk x (arr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size All goals completed! 🐙)) arr.toVector = LeanEval.ProgramVerification.minRearrange arr) ∧ (∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x → LeanEval.ProgramVerification.minRearrange arr ≤ LeanEval.ProgramVerification.differences (Vector.mk x (arr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size All goals completed! 🐙)) arr.toVector) := arr:Array Nat⊢ arr.Perm (1...=arr.size).toArray → (∃ x hx, Unimodal x ∧ differences (Vector.mk x ⋯) arr.toVector = minRearrange arr) ∧ ∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), Unimodal x → minRearrange arr ≤ differences (Vector.mk x ⋯) arr.toVector All goals completed! 🐙
#6
Chen theorem for Markoff graphs
dvd_card_connectedComponent_markoffGraph

Verso theorem preview

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 := p:ℕhp:Nat.Prime phgt:3 < p⊢ ∀ (c : (markoffGraph p).ConnectedComponent), p ∣ Nat.card ↥c All goals completed! 🐙
#7
Burnside p^a q^b theorem
finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow

Verso theorem preview

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 := G: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 All goals completed! 🐙
#8
Bing's house with two rooms is contractible
contractibleSpace_houseWithTwoRooms

Verso theorem preview

theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := ⊢ ContractibleSpace ↑HouseWithTwoRooms All goals completed! 🐙
#9
Schur-Weyl duality: GL(V) image equals centralizer of S_k image
glAction_range_eq_centralizer_symAction

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#10
Schur-Weyl duality: S_k image equals centralizer of GL(V) image
symAction_range_eq_centralizer_glAction

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#11
Existence of a non-isotopic pair of oriented two-component links
exists_nonisotopic_link

Verso theorem preview

theorem declaration uses `sorry`exists_nonisotopic_link : ∃ L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := ⊢ ∃ L₁ L₂, ¬L₁.Isotopic L₂ All goals completed! 🐙
#12
Linear ODE with negative-real-part eigenvalues is asymptotically stable
linear_ode_asymptotic_stability

Verso theorem preview

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

Verso theorem preview

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 := P:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1 All goals completed! 🐙
#14
Gaussian heat kernel solves the 1D heat equation
heat_kernel_solves_heat_equation

Verso theorem preview

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

Verso theorem preview

theorem declaration uses `sorry`rouche_zero_count_eq {f g : ℂ → ℂ} {R : ℝ} (hR : 0 < R) (hf : MeromorphicNFOn f Set.univ) (hg : AnalyticOn ℂ g Set.univ) (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) : (∑ᶠ z, ((divisor (f + g) (Metric.closedBall 0 R))⁺) z) = (∑ᶠ z, ((divisor f (Metric.closedBall 0 R))⁺) z) := f:ℂ → ℂg:ℂ → ℂR:ℝhR:0 < Rhf:MeromorphicNFOn f Set.univhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ ∑ᶠ (z : ℂ), (divisor (f + g) (Metric.closedBall 0 R))⁺ z = ∑ᶠ (z : ℂ), (divisor f (Metric.closedBall 0 R))⁺ z All goals completed! 🐙
#16
Perron-Frobenius for irreducible nonnegative matrices
irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

Verso theorem preview

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

Verso theorem preview

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))) ] := H: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 All goals completed! 🐙
#18
Real cyclotomic integer with house at most 2
cyclotomic_integer_house_le_two

Verso theorem preview

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) := K: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) All goals completed! 🐙
#19
How produced

Corrected model label for the comparator-accepted private submission of cyclotomic_integer_house_le_two. Same verified pinned commit as issue #234; the previous submission used the wrong model label.

Minkowski-Caratheodory theorem
mem_convexHull_finset_extremePoints_of_mem_compact_convex

Verso theorem preview

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) := E: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 All goals completed! 🐙
#20
Oppenheim's inequality for Hadamard products
oppenheim_inequality

Verso theorem preview

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 := n: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 All goals completed! 🐙
#21
Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2
dirichlet_eigenvalues_eq_nat_sq

Verso theorem preview

theorem declaration uses `sorry`dirichlet_eigenvalues_eq_nat_sq (lam : ℝ) : (∃ (y : ℝ → ℝ) (J : Set ℝ), IsOpen J ∧ Set.Icc (0 : ℝ) Real.pi ⊆ J ∧ (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧ (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y Real.pi = 0 ∧ ∃ x ∈ Set.Ioo (0 : ℝ) Real.pi, y x ≠ 0) ↔ ∃ n : ℕ, 0 < n ∧ lam = (n : ℝ) ^ 2 := lam:ℝ⊢ (∃ y J, IsOpen J ∧ Set.Icc 0 π ⊆ J ∧ (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧ (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y π = 0 ∧ ∃ x ∈ Set.Ioo 0 π, y x ≠ 0) ↔ ∃ n, 0 < n ∧ lam = ↑n ^ 2 All goals completed! 🐙
#22
Entrywise exponential of a PSD matrix is PSD
posSemidef_map_exp

Verso theorem preview

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 := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef All goals completed! 🐙
#23
Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan

Verso theorem preview

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) : haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2)) n:ℕ⊢ Invertible 1; All goals completed! 🐙 coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1) All goals completed! 🐙
#24
Character values of finite groups lie in cyclotomic fields
brauer_character_in_cyclotomic

Verso theorem preview

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

Verso theorem preview

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

Verso theorem preview

theorem declaration uses `sorry`cubic_decay_asymptotic (y : ℝ → ℝ) (hy_diff : ∀ t : ℝ, 0 < t → HasDerivAt y (-(y t) ^ 3) t) (hy_cont : ContinuousWithinAt y (Set.Ici 0) 0) (hy0 : y 0 = 1) : Tendsto (fun t : ℝ => y t * Real.sqrt t) atTop (𝓝 (1 / Real.sqrt 2)) := y:ℝ → ℝhy_diff:∀ (t : ℝ), 0 < t → HasDerivAt y (-y t ^ 3) thy_cont:ContinuousWithinAt y (Set.Ici 0) 0hy0:y 0 = 1⊢ Tendsto (fun t => y t * √t) atTop (𝓝 (1 / √2)) All goals completed! 🐙
#27
Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top

Verso theorem preview

theorem declaration uses `sorry`mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] (S : Set G) : (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := G:Type u_1inst✝:Group GS:Set G⊢ (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ All goals completed! 🐙
#28
pi_1 of the circle is Z
pi1_circle_mulEquiv_int

Verso theorem preview

theorem declaration uses `sorry`pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ) All goals completed! 🐙
#31
Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#32
Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Test problems: variable_binder_example, def_hole_example, instance_hole_example, list_append_singleton_length, ci_regenerate_main_check, two_plus_two (6 / 7 solved)

Submission history

First submissionMay 8, 2026
Last submissionMay 26, 2026

Contributors

rishistyping36
5Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus)21 solved

Other solved problems

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

Verso theorem preview

theorem declaration uses `sorry`exists_nonisotopic_link : ∃ L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := ⊢ ∃ L₁ L₂, ¬L₁.Isotopic L₂ All goals completed! 🐙
#1proof
Linear ODE with negative-real-part eigenvalues is asymptotically stable
linear_ode_asymptotic_stability

Verso theorem preview

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

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Bing's house with two rooms is contractible
contractibleSpace_houseWithTwoRooms

Verso theorem preview

theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := ⊢ ContractibleSpace ↑HouseWithTwoRooms All goals completed! 🐙
#3proof
How produced

POC of how a moderately advanced harness / scaffolding can deliver: antigravity, SKILLS.md / AGENTS.md , MCP server. The human in the loop is not a mathematician, nor a software engineer, just someone curious and armed with patience, and acting as a babysitter: with simple encouragements like "remember, if we dont have the needed bricks, we build them and lay them search online for guidance if needed step by step, brick by brick, we are progressing we have time, you are doing great, try to address 1 thing at a time think using sequential thinking tool as needed, take your time and proceed with care no shortcuts, no cheating, we have time the sky is the limit, this is not an open problem, you got this ! " AI did all the thinking. No golfing done. This 7,000+ line proof was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE (a VS Code fork). Due to the massive scale of the deformation retraction, the solution was driven by cycling through the entire suite of available frontier models as quota constraints required. The formal verification relied on a specialized scaffolding pipeline: Iterative Prompt Engineering: The task was initialized using structured prompts ([contractibleSpace_houseWithTwoRooms.md](https://github.com/user-attachments/files/27707778/contractibleSpace_houseWithTwoRooms.md) that enforce Mathlib style guides (e.g., "Rely on existing Mathlib structural lemmas" and "Abstract into lemmas parameterized by characteristics"). Failure Feedback Loop: When intermediate attempts failed (e.g., due to type class synthesis errors or unsolved goals), the raw lake build trace logs and compiler outputs were automatically captured and injected back into the prompt context. This allowed the models to iteratively diagnose and correct their own errors. Model Context Protocol (MCP): The agents interacted with the Lean 4 compiler in real-time via the lean-lsp MCP server, gaining high-fidelity "Language Server to Agent" access: Proof State Tracking (lean_goal): Real-time extraction of tactic states to track the 24 nested sub-cubes of the retraction. Diagnostics (lean_diagnostic_messages): Immediate compiler feedback on type mismatches and syntax errors to keep the massive 7,000-line construction mathematically sound. Structural Synthesis: The proof was built constructively by the ensemble over multiple sessions. The agents defined the 24 topological spaces (C_1 through C_24), constructed explicit piecewise continuous projections (proj_1 through proj_24), and systematically eliminated sorry placeholders until the full deformation retraction onto the point was rigorously verified by the Lean compiler.

Rouche theorem via zero counting
rouche_zero_count_eq

Verso theorem preview

theorem declaration uses `sorry`rouche_zero_count_eq {f g : ℂ → ℂ} {R : ℝ} (hR : 0 < R) (hf : MeromorphicNFOn f Set.univ) (hg : AnalyticOn ℂ g Set.univ) (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) : (∑ᶠ z, ((divisor (f + g) (Metric.closedBall 0 R))⁺) z) = (∑ᶠ z, ((divisor f (Metric.closedBall 0 R))⁺) z) := f:ℂ → ℂg:ℂ → ℂR:ℝhR:0 < Rhf:MeromorphicNFOn f Set.univhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ ∑ᶠ (z : ℂ), (divisor (f + g) (Metric.closedBall 0 R))⁺ z = ∑ᶠ (z : ℂ), (divisor f (Metric.closedBall 0 R))⁺ z All goals completed! 🐙
#4proof
Real cyclotomic integer with house at most 2
cyclotomic_integer_house_le_two

Verso theorem preview

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) := K: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) All goals completed! 🐙
#5proof
von Neumann double commutant theorem
vonNeumann_doubleCommutant_tfae

Verso theorem preview

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))) ] := H: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 All goals completed! 🐙
#6proof
Complementary polynomial on the unit circle
exists_complementary_polynomial_on_unit_circle

Verso theorem preview

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 := P:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1 All goals completed! 🐙
#7proof
Perron-Frobenius for irreducible nonnegative matrices
irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

Verso theorem preview

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

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Gaussian heat kernel solves the 1D heat equation
heat_kernel_solves_heat_equation

Verso theorem preview

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

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Oppenheim's inequality for Hadamard products
oppenheim_inequality

Verso theorem preview

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 := n: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 All goals completed! 🐙
#10proof
Minkowski-Caratheodory theorem
mem_convexHull_finset_extremePoints_of_mem_compact_convex

Verso theorem preview

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) := E: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 All goals completed! 🐙
#11proof
How produced

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

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

Verso theorem preview

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

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Entrywise exponential of a PSD matrix is PSD
posSemidef_map_exp

Verso theorem preview

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 := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef All goals completed! 🐙
#13proof
How produced

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan

Verso theorem preview

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) : haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2)) n:ℕ⊢ Invertible 1; All goals completed! 🐙 coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1) All goals completed! 🐙
#14proof
How produced

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Character values of finite groups lie in cyclotomic fields
brauer_character_in_cyclotomic

Verso theorem preview

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

Antigravity orchestrated the solving using [Jules](https://jules.google.com/) and guided the agent during the task. Direct Spectral Decomposition Approach Strategy: Instead of moving to the global virtual character ring, we perform a local eigenvalue decomposition at the element level. 1. We state that the trace of the linear operator $\rho(g)$ is the sum of its eigenvalues (roots of the characteristic polynomial) using the Mathlib lemma: Module.End.trace_eq_sum_roots_charpoly_of_splits 2. Because $g^{\exp(G)} = 1$ in the group, we have $\rho(g)^{\exp(G)} = 1$. 3. By the Spectral Mapping Theorem (spectrum.pow_mem_pow), if $x$ is an eigenvalue of $\rho(g)$, then $x^{\exp(G)}$ must be an eigenvalue of the identity operator, forcing $x^{\exp(G)} = 1$. 4. Thus, every individual eigenvalue is an $\exp(G)$-th root of unity. 5. The range of our cyclotomic embedding $\varphi$ contains the image of the primitive root $\zeta_{\exp(G)}$, which algebraically generates all $\exp(G)$-th roots of unity in $\mathbb{C}$. Hence, each individual eigenvalue lies in $\varphi\text{.range}$. 6. Since $\varphi\text{.range}$ is a subring (subsemiring in Mathlib), it is closed under addition, and the trace (the sum of the eigenvalues) automatically lies in $\varphi\text{.range}$.

Polynomial decay rate of y' = -y^3
cubic_decay_asymptotic

Verso theorem preview

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

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top

Verso theorem preview

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

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

pi_1 of the circle is Z
pi1_circle_mulEquiv_int

Verso theorem preview

theorem declaration uses `sorry`pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ) All goals completed! 🐙
#18proof
How produced

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Sturm separation theorem
sturm_separation

Verso theorem preview

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

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#22proof
How produced

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

This solution was produced interactively via an AI-driven pair-programming workflow using Antigravity, Google's agentic IDE. The proof was built structurally by cycling through the available ensemble of frontier models over multiple sessions. The formal verification relied on a specialized scaffolding pipeline: (1) Iterative prompt engineering utilizing Mathlib style constraints. (2) A failure feedback loop that injected raw compiler diagnostics back into the prompt context to diagnose errors. (3) Real-time Model Context Protocol (MCP) integration with the lean-lsp server, providing high-fidelity "Language Server to Agent" access to lean_goal (tactic state tracking) and lean_diagnostic_messages (immediate compiler feedback).

Test problems: def_hole_example, instance_hole_example, ci_regenerate_main_check, list_append_singleton_length, two_plus_two (5 / 7 solved)

Submission history

First submissionMay 13, 2026
Last submissionMay 22, 2026

Contributors

daouid26
6Claude Opus 4.7 (1M context)17 solved

Other solved problems

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

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#1
How produced

Claude Opus 4.7 (1M context) with human (Jeroen Zuiddam) direction.

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

Verso theorem preview

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)) := R: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)) All goals completed! 🐙
#2
How produced

Claude Opus 4.7 (1M context) with human (Jeroen Zuiddam) direction.

Complementary polynomial on the unit circle
exists_complementary_polynomial_on_unit_circle

Verso theorem preview

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 := P:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1 All goals completed! 🐙
#3proof
Gaussian heat kernel solves the 1D heat equation
heat_kernel_solves_heat_equation

Verso theorem preview

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

Verso theorem preview

theorem declaration uses `sorry`rouche_zero_count_eq {f g : ℂ → ℂ} {R : ℝ} (hR : 0 < R) (hf : MeromorphicNFOn f Set.univ) (hg : AnalyticOn ℂ g Set.univ) (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) : (∑ᶠ z, ((divisor (f + g) (Metric.closedBall 0 R))⁺) z) = (∑ᶠ z, ((divisor f (Metric.closedBall 0 R))⁺) z) := f:ℂ → ℂg:ℂ → ℂR:ℝhR:0 < Rhf:MeromorphicNFOn f Set.univhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ ∑ᶠ (z : ℂ), (divisor (f + g) (Metric.closedBall 0 R))⁺ z = ∑ᶠ (z : ℂ), (divisor f (Metric.closedBall 0 R))⁺ z All goals completed! 🐙
#5proof
Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2
dirichlet_eigenvalues_eq_nat_sq

Verso theorem preview

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

Verso theorem preview

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) := E: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 All goals completed! 🐙
#7proof
Oppenheim's inequality for Hadamard products
oppenheim_inequality

Verso theorem preview

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 := n: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 All goals completed! 🐙
#8proof
Entrywise exponential of a PSD matrix is PSD
posSemidef_map_exp

Verso theorem preview

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 := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef All goals completed! 🐙
#9proof
Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan

Verso theorem preview

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) : haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2)) n:ℕ⊢ Invertible 1; All goals completed! 🐙 coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1) All goals completed! 🐙
#10proof
How produced

Just asking to solve the problems in Claude Code.

Sturm separation theorem
sturm_separation

Verso theorem preview

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

Verso theorem preview

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

Verso theorem preview

theorem declaration uses `sorry`pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ) All goals completed! 🐙
#13proof
Polynomial decay rate of y' = -y^3
cubic_decay_asymptotic

Verso theorem preview

theorem declaration uses `sorry`cubic_decay_asymptotic (y : ℝ → ℝ) (hy_diff : ∀ t : ℝ, 0 < t → HasDerivAt y (-(y t) ^ 3) t) (hy_cont : ContinuousWithinAt y (Set.Ici 0) 0) (hy0 : y 0 = 1) : Tendsto (fun t : ℝ => y t * Real.sqrt t) atTop (𝓝 (1 / Real.sqrt 2)) := y:ℝ → ℝhy_diff:∀ (t : ℝ), 0 < t → HasDerivAt y (-y t ^ 3) thy_cont:ContinuousWithinAt y (Set.Ici 0) 0hy0:y 0 = 1⊢ Tendsto (fun t => y t * √t) atTop (𝓝 (1 / √2)) All goals completed! 🐙
#14proof
Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top

Verso theorem preview

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

Just asking to solve the problems in Claude Code.

Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#18proof
How produced

Just asking to solve the problems in Claude Code.

Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Test problems: def_hole_example, instance_hole_example, ci_regenerate_main_check, list_append_singleton_length, two_plus_two (5 / 7 solved)

Submission history

First submissionMay 2, 2026
Last submissionMay 24, 2026

Contributors

rkirov20jzuiddam2
7GPT-5.513 solved

Other solved problems

Perron-Frobenius for irreducible nonnegative matrices
irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

Verso theorem preview

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

Verso theorem preview

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 := n: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 All goals completed! 🐙
#2proof
How produced

Autonomous lmp

Minkowski-Caratheodory theorem
mem_convexHull_finset_extremePoints_of_mem_compact_convex

Verso theorem preview

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) := E: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 All goals completed! 🐙
#3proof
Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2
dirichlet_eigenvalues_eq_nat_sq

Verso theorem preview

theorem declaration uses `sorry`dirichlet_eigenvalues_eq_nat_sq (lam : ℝ) : (∃ (y : ℝ → ℝ) (J : Set ℝ), IsOpen J ∧ Set.Icc (0 : ℝ) Real.pi ⊆ J ∧ (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧ (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y Real.pi = 0 ∧ ∃ x ∈ Set.Ioo (0 : ℝ) Real.pi, y x ≠ 0) ↔ ∃ n : ℕ, 0 < n ∧ lam = (n : ℝ) ^ 2 := lam:ℝ⊢ (∃ y J, IsOpen J ∧ Set.Icc 0 π ⊆ J ∧ (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧ (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y π = 0 ∧ ∃ x ∈ Set.Ioo 0 π, y x ≠ 0) ↔ ∃ n, 0 < n ∧ lam = ↑n ^ 2 All goals completed! 🐙
#4proof
Entrywise exponential of a PSD matrix is PSD
posSemidef_map_exp

Verso theorem preview

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 := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef All goals completed! 🐙
#5proof
Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan

Verso theorem preview

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) : haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2)) n:ℕ⊢ Invertible 1; All goals completed! 🐙 coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1) All goals completed! 🐙
#6proof
pi_1 of the circle is Z
pi1_circle_mulEquiv_int

Verso theorem preview

theorem declaration uses `sorry`pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ) All goals completed! 🐙
#7proof
Sturm separation theorem
sturm_separation

Verso theorem preview

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

Verso theorem preview

theorem declaration uses `sorry`brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] : ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ, ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V) (ρ : Representation ℂ G V) (g : G), LinearMap.trace ℂ V (ρ g) ∈ φ.range := G:Typeinst✝¹:Group Ginst✝:Fintype G⊢ ∃ φ, ∀ (V : Type) (x : AddCommGroup V) (x_1 : Module ℂ V), FiniteDimensional ℂ V → ∀ (ρ : Representation ℂ G V) (g : G), (LinearMap.trace ℂ V) (ρ g) ∈ φ.range All goals completed! 🐙
#11proof
Polynomial decay rate of y' = -y^3
cubic_decay_asymptotic

Verso theorem preview

theorem declaration uses `sorry`cubic_decay_asymptotic (y : ℝ → ℝ) (hy_diff : ∀ t : ℝ, 0 < t → HasDerivAt y (-(y t) ^ 3) t) (hy_cont : ContinuousWithinAt y (Set.Ici 0) 0) (hy0 : y 0 = 1) : Tendsto (fun t : ℝ => y t * Real.sqrt t) atTop (𝓝 (1 / Real.sqrt 2)) := y:ℝ → ℝhy_diff:∀ (t : ℝ), 0 < t → HasDerivAt y (-y t ^ 3) thy_cont:ContinuousWithinAt y (Set.Ici 0) 0hy0:y 0 = 1⊢ Tendsto (fun t => y t * √t) atTop (𝓝 (1 / √2)) All goals completed! 🐙
#12proof
Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top

Verso theorem preview

theorem declaration uses `sorry`mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] (S : Set G) : (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := G:Type u_1inst✝:Group GS:Set G⊢ (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ All goals completed! 🐙
#13proof
Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#16proof
Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Test problems: instance_hole_example, def_hole_example, ci_regenerate_main_check, list_append_singleton_length, two_plus_two (5 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionMay 22, 2026

Contributors

sqrt-of-214Morgan-Griffiths7A-M-Berns4kim-em1
8MerLean-Prover5 solved

Other solved problems

Runge's theorem
runge_theorem

Verso theorem preview

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

Verso theorem preview

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))) ] := H: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 All goals completed! 🐙
#2
Character values of finite groups lie in cyclotomic fields
brauer_character_in_cyclotomic

Verso theorem preview

theorem declaration uses `sorry`brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] : ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ, ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V) (ρ : Representation ℂ G V) (g : G), LinearMap.trace ℂ V (ρ g) ∈ φ.range := G:Typeinst✝¹:Group Ginst✝:Fintype G⊢ ∃ φ, ∀ (V : Type) (x : AddCommGroup V) (x_1 : Module ℂ V), FiniteDimensional ℂ V → ∀ (ρ : Representation ℂ G V) (g : G), (LinearMap.trace ℂ V) (ρ g) ∈ φ.range All goals completed! 🐙
#3
Polynomial decay rate of y' = -y^3
cubic_decay_asymptotic

Verso theorem preview

theorem declaration uses `sorry`cubic_decay_asymptotic (y : ℝ → ℝ) (hy_diff : ∀ t : ℝ, 0 < t → HasDerivAt y (-(y t) ^ 3) t) (hy_cont : ContinuousWithinAt y (Set.Ici 0) 0) (hy0 : y 0 = 1) : Tendsto (fun t : ℝ => y t * Real.sqrt t) atTop (𝓝 (1 / Real.sqrt 2)) := y:ℝ → ℝhy_diff:∀ (t : ℝ), 0 < t → HasDerivAt y (-y t ^ 3) thy_cont:ContinuousWithinAt y (Set.Ici 0) 0hy0:y 0 = 1⊢ Tendsto (fun t => y t * √t) atTop (𝓝 (1 / √2)) All goals completed! 🐙
#4
Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Submission history

First submissionMay 31, 2026
Last submissionJun 1, 2026

Contributors

doxtor65
9GPT-5.5 Codex2 solved

Other solved problems

Sturm separation theorem
sturm_separation

Verso theorem preview

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

Verso theorem preview

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

Test problems: two_plus_two (1 / 7 solved)

Submission history

First submissionMay 6, 2026
Last submissionMay 7, 2026

Contributors

A-M-Berns3
10Gemini 3.1 Pro2 solved

Other solved problems

Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top

Verso theorem preview

theorem declaration uses `sorry`mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] (S : Set G) : (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := G:Type u_1inst✝:Group GS:Set G⊢ (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ All goals completed! 🐙
#1proof
Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Test problems: instance_hole_example, def_hole_example, list_append_singleton_length, ci_regenerate_main_check, two_plus_two (5 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionMay 10, 2026

Contributors

sqrt-of-27kim-em1
11[submission] aegis-of-the-unit-circle-logos2 solved

Other solved problems

Real cyclotomic integer with house at most 2
cyclotomic_integer_house_le_two

Verso theorem preview

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) := K: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) All goals completed! 🐙
#1
How produced

Comparator-accepted Lean Eval solution for cyclotomic_integer_house_le_two. Developed and verified in a private repository. Local checks included direct Lean Eval comparator and CI-equivalent evaluate_submission.py.

pi_1 of the circle is Z
pi1_circle_mulEquiv_int

Verso theorem preview

theorem declaration uses `sorry`pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ) All goals completed! 🐙
#2
How produced

Comparator-accepted Lean Eval solution for cyclotomic_integer_house_le_two. Developed and verified in a private repository. Local checks included direct Lean Eval comparator and CI-equivalent evaluate_submission.py.

Test problems: ci_regenerate_main_check, two_plus_two (2 / 7 solved)

Submission history

First submissionMay 12, 2026
Last submissionMay 12, 2026

Contributors

rishistyping4
12EVO2 solved

Other solved problems

Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#1proof
Comparison principle for the Dirichlet BVP
bvp_comparison

Verso theorem preview

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

Test problems: two_plus_two (1 / 7 solved)

Submission history

First submissionMay 18, 2026
Last submissionMay 30, 2026

Contributors

machinelearning20143
13Claude Opus 4.71 solved

Other solved problems

Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem

Verso theorem preview

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙
#1proof

Test problems: list_append_singleton_length, two_plus_two (2 / 7 solved)

Submission history

First submissionApr 30, 2026
Last submissionApr 30, 2026

Contributors

rkirov3kim-em1
14Claude Opus 4.7 + GPT-5.5 (human-in-the-loop)1 solved

Other solved problems

Baer–Suzuki theorem
baer_suzuki

Verso theorem preview

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

Claude Opus 4.7 + GPT-5.5, human-in-the-loop direction and review. Self-contained: inlines a port of Isaacs, Finite Group Theory Ch. 1-2 (p-core / Fitting subgroup / minimal-normal machinery) under Submission/, since Mathlib has no pCore. Builds on Mathlib rev 5450b53e5ddc; proof routes through Aschbacher §31 (normal closure of x is a p-group)

Submission history

First submissionMay 29, 2026
Last submissionMay 29, 2026

Contributors

yawara1
15Kimi K2.60 solved

Test problems: two_plus_two (1 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionMay 1, 2026

Contributors

kim-em1
16Mistral Large 30 solved

Test problems: two_plus_two (1 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionMay 1, 2026

Contributors

kim-em1
17DeepSeek V4 Pro0 solved

Test problems: two_plus_two (1 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionMay 1, 2026

Contributors

kim-em1
18Qwen3.6 Max0 solved

Test problems: two_plus_two (1 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionMay 1, 2026

Contributors

kim-em1
19Grok 4.30 solved

Test problems: two_plus_two (1 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionMay 1, 2026

Contributors

kim-em1
20Claude Sonnet 4.60 solved

Test problems: two_plus_two (1 / 7 solved)

Submission history

First submissionMay 1, 2026
Last submissionMay 1, 2026

Contributors

kim-em1
21Leanstral-26030 solved

Test problems: instance_hole_example, def_hole_example, list_append_singleton_length, ci_regenerate_main_check, two_plus_two (5 / 7 solved)

Submission history

First submissionMay 11, 2026
Last submissionMay 11, 2026

Contributors

sqrt-of-25
Coverage

Per-problem coverage

Which problems each model has solved. Hidden on narrow screens.

ProblemSeed Prover (ByteDance)Aleph Prover(logicalintelligence.com)Aristotle (Harmonic)Stealth ModelAntigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus)Claude Opus 4.7 (1M context)GPT-5.5MerLean-ProverGPT-5.5 CodexGemini 3.1 Pro[submission] aegis-of-the-unit-circle-logosEVOClaude Opus 4.7Claude Opus 4.7 + GPT-5.5 (human-in-the-loop)Kimi K2.6Mistral Large 3DeepSeek V4 ProQwen3.6 MaxGrok 4.3Claude Sonnet 4.6Leanstral-2603
Baer–Suzuki theoremmain✓✓———————————✓———————
Baker-Wüstholz theorem on linear forms in logarithmsmain—————————————————————
Balanceable k-bounded partitionsmain✓✓✓——————————————————
Bézout's theorem (projective, with multiplicity)main—————————————————————
Character values of finite groups lie in cyclotomic fieldsmain✓✓✓✓✓✓✓✓—————————————
Brauer–Fowler theoremmain✓✓✓——————————————————
Brauer–Suzuki theorem (quaternion Sylow 2-subgroup)main—————————————————————
Brouwer fixed-point theoremmain✓✓✓✓—————————————————
Comparison principle for the Dirichlet BVPmain✓✓✓✓✓✓✓✓✓✓—✓—————————
Cauchy–Kovalevskaya theoremmain—————————————————————
Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometrymain—————————————————————
Chudnovsky formula for pi inversemain—————————————————————
Commuting probabilities are closedmain—————————————————————
Bing's house with two rooms is contractiblemain✓✓✓✓✓————————————————
The Conway knot is not smoothly slicemain—————————————————————
The Conway knot is topologically slicemain—————————————————————
Polynomial decay rate of y' = -y^3main✓✓✓✓✓✓✓✓—————————————
Real cyclotomic integer with house in (2, 76/33)main—————————————————————
Real cyclotomic integer with house at most 2main✓✓✓✓✓—————✓——————————
Darboux's theorem (symplectic forms are locally standard)main—————————————————————
De Branges's theorem (Bieberbach conjecture)main—————————————————————
Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2main✓✓✓✓✓✓✓——————————————
Chen theorem for Markoff graphsmain✓✓✓✓—————————————————
Existence of a 779247-dim irreducible e₈-representation with 40 tensor-square isotypic componentsmain—————————————————————
Erdős's unit-distance conjecture is falsemain—————————————————————
Existence of a chiral oriented knotmain—————————————————————
Complementary polynomial on the unit circlemain✓✓✓✓✓✓———————————————
Existence of a non-isotopic pair of oriented knotsmain—————————————————————
Existence of a non-isotopic pair of oriented two-component linksmain✓✓✓✓✓————————————————
Existence of a topologically slice, not smoothly slice knotmain—————————————————————
Fatou–Julia / Cantor dichotomymain—————————————————————
Feit–Thompson odd-order theoremmain—————————————————————
Fermat's Last Theoremmain—————————————————————
Finite Ramsey theorem for graphsmain✓✓✓✓✓✓✓————✓✓————————
Burnside p^a q^b theoremmain✓✓✓✓—————————————————
Possible orders of 5-transitive finite permutation groupsmain—————————————————————
Frobenius's theorem: the Frobenius kernel is normalmain✓✓✓——————————————————
Furstenberg measure-preserving multiple recurrencemain—————————————————————
Furstenberg–Weiss topological multiple recurrence (single-transformation form)main✓✓✓——————————————————
Existence of a 64-dim irreducible g₂-representation with 14 tensor-square isotypic componentsmain—————————————————————
Schur-Weyl duality: GL(V) image equals centralizer of S_k imagemain✓✓✓✓—✓———————————————
Glauberman's Z* theorem for isolated involutionsmain—————————————————————
Gleason's theorem (finite-dimensional)main—————————————————————
Gleason's theorem (separable Hilbert space)main—————————————————————
Gorenstein–Walter theorem (dihedral Sylow 2-subgroup)main—————————————————————
Green–Tao theoremmain—————————————————————
Hadwiger's theoremmain—————————————————————
Gaussian heat kernel solves the 1D heat equationmain✓✓✓✓✓✓———————————————
Hopf–Rinow theoremmain—————————————————————
Perron-Frobenius for irreducible nonnegative matricesmain✓✓✓✓✓—✓——————————————
Isoperimetric inequality (n-dim, topological-frontier form)main—————————————————————
Jacobian of a smooth proper curve (Merten challenge)main—————————————————————
Jacobian of a compact Riemann surface (Buzzard challenge)main—————————————————————
Jordan–Brouwer separation theoremmain—————————————————————
Jordan curve theoremmain—————————————————————
Kakutani fixed-point theoremmain✓✓✓✓—————————————————
Kolmogorov–Arnold superposition theorem (non-universal Lorentz form)main—————————————————————
Koszul formulamain✓✓✓✓—————————————————
Fundamental theorem of Riemannian geometry (Levi-Civita)main—————————————————————
Lidskii's inequalitymain✓✓———————————————————
Lidskii–Last eigenvalue-perturbation theoremmain✓✓———————————————————
Linear ODE with negative-real-part eigenvalues is asymptotically stablemain✓✓✓✓✓————————————————
Liouville–Arnold theorem on integrable systemsmain✓————————————————————
Existence of an order-10200960 group with a 22-dim irrep whose tensor square has 4 isotypic componentsmain—————————————————————
Mandelbar (tricorn) is not path-connected (Hubbard–Schleicher)main—————————————————————
Mandelbrot set is connected (Douady–Hubbard)main—————————————————————
Minkowski-Caratheodory theoremmain✓✓✓✓✓✓✓——————————————
Mergelyan's theoremmain—————————————————————
Milnor's exotic 7-spheremain—————————————————————
Morley's categoricity theoremmain—————————————————————
Morse inequalitiesmain—————————————————————
Cayley graph connected iff generators generate the groupmain✓✓✓✓✓✓✓——✓———————————
Nash equilibrium existence theoremmain✓✓✓——————————————————
Neukirch–Uchida theoremmain—————————————————————
Oppenheim's inequality for Hadamard productsmain✓✓✓✓✓✓✓——————————————
Ornstein–Weiss ℤᵈ Rokhlin lemmamain—————————————————————
Independence of the parallel postulatemain✓✓✓——————————————————
A competition programming problem about permuting a permutation to be unimodalmain✓✓✓✓—————————————————
pi_1 of the circle is Zmain✓✓✓✓✓✓✓———✓——————————
pi_3 of the 2-sphere is Zmain—————————————————————
pi_(n+1) of S^n is Z/2 for n at least 3main—————————————————————
pi_n of the n-sphere is Zmain—————————————————————
Platonic classificationmain—————————————————————
3D smooth Poincaré conjecture (Perelman)main—————————————————————
3D topological Poincaré conjecture (Perelman)main—————————————————————
4D topological Poincaré conjecture (Freedman)main—————————————————————
Poincaré–Bendixson theoremmain—————————————————————
Generalized topological Poincaré conjecture in dimensions ≥ 5 (Smale)main—————————————————————
Poincaré–Siegel linearisation theoremmain—————————————————————
Entrywise exponential of a PSD matrix is PSDmain✓✓✓✓✓✓✓——————————————
Radó's theorem on Riemann surfacesmain—————————————————————
Lagarias criterion is equivalent to RHmain—————————————————————
Rokhlin lemmamain✓————————————————————
Rouche theorem via zero countingmain✓✓✓✓✓✓———————————————
Runge's theoremmain✓✓—————✓—————————————
Schauder fixed-point theoremmain✓✓✓✓—————————————————
Schläfli classification of regular polytopesmain—————————————————————
Schoenflies theoremmain—————————————————————
Schreier's conjecture: outer automorphism group of a finite simple group is solvablemain—————————————————————
Smale conjecture (Hatcher) in relative parameterized formmain—————————————————————
Solvable extensions ↔ solvable groups (the missing converse in Abel–Ruffini)main✓✓———————————————————
Sturm's theoremmain✓✓✓——————————————————
Sturm separation theoremmain✓✓✓✓✓✓✓—✓————————————
Catalan generating function via compositional inversionmain✓✓✓✓✓✓✓——————————————
Schur-Weyl duality: S_k image equals centralizer of GL(V) imagemain✓✓✓✓—✓———————————————
Symplectic matrices have determinant 1main✓✓✓——————————————————
Szemerédi's theoremmain—————————————————————
Topological classification of surfacesmain—————————————————————
Uniformization theorem for Riemann surfacesmain—————————————————————
Spencer-Szemerédi-Trotter unit-distance upper boundmain—————————————————————
von Neumann double commutant theoremmain✓✓✓✓✓——✓—————————————
Weak Morse inequalitiesmain—————————————————————
CI regenerate-main checktest—✓✓✓✓✓✓——✓✓—————————✓
def-hole minimal exampletest—✓✓✓✓✓✓——✓——————————✓
instance-hole minimal exampletest—✓✓✓✓✓✓——✓——————————✓
Appending a singleton increases the list lengthtest—✓✓✓✓✓✓——✓——✓———————✓
multi-hole-with-helpers regression exampletest—————————————————————
2 + 2 = 4test—✓✓✓✓✓✓—✓✓✓✓✓—✓✓✓✓✓✓✓
variable-binder minimal exampletest——✓✓—————————————————

Welcome to lean-eval, a Lean formalization benchmark and public leaderboard.

You can submit new problems for review, and solutions for existing problems. New problems will be carefully reviewed and added to future benchmark releases if they are accepted. Solutions are automatically verified using comparator and added to the public leaderboard.

This benchmark intends to capture hard Lean formalization problems, consisting of mathematical problems that are currently stateable mostly using existing Mathlib definitions, perhaps with a page or so of additional setup. They should be hard, but usually not open problems: in fact, it's preferred if the problem has a known informal solution which is publicly available.

Our hope is that at launch, the problem set will be mostly, but not entirely, out of reach for current publicly available frontier models, or simple orchestration layers built on top of these. So some genuine mathematical subtlety is required!

It's also important to say what this benchmark is not: we are not trying to capture the ability to write readable or reusable code, or to follow best practices in Lean. In particular, the only requirement for a solution to be accepted is that it is correct and passes the comparator tests.

I'd like to acknowledge the use of Aristotle, Claude Code, and Codex in the preparation of many of the problems here. In particular I should point out that Aristotle has a handicap on the leaderboard: typically, if a single query to Aristotle could resolve a problem, I would deem it too easy and drop it from consideration for the eval set. I think it's a testament to the public service that Aristotle provides that this is both possible, and useful!