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 — 10 of them, so the table scrolls sideways when they do not all fit.
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 Lean-ish `α ≃ β` with `toFun, invFun, left_inv, right_inv` miss miss miss miss miss miss #107 miss miss #5 LaTeX $\alpha \cong \beta$ with two-sided inverse miss miss miss miss miss miss #77 miss miss #7 Natural language a function with a two-sided inverse miss miss miss miss miss miss miss miss miss #2 Slogan bijection bundled with its inverse miss miss miss miss miss miss miss miss miss miss Nickname isomorphism miss miss miss miss miss miss miss miss miss miss 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
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.
{ι : 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 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 LaTeX list of nontrivial elements from indexed monoids with consecutive ones from different factors miss miss miss #184 #22 miss #28 miss miss miss Natural language a list of nontrivial elements where consecutive entries come from different summands miss miss miss miss miss miss miss miss miss miss Slogan reduced word in a free product miss miss miss miss miss miss miss miss miss #15 Nickname reduced word miss miss miss miss miss miss #180 miss miss #74 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 Lean-ish a `CategoryStruct` with `whiskerLeft`, `whiskerRight`, `associator`, `leftUnitor`, `rightUnitor` satisfying pentagon and triangle miss miss miss miss miss miss miss miss miss #47 LaTeX category enriched in categories with weak associator/unitor satisfying pentagon and triangle laws miss miss miss miss miss miss miss miss miss 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 Slogan weak 2-category with coherent associator and unitors miss miss miss miss miss miss miss miss miss #9 Nickname bicategory miss #32 #26 miss #15 miss #21 miss miss #68 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
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 Lean-ish `M ≃ₗ[R] (ι →₀ R)` miss miss miss miss miss miss miss miss miss miss LaTeX $M \cong_R \bigoplus_\iota R$ via a chosen isomorphism 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 Slogan a linear iso with a free module on an index set miss miss miss miss miss miss miss miss miss miss Nickname basis of a module miss #2 #32 #63 #3 #49 #3 #5 #2 #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 sorryHomology 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 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 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 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 Slogan paired left/right homology data of a short complex miss #56 miss miss #28 #71 #140 miss miss #3 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 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 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 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 Slogan strictly increasing and limit-preserving on well-orders miss miss miss miss miss miss miss miss miss miss Nickname normal function miss #27 #60 #109 #2 #44 #3 #46 #3 #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 sorryNucleus 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 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 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 Natural language an inflationary, idempotent self-map that also preserves meets miss miss miss miss miss miss miss miss miss miss Nickname nucleus #65 #68 #11 #53 #14 #103 #2 #93 miss #1 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 Lean-ish `zero | oadd : ONote → ℕ+ → ONote → ONote` #160 miss miss miss miss #97 #108 miss miss #8 LaTeX $\omega^e \cdot n + a$ — Cantor normal form below $\varepsilon_0$ miss miss miss miss miss miss miss miss miss miss Natural language ordinal terms below $\varepsilon_0$ in Cantor normal form miss miss miss miss miss #113 miss miss miss #102 Slogan Cantor normal form notation for ordinals below $\varepsilon_0$ #197 miss miss miss miss #117 #196 miss miss #77 Nickname ordinal notation (Cantor normal form) #142 #52 #180 #87 #90 #69 #92 #108 miss #24 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
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 Lean-ish `extends CoalgebraStruct` with `coassoc`, `rTensor_counit_comp_comul`, `lTensor_counit_comp_comul` miss miss miss miss #98 miss #137 miss miss #74 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 Natural language a module equipped with comultiplication and counit dual to the algebra axioms miss miss miss miss miss miss #104 miss miss #65 Slogan dual of an algebra: comultiplication + counit miss miss miss miss miss miss miss miss miss #23 Nickname coalgebra miss #31 #72 miss #33 #158 #3 miss miss #1 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
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 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 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 Natural language a family of morphisms between two functors that commutes with morphism action miss miss miss miss miss miss #182 miss miss miss Slogan morphism between functors miss miss miss miss miss miss #181 miss miss miss Nickname natural transformation miss #22 #17 miss #3 #42 #2 #53 #2 #11 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 sorryMatroid — 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 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 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 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 Slogan combinatorial abstraction of linear independence miss miss miss miss miss miss miss miss miss miss Nickname matroid miss #21 miss #28 #16 #136 #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
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 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 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 Natural language a map between categories that preserves identities and composition miss miss miss miss miss miss miss miss miss #2 Slogan a structure-preserving map between categories miss miss miss miss miss miss miss miss miss #1 Nickname functor miss #55 #34 miss #35 miss #1 #120 #5 #15 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 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 Lean-ish `extends M →ₗ[R] N →ₗ[R] R; root, coroot, reflectionPerm` with axioms miss miss miss miss #170 miss miss miss miss #26 LaTeX perfect pairing $M \otimes N \to R$ + indexed roots/coroots + reflection permutations miss #163 miss miss #71 miss #101 miss miss #30 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 Slogan data for a root system: roots, coroots, perfect pairing, reflections miss miss miss miss miss miss miss miss miss #20 Nickname root pairing miss #69 #67 #82 #11 miss #4 miss miss #25 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 sorryRing 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 Lean-ish `∀ p : Ideal R, p ≠ ⊥ → p.IsPrime → p.IsMaximal` miss miss miss miss miss miss miss miss miss miss LaTeX $\forall \mathfrak{p}$ prime, $\mathfrak{p} \ne 0 \Rightarrow \mathfrak{p}$ maximal miss miss miss miss miss miss #100 miss miss miss Natural language a ring whose every nonzero prime ideal is maximal #66 miss miss miss #78 miss #20 miss miss miss Slogan nonzero primes are maximal #155 miss miss miss miss miss miss miss miss miss Nickname Krull dimension ≤ 1 #181 #46 #81 #79 #14 #6 #1 #9 #1 #26 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
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 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 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 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 Slogan every element of L has a p-power in K miss miss miss miss miss miss miss miss miss #5 Nickname p-radical (purely inseparable) miss miss miss miss #181 miss #167 miss miss #11 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 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 Lean-ish `Subsingleton Ω[A⁄R]` and `Subsingleton (H1Cotangent R A)` miss miss miss miss miss miss miss miss miss miss LaTeX $\Omega^1_{A/R} = 0$ and $H^1(L_{A/R}) = 0$ miss miss miss miss miss miss 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 Slogan vanishing differentials and obstructions miss miss miss miss miss miss miss miss miss miss Nickname formally étale #30 #37 #1 #2 #1 #22 #1 #51 #3 #2 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
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 Lean-ish `measureOf' : Set α → M`, σ-additive on countable disjoint families miss miss miss miss miss miss miss miss miss #3 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 Natural language a σ-additive set function valued in a topological additive monoid miss miss miss miss miss #22 #9 miss miss miss Slogan σ-additive set function in a topological group miss miss miss miss miss miss miss miss miss miss Nickname vector measure miss #6 #1 #11 #2 #4 #1 #14 #1 #39 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 LaTeX $X \cong \mathrm{Spec}\,\Gamma(X, \mathcal{O}_X)$ miss miss miss miss miss miss miss miss miss miss Natural language a scheme that is isomorphic to Spec A miss miss miss miss miss miss miss miss miss #8 Slogan a scheme that is the spectrum of its ring of functions miss miss miss miss miss miss miss miss miss miss Nickname affine scheme #50 #7 #92 #56 #3 #82 #3 #38 #12 #1 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
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.
TypePhrasing Query BM25 Qwen3-0.6B EmbGemma-300M BGE-M3 Nemotron3-1B Qwen3-4B Nemotron3-8B Qwen3-8B LeanSearch v2 LeanExplore Lean-ish a `Finset (ℕ × ℕ)` that is a lower set miss miss miss miss miss miss miss miss miss miss LaTeX a finite lower set in $\mathbb{N} \times \mathbb{N}$ miss miss miss miss miss miss miss miss miss miss 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 Slogan finite lower set of cells in the integer grid miss miss miss miss miss miss miss miss miss #2 Nickname Young diagram #13 #1 #1 #6 #2 #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 Lean-ish a `LocallyRingedSpace` that is locally `Spec R` near every point miss miss miss miss miss miss miss miss miss #2 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 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 Slogan a locally ringed space modeled on Spec of rings miss miss miss miss miss miss miss miss miss #80 Nickname scheme miss #4 #6 #9 #1 #1 #1 #6 #1 #2 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
Markov kernel — A Markov kernel from $\alpha$ to $\beta$ is a function assigning to each $x \in \alpha$ a probability measure on $\beta$, such that the map $x \mapsto \mu_x$ is measurable with respect to the measurable space structures on $\alpha$ and $\beta$.
(α : Type u_1) → (β : Type u_2) → [MeasurableSpace α] → [MeasurableSpace β] → 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 Lean-ish `toFun : α → Measure β` with `measurable' : Measurable toFun` miss miss miss miss miss miss miss miss miss miss LaTeX a measurable family $\kappa : \alpha \to \mathrm{Measure}\,\beta$ miss miss miss miss #50 miss #35 #53 #12 #3 Natural language a measurable family of measures parameterized by a base space miss miss miss miss miss miss #172 miss miss miss Slogan measurable family of measures miss miss miss miss miss miss miss miss miss miss Nickname Markov kernel (transition kernel) miss #8 #1 #53 #1 #1 #1 #3 #1 #6 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Markov kernel: A Markov kernel from $\alpha$ to $\beta$ is a function assigning to each $x \in \alpha$ a probability measure on $\beta$, such that the map $x \mapsto \mu_x$ is measurable with respect to the measurable space structures on $\alpha$ and $\beta$. Formal content: ProbabilityTheory.Kernel (α : Type u_1) → (β : Type u_2) → [MeasurableSpace α] → [MeasurableSpace β] → Type (max u_1 u_2) := by sorry
Grothendieck topology on a category — An inductive definition of a Grothendieck topology on a category $\mathcal{C}$, specifying that a collection of sieves satisfies the axioms of being closed under pullbacks, composition, and containing maximal sieves.
(C : Type u) → [CategoryTheory.Category.{v, u} 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 Lean-ish `sieves : (X : C) → Set (Sieve X)` satisfying maximality, pullback stability, transitivity #98 miss miss miss #194 #126 miss miss miss #1 LaTeX assignment $X \mapsto J(X) \subseteq \mathrm{Sieve}(X)$ closed under maximality, pullback, transitivity #101 miss miss miss miss #140 #120 miss miss miss Natural language an assignment of covering sieves to each object satisfying maximality, pullback stability, and transitivity #199 miss miss miss miss #172 miss miss miss #1 Slogan axiomatic notion of "open cover" in a category miss miss miss miss miss miss #88 miss miss #127 Nickname Grothendieck topology #58 #48 #25 #147 #3 #52 #1 #10 #2 #6 Indexed document — the exact text every model embedded
Represent the following lean content for semantic search: Informal content: ['inductive']: Grothendieck topology on a category: An inductive definition of a Grothendieck topology on a category $\mathcal{C}$, specifying that a collection of sieves satisfies the axioms of being closed under pullbacks, composition, and containing maximal sieves. Formal content: CategoryTheory.GrothendieckTopology (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v) := by sorryPerfect 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 Lean-ish `Function.Bijective (fun x : R => x ^ p)` miss miss miss miss #135 miss miss miss miss miss LaTeX $x \mapsto x^p$ is a bijection on $R$ miss miss miss miss #187 miss #81 miss miss #2 Natural language a ring of characteristic p where the Frobenius map is a bijection miss miss miss miss #169 miss #174 miss miss #1 Slogan Frobenius is a bijection miss miss miss miss miss miss miss miss miss #3 Nickname perfect ring #51 #4 #1 #87 #2 #2 #1 #11 #2 #1 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
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.
(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 Lean-ish `∀ x, Dense (orbit M x)` miss miss miss miss miss miss miss miss miss #2 LaTeX $\forall x \in \alpha,\ \overline{Mx} = \alpha$ miss miss miss miss #133 miss #82 miss miss miss Natural language a group action all of whose orbits are dense miss miss miss miss miss miss #114 miss miss #33 Slogan every orbit is dense miss miss miss miss miss miss miss miss miss #4 Nickname minimal action #5 #3 #2 #1 #1 #1 #1 #2 #1 #6 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