Explore datasets
Every pair the leaderboard is computed from: a query, the Mathlib declaration it is supposed to find, and where each system actually ranked that declaration. The six phrasings of each target sit side by side — Lean-ish notation through to the nickname a mathematician would say out loud — because that is the axis on which lexical and dense retrieval fail in opposite directions.
200 of 200 declarations
Phrasing
DifficultyOrder
Scope
MathlibQR against mathlib-4280 at c5f07cc71d42, rendered by lsv2-compat (5f1e87b6661e). 11 of 200 gold declarations do not exist in this corpus revision — those pairs are unscoreable and are excluded from every metric rather than counted as misses by all systems. Each phrasing carries one rank column per system — 14 of them, so the table scrolls sideways when they do not all fit.
Basis of a module over a semiring — A basis of a module $ M $ over a semiring $ R $, consisting of a linearly independent spanning set.
Type u_1 → (R : Type u_3) → (M : Type u_6) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max (max u_1 u_3) u_6)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `M ≃ₗ[R] (ι →₀ R)` miss miss miss miss miss miss miss miss miss miss miss miss miss #63 LaTeX $M \cong_R \bigoplus_\iota R$ via a chosen isomorphism miss miss miss miss miss miss miss miss miss miss miss miss miss miss Natural language a linear isomorphism between the module and a free module on an index set miss miss miss miss miss miss miss miss miss miss miss #187 miss #4 Slogan a linear iso with a free module on an index set miss miss miss miss miss miss miss miss miss miss miss miss miss #6 Nickname basis of a module miss #2 #32 #63 #3 #49 #3 #5 #2 #1 #1 #2 miss #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Basis of a module over a semiring: A basis of a module $ M $ over a semiring $ R $, consisting of a linearly independent spanning set. Formal content: Module.Basis Type u_1 → (R : Type u_3) → (M : Type u_6) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max (max u_1 u_3) u_6) := by sorryWord in the indexed coproduct of monoids — The type of words formed by elements from a family of monoids indexed by $\iota$, used in the construction of their coproduct.
{ι : Type u_1} → (M : ι → Type u_2) → [(i : ι) → Monoid (M i)] → Type (max u_1 u_2)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `toList : List ((i : ι) × M i)` with `ne_one` and `chain_ne` (no 1's, adjacent letters from different summands) miss miss miss miss miss miss #91 miss miss miss #42 #31 #182 #4 LaTeX list of nontrivial elements from indexed monoids with consecutive ones from different factors miss miss miss #184 #22 miss #28 miss miss miss #78 #96 #117 #1 Natural language a list of nontrivial elements where consecutive entries come from different summands miss miss miss miss miss miss miss miss miss miss miss miss miss #1 Slogan reduced word in a free product miss miss miss miss miss miss miss miss miss #15 #139 #194 #3 #1 Nickname reduced word miss miss miss miss miss miss #180 miss miss #74 miss miss #16 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Word in the indexed coproduct of monoids: The type of words formed by elements from a family of monoids indexed by $\iota$, used in the construction of their coproduct. Formal content: Monoid.CoprodI.Word {ι : Type u_1} → (M : ι → Type u_2) → [(i : ι) → Monoid (M i)] → Type (max u_1 u_2) := by sorryType of 2-cells in a bicategory — For objects $A$ and $B$ in a bicategory, the type of 2-cells between 1-cells $A o B$.
Type u → Type (max (max u (v + 1)) (w + 1))Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish a `CategoryStruct` with `whiskerLeft`, `whiskerRight`, `associator`, `leftUnitor`, `rightUnitor` satisfying pentagon and triangle miss miss miss miss miss miss miss miss miss #47 miss miss #24 #4 LaTeX category enriched in categories with weak associator/unitor satisfying pentagon and triangle laws miss miss miss miss miss miss miss miss miss miss miss miss #122 miss Natural language a category whose composition is associative only up to coherent 2-isomorphism miss miss miss miss miss miss miss miss miss miss miss miss #1 #1 Slogan weak 2-category with coherent associator and unitors miss miss miss miss miss miss miss miss miss #9 miss miss #6 #1 Nickname bicategory miss #32 #26 miss #15 miss #21 miss miss #68 #67 #96 #2 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Type of 2-cells in a bicategory: For objects $A$ and $B$ in a bicategory, the type of 2-cells between 1-cells $A o B$. Formal content: CategoryTheory.Bicategory Type u → Type (max (max u (v + 1)) (w + 1)) := by sorry
Equivalence between α and β — The type of equivalences (bijections) between two types α and β.
Sort u_1 → Sort u_2 → Sort (max (max 1 u_1) u_2)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `α ≃ β` with `toFun, invFun, left_inv, right_inv` miss miss miss miss miss miss #107 miss miss #5 #34 #78 #1 #2 LaTeX $\alpha \cong \beta$ with two-sided inverse miss miss miss miss miss miss #77 miss miss #7 #8 #109 #1 #3 Natural language a function with a two-sided inverse miss miss miss miss miss miss miss miss miss #2 miss miss #128 #4 Slogan bijection bundled with its inverse miss miss miss miss miss miss miss miss miss miss #154 miss #2 #2 Nickname isomorphism miss miss miss miss miss miss miss miss miss miss miss miss #168 #10 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Equivalence between α and β: The type of equivalences (bijections) between two types α and β. Formal content: Equiv Sort u_1 → Sort u_2 → Sort (max (max 1 u_1) u_2) := by sorry
Homology data for a short complex in a category with zero morphisms — A type representing the data required to define homology for a short complex in a category equipped with zero morphisms, typically involving the kernel and image of the differentials in the complex.
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Type (max u v)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish a `LeftHomologyData` and `RightHomologyData` with an iso between their `H` and a compatibility square miss miss miss miss miss miss miss miss miss #24 miss miss #171 #3 LaTeX $H_{\mathrm{left}} \xrightarrow{\sim} H_{\mathrm{right}}$ on a short complex with compatible square miss miss miss miss miss miss miss miss miss #18 miss miss miss miss Natural language a left and right homology data of a short complex together with an iso between them miss miss miss miss #114 miss miss miss miss #1 #75 #182 #83 #8 Slogan paired left/right homology data of a short complex miss #56 miss miss #28 #71 #140 miss miss #3 #8 #12 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Homology data for a short complex in a category with zero morphisms: A type representing the data required to define homology for a short complex in a category equipped with zero morphisms, typically involving the kernel and image of the differentials in the complex. Formal content: CategoryTheory.ShortComplex.HomologyData {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Type (max u v) := by sorryNormal function between linearly ordered sets — A property of functions between linearly ordered sets $\alpha$ and $\beta$, asserting that the function satisfies the conditions defined by the inductive type `IsNormal`.
{α : Type u_1} → {β : Type u_2} → [LinearOrder α] → [LinearOrder β] → (α → β) → PropPhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish strictly monotone `f` on well-orders, with `f a = sup (f '' Iio a)` at successor-limits miss miss miss miss miss miss miss miss miss miss miss miss #189 #2 LaTeX $f$ strictly increasing with $f(a) = \sup_{b<a} f(b)$ at each successor-limit $a$ miss miss miss miss miss miss miss miss miss miss miss miss miss #7 Natural language a strictly increasing function between well-orders that is continuous at every limit miss miss miss miss miss miss miss miss miss #4 miss miss #2 #1 Slogan strictly increasing and limit-preserving on well-orders miss miss miss miss miss miss miss miss miss miss miss miss #39 #2 Nickname normal function miss #27 #60 #109 #2 #44 #3 #46 #3 #4 #2 #2 #1 #4 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Normal function between linearly ordered sets: A property of functions between linearly ordered sets $\alpha$ and $\beta$, asserting that the function satisfies the conditions defined by the inductive type `IsNormal`. Formal content: Order.IsNormal {α : Type u_1} → {β : Type u_2} → [LinearOrder α] → [LinearOrder β] → (α → β) → Prop := by sorryFormally étale algebra — A property of an algebra $ A $ over a commutative ring $ R $, asserting that $ A $ is formally étale, meaning it satisfies the infinitesimal lifting property characterizing étale morphisms in algebraic geometry.
(R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → PropPhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `Subsingleton Ω[A⁄R]` and `Subsingleton (H1Cotangent R A)` miss miss miss miss miss miss miss miss miss miss miss miss miss #15 LaTeX $\Omega^1_{A/R} = 0$ and $H^1(L_{A/R}) = 0$ miss miss miss miss miss miss miss miss miss #3 miss miss miss #3 Natural language an R-algebra with vanishing Kähler differentials and first cotangent cohomology miss miss miss miss miss miss miss miss miss #9 miss miss miss #2 Slogan vanishing differentials and obstructions miss miss miss miss miss miss miss miss miss miss miss miss miss #1 Nickname formally étale #30 #37 #1 #2 #1 #22 #1 #51 #3 #2 #2 #6 #2 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Formally étale algebra: A property of an algebra $ A $ over a commutative ring $ R $, asserting that $ A $ is formally étale, meaning it satisfies the infinitesimal lifting property characterizing étale morphisms in algebraic geometry. Formal content: Algebra.FormallyEtale (R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop := by sorry
Ring of dimension at most one — The commutative ring $ R $ has Krull dimension at most one, meaning every prime ideal is either maximal or there are no chains of prime ideals of length greater than one.
(R : Type u_1) → [CommRing R] → PropPhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `∀ p : Ideal R, p ≠ ⊥ → p.IsPrime → p.IsMaximal` miss miss miss miss miss miss miss miss miss miss miss miss miss #12 LaTeX $\forall \mathfrak{p}$ prime, $\mathfrak{p} \ne 0 \Rightarrow \mathfrak{p}$ maximal miss miss miss miss miss miss #100 miss miss miss miss miss #187 #12 Natural language a ring whose every nonzero prime ideal is maximal #66 miss miss miss #78 miss #20 miss miss miss #86 #170 #23 #1 Slogan nonzero primes are maximal #155 miss miss miss miss miss miss miss miss miss miss miss miss #92 Nickname Krull dimension ≤ 1 #181 #46 #81 #79 #14 #6 #1 #9 #1 #26 #2 #2 #7 #54 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Ring of dimension at most one: The commutative ring $ R $ has Krull dimension at most one, meaning every prime ideal is either maximal or there are no chains of prime ideals of length greater than one. Formal content: Ring.DimensionLEOne (R : Type u_1) → [CommRing R] → Prop := by sorry
Matroid — The type of matroids on a ground set $ \alpha $.
Type u_1 → Type u_1Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish ground set `E`, base predicate `IsBase`, indep predicate `Indep` satisfying exchange and maximality miss miss miss miss miss miss miss miss miss #13 miss miss #23 #2 LaTeX a ground set $E$ with families $\mathcal{B}, \mathcal{I}$ of bases and independents satisfying exchange and maximality miss miss miss miss miss miss miss miss miss #1 miss miss #1 #2 Natural language a ground set with families of bases and independent sets satisfying exchange and maximality miss miss miss miss miss miss miss miss miss #7 miss miss #2 #2 Slogan combinatorial abstraction of linear independence miss miss miss miss miss miss miss miss miss miss miss miss miss miss Nickname matroid miss #21 miss #28 #16 #136 #1 #1 #1 #1 #1 #1 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Matroid: The type of matroids on a ground set $ \alpha $. Formal content: Matroid Type u_1 → Type u_1 := by sorry
Coalgebra over a commutative semiring — A coalgebra over a commutative semiring $ R $ is an additive commutative monoid $ A $ equipped with an $ R $-module structure, forming a type in the maximum universe of $ R $ and $ A $.
(R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Type (max u v)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `extends CoalgebraStruct` with `coassoc`, `rTensor_counit_comp_comul`, `lTensor_counit_comp_comul` miss miss miss miss #98 miss #137 miss miss #74 miss miss #1 #33 LaTeX comultiplication $\Delta : A \to A \otimes A$ + counit $\varepsilon : A \to R$ with coassociativity and counitality miss miss miss miss miss miss #184 miss miss #4 miss miss #1 #12 Natural language a module equipped with comultiplication and counit dual to the algebra axioms miss miss miss miss miss miss #104 miss miss #65 miss #189 #1 #8 Slogan dual of an algebra: comultiplication + counit miss miss miss miss miss miss miss miss miss #23 miss miss #2 #85 Nickname coalgebra miss #31 #72 miss #33 #158 #3 miss miss #1 #7 #6 #1 #3 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Coalgebra over a commutative semiring: A coalgebra over a commutative semiring $ R $ is an additive commutative monoid $ A $ equipped with an $ R $-module structure, forming a type in the maximum universe of $ R $ and $ A $. Formal content: Coalgebra (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Type (max u v) := by sorry
Nucleus inductive type for a semilattice — An inductive type defined for a type $\alpha$ equipped with a semilattice infimum structure, constructing a new type based on $\alpha$.
(X : Type u_2) → [SemilatticeInf X] → Type u_2Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish an `InfHom` `j` with `x ≤ j x` and `j (j x) ≤ j x` miss miss miss miss miss miss miss miss miss miss #73 #68 #168 #5 LaTeX $j : L \to L$ inflationary, idempotent, $j(x \sqcap y) = j(x) \sqcap j(y)$ miss miss miss miss miss miss miss miss miss miss #161 miss #1 #4 Natural language an inflationary, idempotent self-map that also preserves meets miss miss miss miss miss miss miss miss miss miss miss miss #10 #3 Nickname nucleus #65 #68 #11 #53 #14 #103 #2 #93 miss #1 #40 #33 #3 #2 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Nucleus inductive type for a semilattice: An inductive type defined for a type $\alpha$ equipped with a semilattice infimum structure, constructing a new type based on $\alpha$. Formal content: Nucleus (X : Type u_2) → [SemilatticeInf X] → Type u_2 := by sorry
Ordinal Notation — An inductive data type representing ordinal numbers, used to construct and manipulate ordinal notations in set theory.
: TypePhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `zero | oadd : ONote → ℕ+ → ONote → ONote` #160 miss miss miss miss #97 #108 miss miss #8 #101 miss #13 #27 LaTeX $\omega^e \cdot n + a$ — Cantor normal form below $\varepsilon_0$ miss miss miss miss miss miss miss miss miss miss miss miss #33 #56 Natural language ordinal terms below $\varepsilon_0$ in Cantor normal form miss miss miss miss miss #113 miss miss miss #102 #98 #155 #11 #7 Slogan Cantor normal form notation for ordinals below $\varepsilon_0$ #197 miss miss miss miss #117 #196 miss miss #77 #78 #146 #1 #12 Nickname ordinal notation (Cantor normal form) #142 #52 #180 #87 #90 #69 #92 #108 miss #24 #6 #50 #1 #2 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Ordinal Notation: An inductive data type representing ordinal numbers, used to construct and manipulate ordinal notations in set theory. Formal content: ONote Type := by sorry
Vector measure — A structure parameterized by a measurable space $\alpha$ and a topological additive commutative monoid $M$, representing a function from measurable subsets of $\alpha$ to $M$ equipped with additivity and continuity properties.
(α : Type u_3) → [MeasurableSpace α] → (M : Type u_4) → [AddCommMonoid M] → [TopologicalSpace M] → Type (max u_3 u_4)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `measureOf' : Set α → M`, σ-additive on countable disjoint families miss miss miss miss miss miss miss miss miss #3 #89 #70 #126 #24 LaTeX $\mu\bigl(\bigsqcup_n A_n\bigr) = \sum_n \mu(A_n)$, $\mu : \Sigma \to M$ miss miss miss miss miss miss miss miss miss miss miss miss miss #194 Natural language a σ-additive set function valued in a topological additive monoid miss miss miss miss miss #22 #9 miss miss miss #9 #4 #19 #1 Slogan σ-additive set function in a topological group miss miss miss miss miss miss miss miss miss miss #148 miss #139 #26 Nickname vector measure miss #6 #1 #11 #2 #4 #1 #14 #1 #39 #1 #1 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Vector measure: A structure parameterized by a measurable space $\alpha$ and a topological additive commutative monoid $M$, representing a function from measurable subsets of $\alpha$ to $M$ equipped with additivity and continuity properties. Formal content: MeasureTheory.VectorMeasure (α : Type u_3) → [MeasurableSpace α] → (M : Type u_4) → [AddCommMonoid M] → [TopologicalSpace M] → Type (max u_3 u_4) := by sorry
Affineness of a scheme — A predicate indicating whether a given scheme is affine.
AlgebraicGeometry.Scheme → PropPhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 LaTeX $X \cong \mathrm{Spec}\,\Gamma(X, \mathcal{O}_X)$ miss miss miss miss miss miss miss miss miss miss miss miss #151 #7 Natural language a scheme that is isomorphic to Spec A miss miss miss miss miss miss miss miss miss #8 #139 #58 #26 #3 Slogan a scheme that is the spectrum of its ring of functions miss miss miss miss miss miss miss miss miss miss miss miss #93 #2 Nickname affine scheme #50 #7 #92 #56 #3 #82 #3 #38 #12 #1 #3 #3 #9 #3 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Affineness of a scheme: A predicate indicating whether a given scheme is affine. Formal content: AlgebraicGeometry.IsAffine AlgebraicGeometry.Scheme → Prop := by sorry
Is n-radical homomorphism — Given commutative semirings $ K $ and $ L $, a ring homomorphism $ f : K o L $, and a natural number $ n $, the proposition that $ f $ satisfies the $ n $-radical condition.
{K : Type u_1} → {L : Type u_2} → [inst : CommSemiring K] → [inst_1 : CommSemiring L] → (K →+* L) → ℕ → PropPhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `i : K →+* L` with `∀ x, ∃ n y, i y = x ^ p^n` and `ker i ≤ pNilradical K p` miss miss miss #13 #39 miss #49 miss miss #6 #73 #63 #4 #5 LaTeX ring map $i : K \to L$ such that every $x \in L$ has $x^{p^n} \in i(K)$ and $\ker i \subseteq \mathrm{pNilradical}(K)$ miss miss miss #118 #72 #136 #77 #98 #15 #2 #39 #36 #2 #9 Natural language a ring map where every element of the target has a $p^n$-power in the source miss miss miss miss miss miss miss miss miss #2 #56 #111 #20 #12 Slogan every element of L has a p-power in K miss miss miss miss miss miss miss miss miss #5 #103 #92 miss miss Nickname p-radical (purely inseparable) miss miss miss miss #181 miss #167 miss miss #11 miss miss #3 #33 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Is n-radical homomorphism: Given commutative semirings $ K $ and $ L $, a ring homomorphism $ f : K o L $, and a natural number $ n $, the proposition that $ f $ satisfies the $ n $-radical condition. Formal content: IsPRadical {K : Type u_1} → {L : Type u_2} → [inst : CommSemiring K] → [inst_1 : CommSemiring L] → (K →+* L) → ℕ → Prop := by sorryYoung diagram — The type of Young diagrams, which are combinatorial objects representing integer partitions as arrays of boxes arranged in left-aligned rows with non-increasing row lengths.
TypePhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish a `Finset (ℕ × ℕ)` that is a lower set miss miss miss miss miss miss miss miss miss miss miss miss #31 #1 LaTeX a finite lower set in $\mathbb{N} \times \mathbb{N}$ miss miss miss miss miss miss miss miss miss miss miss miss #58 #2 Natural language a finite collection of cells forming a lower set in the integer grid miss miss miss miss miss miss miss miss miss #1 #138 #89 #5 #1 Slogan finite lower set of cells in the integer grid miss miss miss miss miss miss miss miss miss #2 miss miss #80 #3 Nickname Young diagram #13 #1 #1 #6 #2 #1 #1 #1 #1 #1 #1 #1 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Young diagram: The type of Young diagrams, which are combinatorial objects representing integer partitions as arrays of boxes arranged in left-aligned rows with non-increasing row lengths. Formal content: YoungDiagram Type := by sorry
Scheme — The type of schemes in algebraic geometry.
Type (u_1 + 1)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish a `LocallyRingedSpace` that is locally `Spec R` near every point miss miss miss miss miss miss miss miss miss #2 miss miss #14 #1 LaTeX a locally ringed space $(X, \mathcal{O}_X)$ in which every point has a neighborhood isomorphic to $\mathrm{Spec}\,R$ for some commutative ring $R$ miss miss miss miss miss miss miss miss miss #1 miss miss #13 #1 Natural language a locally ringed space that is locally isomorphic to the spectrum of a commutative ring miss miss miss miss miss miss miss miss miss #4 miss miss #12 #1 Slogan a locally ringed space modeled on Spec of rings miss miss miss miss miss miss miss miss miss #80 miss miss #16 #3 Nickname scheme miss #4 #6 #9 #1 #1 #1 #6 #1 #2 #1 #1 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Scheme: The type of schemes in algebraic geometry. Formal content: AlgebraicGeometry.Scheme Type (u_1 + 1) := by sorry
Perfect ring with exponential characteristic $ p $ — Given a commutative semiring $ R $ with exponential characteristic $ p $, $ R $ is a perfect ring if every element of $ R $ has a $ p $-th root.
(R : Type u_1) → (p : ℕ) → [inst : CommSemiring R] → [ExpChar R p] → PropPhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `Function.Bijective (fun x : R => x ^ p)` miss miss miss miss #135 miss miss miss miss miss #167 #125 miss #6 LaTeX $x \mapsto x^p$ is a bijection on $R$ miss miss miss miss #187 miss #81 miss miss #2 #171 #116 miss #1 Natural language a ring of characteristic p where the Frobenius map is a bijection miss miss miss miss #169 miss #174 miss miss #1 #88 #89 #38 #1 Slogan Frobenius is a bijection miss miss miss miss miss miss miss miss miss #3 miss miss miss #49 Nickname perfect ring #51 #4 #1 #87 #2 #2 #1 #11 #2 #1 #1 #3 #1 #2 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Perfect ring with exponential characteristic $ p $: Given a commutative semiring $ R $ with exponential characteristic $ p $, $ R $ is a perfect ring if every element of $ R $ has a $ p $-th root. Formal content: PerfectRing (R : Type u_1) → (p : ℕ) → [inst : CommSemiring R] → [ExpChar R p] → Prop := by sorry
Natural transformation between functors from C to D — The type of natural transformations between two functors $ F $ and $ G $ from category $ C $ to category $ D $.
{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.Functor C D → Type (max u₁ v₂)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `app (X : C) : F.obj X ⟶ G.obj X` with `naturality (f : X ⟶ Y)` miss miss miss miss #31 miss #166 miss miss #7 miss #182 #14 #3 LaTeX family $\alpha_X : F(X) \to G(X)$ satisfying $\alpha_Y \circ F(f) = G(f) \circ \alpha_X$ miss miss miss miss miss miss miss miss miss miss #161 miss #18 #1 Natural language a family of morphisms between two functors that commutes with morphism action miss miss miss miss miss miss #182 miss miss miss #29 #40 #10 #1 Slogan morphism between functors miss miss miss miss miss miss #181 miss miss miss #7 #4 #17 #1 Nickname natural transformation miss #22 #17 miss #3 #42 #2 #53 #2 #11 #5 #1 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Natural transformation between functors from C to D: The type of natural transformations between two functors $ F $ and $ G $ from category $ C $ to category $ D $. Formal content: CategoryTheory.NatTrans {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.Functor C D → Type (max u₁ v₂) := by sorryRoot pairing between R-modules — Given a commutative ring $ R $, an additive commutative group $ M $ with an $ R $-module structure, and an additive commutative group $ N $ with an $ R $-module structure, this constructs the type of root pairings between $ M $ and $ N $.
Type u_1 → (R : Type u_2) → (M : Type u_3) → (N : Type u_4) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → [inst_3 : AddCommGroup N] → [Module R N] → Type (max (max (max u_1 u_2) u_3) u_4)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `extends M →ₗ[R] N →ₗ[R] R; root, coroot, reflectionPerm` with axioms miss miss miss miss #170 miss miss miss miss #26 #122 #22 #15 #2 LaTeX perfect pairing $M \otimes N \to R$ + indexed roots/coroots + reflection permutations miss #163 miss miss #71 miss #101 miss miss #30 #21 #19 #1 #10 Natural language a perfect pairing on dual modules with families of roots, coroots, and reflection permutations satisfying compatibility miss #168 miss miss #95 miss #146 miss miss #130 miss miss #1 #11 Slogan data for a root system: roots, coroots, perfect pairing, reflections miss miss miss miss miss miss miss miss miss #20 #118 #53 #5 #8 Nickname root pairing miss #69 #67 #82 #11 miss #4 miss miss #25 #3 #1 #3 #4 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Root pairing between R-modules: Given a commutative ring $ R $, an additive commutative group $ M $ with an $ R $-module structure, and an additive commutative group $ N $ with an $ R $-module structure, this constructs the type of root pairings between $ M $ and $ N $. Formal content: RootPairing Type u_1 → (R : Type u_2) → (M : Type u_3) → (N : Type u_4) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → [inst_3 : AddCommGroup N] → [Module R N] → Type (max (max (max u_1 u_2) u_3) u_4) := by sorrySolvable group — A group $ G $ is solvable.
(G : Type u_1) → [Group G] → PropPhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `∃ n : ℕ, derivedSeries G n = ⊥` miss miss miss miss miss #185 #98 miss miss miss #100 #104 #52 #4 LaTeX $\exists n \in \mathbb{N},\ G^{(n)} = \{e\}$ miss miss miss miss miss miss #87 miss miss miss miss miss miss #4 Natural language a group whose derived series eventually reaches the trivial subgroup miss miss miss miss miss #60 #176 #134 #4 #6 #98 #133 #25 #4 Slogan derived series eventually trivial miss miss miss miss miss miss miss miss miss #39 miss miss #92 #74 Nickname solvable group #12 #5 #20 #20 #1 #2 #1 #1 #1 #2 #1 #1 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Solvable group: A group $ G $ is solvable. Formal content: IsSolvable (G : Type u_1) → [Group G] → Prop := by sorry
Functor from category C to category D — The type of functors from category $ C $ to category $ D $, given categories $ C $ and $ D $.
(C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → Type (max v₁ v₂ u₁ u₂)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish a map between categories with `obj : C → D` and `map : (X ⟶ Y) → (F X ⟶ F Y)` preserving `𝟙` and `≫` miss miss miss miss miss miss miss miss miss #1 #113 #197 #1 #1 LaTeX $F : C \to D$ with $F(\mathrm{id}_X) = \mathrm{id}_{F X}$ and $F(g \circ f) = F g \circ F f$ miss miss miss miss miss miss #153 miss miss #1 #23 #28 #1 #2 Natural language a map between categories that preserves identities and composition miss miss miss miss miss miss miss miss miss #2 #89 #108 #1 #1 Slogan a structure-preserving map between categories miss miss miss miss miss miss miss miss miss #1 #21 #30 #3 #1 Nickname functor miss #55 #34 miss #35 miss #1 #120 #5 #15 #3 #4 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Functor from category C to category D: The type of functors from category $ C $ to category $ D $, given categories $ C $ and $ D $. Formal content: CategoryTheory.Functor (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → Type (max v₁ v₂ u₁ u₂) := by sorryMinimal monoid action — A monoid action of $M$ on a topological space $\alpha$ is minimal if the only closed subsets of $\alpha$ invariant under the action are the empty set and $\alpha$ itself.
(M : Type u_1) → (α : Type u_2) → [inst : Monoid M] → [TopologicalSpace α] → [MulAction M α] → PropPhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `∀ x, Dense (orbit M x)` miss miss miss miss miss miss miss miss miss #2 #84 #82 #5 #25 LaTeX $\forall x \in \alpha,\ \overline{Mx} = \alpha$ miss miss miss miss #133 miss #82 miss miss miss #34 #23 miss #7 Natural language a group action all of whose orbits are dense miss miss miss miss miss miss #114 miss miss #33 #106 miss #4 #14 Slogan every orbit is dense miss miss miss miss miss miss miss miss miss #4 miss miss #4 #25 Nickname minimal action #5 #3 #2 #1 #1 #1 #1 #2 #1 #6 #1 #1 #2 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Minimal monoid action: A monoid action of $M$ on a topological space $\alpha$ is minimal if the only closed subsets of $\alpha$ invariant under the action are the empty set and $\alpha$ itself. Formal content: MulAction.IsMinimal (M : Type u_1) → (α : Type u_2) → [inst : Monoid M] → [TopologicalSpace α] → [MulAction M α] → Prop := by sorry
Combinatorial line in Hales-Jewett theorem — A type representing combinatorial lines in the context of the Hales-Jewett theorem, parameterized by two types $A$ and $B$.
Type u_5 → Type u_6 → Type (max u_5 u_6)Phrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore MathLeap-Qwen MathLeap-Octen Lean Finder v1 Lean Finder v2 Lean-ish `idxFun : ι → Option α` with at least one `none` (the free coordinate) miss miss miss miss miss miss miss miss miss miss miss miss #35 #14 LaTeX $\ell : \alpha \to (\iota \to \alpha)$ where some coordinates vary together and others are fixed miss miss miss miss miss miss miss miss miss miss miss miss #11 #1 Natural language a parametric family of points in a hypercube where some coordinates vary together and others are fixed miss miss miss miss miss miss #125 miss miss miss miss miss #3 #3 Slogan non-trivial axis-parallel line in a hypercube #174 #13 miss miss #111 #17 #14 #155 #1 #1 #67 #116 #2 #6 Nickname combinatorial line #12 #4 #12 #21 #2 #1 #2 #2 #1 #1 #2 #7 #1 #1 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Combinatorial line in Hales-Jewett theorem: A type representing combinatorial lines in the context of the Hales-Jewett theorem, parameterized by two types $A$ and $B$. Formal content: Combinatorics.Line Type u_5 → Type u_6 → Type (max u_5 u_6) := by sorry