Introducing Lean Finder – A Smarter Search for Lean

Stream: general

[Wuyang]

Dear Lean Users,

We DeLTA Lab (at Simon Fraser University) are building foundational tools to support mathematicians working on formal mathematics.

We are excited to introduce Lean Finder, a semantic search engine for Lean that understands latent intents behind your queries.

You can try Lean Finder in two ways:

1. Web Service: With beautifully rendered LaTeX and code: https://leanfinder.github.io/
2. Zulip Chat: You can simply ping our chatbot: @leanfinder + your inquiry.

Lean Finder supports four types of input:

• Informalized statement – A full or partial natural-language description of the statement you’re looking for.
• User question – Ask in your own words, e.g., “Is there code for …” · “Why does this give an error …” · “How to define or derive instances …” · “How to finish or shorten proofs …” · “How to apply this lemma or theorem …”
• Proof state – Paste your current state directly from VS Code.
• Statement definition – Provide any fragment or complete definition.

Finally, our web service includes feedback tools. Please vote or upvote retrievals you find useful. Your feedback directly helps us improve Lean Finder, making it an even more powerful resource for the Lean and Zulip communities.

Thank you!

Sincerely,
Wuyang

[Wuyang]

Some examples of use cases:

@leanfinder Let L/K be a field extension and let x, y ∈ L be algebraic elements over K with the same minimal polynomial. Then the K-algebra isomorphism algEquiv between the simple field extensions K(x) and K(y) maps the generator x of K(x) to the generator y of K(y); i.e. algEquiv(x) = y.

[leanfinder]

Here’s what I found:

• theorem minpoly.algEquiv_apply {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : algEquiv hx h_mp (AdjoinSimple.gen K x) = AdjoinSimple.gen K y := by have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩ rw [algEquiv, trans_apply, ← adjoinRootEquivAdjoin_apply_root K hx.isIntegral, symm_apply_apply, trans_apply, AdjoinRoot.algEquivOfEq_apply_root, adjoinRootEquivAdjoin_apply_root K hy.isIntegral] "Let $L/K$ be a field extension and let $x, y \in L$ be algebraic elements over $K$ with the same minimal polynomial. Then the $K$-algebra isomorphism $\text{algEquiv}$ between the simple field extensions $K(x)$ and $K(y)$ maps the generator $x$ of $K(x)$ to the generator $y$ of $K(y)$, i.e.,
  $\text{algEquiv}(x) = y.$" (score: 0.861)

• theorem algEquiv_apply {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : algEquiv hx h_mp (AdjoinSimple.gen K x) = AdjoinSimple.gen K y := by have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩ rw [algEquiv, trans_apply, ← adjoinRootEquivAdjoin_apply_root K hx.isIntegral, symm_apply_apply, trans_apply, AdjoinRoot.algEquivOfEq_apply_root, adjoinRootEquivAdjoin_apply_root K hy.isIntegral] "Let $L/K$ be a field extension and let $x, y \in L$ be algebraic elements over $K$ with the same minimal polynomial. Then the $K$-algebra isomorphism $\text{algEquiv}$ between the simple field extensions $K(x)$ and $K(y)$ maps the generator $x$ of $K(x)$ to the generator $y$ of $K(y)$, i.e., $\text{algEquiv}(x) = y.$" (score: 0.859)

• /-- The canonical algEquiv between K⟮x⟯and K⟮y⟯, sending x to y, where x and y have
  the same minimal polynomial over K. -/ noncomputable def algEquiv {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := by have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩ exact AlgEquiv.trans (adjoinRootEquivAdjoin K hx.isIntegral).symm (AlgEquiv.trans (AdjoinRoot.algEquivOfEq (ne_zero hx.isIntegral) h_mp) (adjoinRootEquivAdjoin K hy.isIntegral)) "Let $L/K$ be a field extension and let $x, y \in L$ be algebraic elements over $K$ with the same minimal polynomial. Then there exists a canonical $K$-algebra isomorphism between the simple field extensions $K(x)$ and $K(y)$ that maps $x$ to $y$." (score: 0.842)

• definition minpoly.algEquiv {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := by have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩ exact AlgEquiv.trans (adjoinRootEquivAdjoin K hx.isIntegral).symm (AlgEquiv.trans (AdjoinRoot.algEquivOfEq (ne_zero hx.isIntegral) h_mp) (adjoinRootEquivAdjoin K hy.isIntegral)) "Given a field extension $L/K$ and two elements $x, y \in L$ that are algebraic over $K$ with the same minimal polynomial, there exists a $K$-algebra isomorphism between the intermediate fields $K(x)$ and $K(y)$. This isomorphism maps the generator $x$ of $K(x)$ to the generator $y$ of $K(y)$." (score: 0.834)

• theorem algEquivOfEq_apply_root {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) : algEquivOfEq hp h_eq (root p) = root q := by rw [← coe_algHom, algEquivOfEq_toAlgHom, liftHom_root] "Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials such that $p = q$. The algebra isomorphism $\text{algEquivOfEq}$ from $\text{AdjoinRoot}\,p$ to $\text{AdjoinRoot}\,q$ maps the adjoined root of $p$ to the adjoined root of $q$, i.e., $\text{algEquivOfEq}\,h_p\,h_{eq}(\text{root}\,p) = \text{root}\,q.$" (score: 0.791)

• theorem minpoly.exists_algEquiv_of_root [Normal K L] {x y : L} (hy : IsAlgebraic K y) (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ x = y := by have hx : IsAlgebraic K x := ⟨minpoly K y, ne_zero hy.isIntegral, h_ev⟩ set f : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := algEquiv hx (eq_of_root hy h_ev) have hxy : (liftNormal f L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y := by rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y] exact ⟨(liftNormal f L), hxy⟩ "Let $L/K$ be a normal field extension, and let $x, y \in L$ be elements such that $y$ is algebraic over $K$ and $x$ is a root of the minimal polynomial of $y$ over $K$. Then there exists a $K$-algebra automorphism $\sigma: L \to L$ such that $\sigma(x) = y$." (score: 0.790)

• theorem exists_algEquiv_of_root [Normal K L] {x y : L} (hy : IsAlgebraic K y) (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ x = y := by have hx : IsAlgebraic K x := ⟨minpoly K y, ne_zero hy.isIntegral, h_ev⟩ set f : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := algEquiv hx (eq_of_root hy h_ev) have hxy : (liftNormal f L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y := by rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y] exact ⟨(liftNormal f L), hxy⟩ "Let $L/K$ be a normal field extension, and let $x, y \in L$ be algebraic over $K$. If $x$ is a root of the minimal polynomial of $y$ over $K$, then there exists a $K$-algebra isomorphism $\sigma: L \simeq L$ such that $\sigma(x) = y$. This means $x$ and $y$ are Galois conjugates." (score: 0.789)

• theorem minpoly.exists_algEquiv_of_root' [Normal K L] {x y : L} (hy : IsAlgebraic K y) (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ y = x := by obtain ⟨σ, hσ⟩ := exists_algEquiv_of_root hy h_ev use σ.symm rw [← hσ, symm_apply_apply] "Let $L/K$ be a normal field extension, and let $x, y \in L$ be elements such that $y$ is algebraic over $K$ and $x$ is a root of the minimal polynomial of $y$ over $K$. Then there exists a $K$-algebra automorphism $\sigma: L \to L$ such that $\sigma(y) = x$." (score: 0.782)

• theorem AdjoinRoot.algEquivOfEq_apply_root {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) : algEquivOfEq hp h_eq (root p) = root q := by rw [← coe_algHom, algEquivOfEq_toAlgHom, liftHom_root] "Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials such that $p = q$. The algebra isomorphism $\text{algEquivOfEq}$ from $\text{AdjoinRoot}\,p$ to $\text{AdjoinRoot}\,q$ maps the adjoined root of $p$ to the adjoined root of $q$, i.e.,
  $\text{algEquivOfEq}\,h_p\,h_{eq}(\text{root}\,p) = \text{root}\,q.$" (score: 0.780)

• theorem algEquivOfAssociated_apply_root {p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) : algEquivOfAssociated hp hpq (root p) = root q := by rw [← coe_algHom, algEquivOfAssociated_toAlgHom, liftHom_root] "Let $K$ be a field and let $p, q \in K[X]$ be nonzero associated polynomials. If $\operatorname{AdjoinRoot} p \simeq \operatorname{AdjoinRoot} q$ is an algebra equivalence, then the adjoined root $\operatorname{root}_p$ of $p$ is mapped to the adjoined root $\operatorname{root}_q$ of $q$ under this equivalence." (score: 0.780)

[Wuyang]

@leanfinder K : Type u_1
E : Type u_2
inst✝ : RCLike K
z✝ z : K
⊢ |re z| ≤ ‖z‖
Transform the goal from proving that the absolute value of the real part of a complex number is less than or equal to its norm, to proving that the square of the real part is less than or equal to the squared norm of the number.

[leanfinder]

Here’s what I found:

• theorem RCLike.abs_re_le_norm (z : K) : |re z| ≤ ‖z‖ := by rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm] apply re_sq_le_normSq "For any element $z$ in a real-complex like field $K$ (where $K$ is either $\mathbb{R}$ or $\mathbb{C}$), the absolute value of its real part is bounded by its norm, i.e., $|\text{Re } z| \leq \|z\|$." (score: 0.797)

• theorem RCLike.normSq_eq_def' (z : K) : normSq z = ‖z‖ ^ 2 := norm_sq_eq_def.symm "For any element $z$ in an RCLike field $K$ (which is either $\mathbb{R}$ or $\mathbb{C}$), the squared norm $\text{normSq}(z)$ equals the square of its norm, i.e.,
  $\text{normSq}(z) = \|z\|^2.$" (score: 0.793)

• theorem sq_le_sq : a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b| := by simpa only [sq_abs] using sq_le_sq₀ (abs_nonneg a) (abs_nonneg b) "For any elements $a$ and $b$ in a linearly ordered ring $\alpha$, the square of $a$ is less than or equal to the square of $b$ if and only if the absolute value of $a$ is less than or equal to the absolute value of $b$, i.e., $a^2 \leq b^2 \leftrightarrow |a| \leq |b|$." (score: 0.791)

• theorem RCLike.re_le_norm (z : K) : re z ≤ ‖z‖ := (abs_le.1 (abs_re_le_norm z)).2 "For any element $z$ in a real-complex like field $K$ (where $K$ is either $\mathbb{R}$ or $\mathbb{C}$), the real part of $z$ is bounded by its norm, i.e., $\text{Re } z \leq \|z\|$." (score: 0.790)

• theorem RCLike.norm_re_le_norm (z : K) : ‖re z‖ ≤ ‖z‖ := abs_re_le_norm z "For any element $z$ in a real-complex like field $K$ (where $K$ is either $\mathbb{R}$ or $\mathbb{C}$), the norm of its real part is bounded by its norm, i.e., $\|\text{Re } z\| \leq \|z\|$." (score: 0.790)

• theorem RCLike.re_sq_le_normSq (z : K) : re z * re z ≤ normSq z := le_add_of_nonneg_right (mul_self_nonneg _) "For any element $z$ in a real-complex like field $K$ (where $K$ is either $\mathbb{R}$ or $\mathbb{C}$), the square of its real part is less than or equal to its squared norm, i.e., $(\text{Re } z)^2 \leq \text{normSq } z$." (score: 0.790)

• theorem Real.le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ √y ↔ x ^ 2 ≤ y := le_iff_le_iff_lt_iff_lt.2 <| sqrt_lt hy hx "For any nonnegative real numbers $x$ and $y$, the inequality $x \leq \sqrt{y}$ holds if and only if $x^2 \leq y$." (score: 0.786)

• theorem sq_abs (a : α) : |a| ^ 2 = a ^ 2 := by simpa only [sq] using abs_mul_abs_self a "For any element $a$ in a linearly ordered ring $\alpha$, the square of the absolute value of $a$ equals the square of $a$, i.e., $|a|^2 = a^2$." (score: 0.786)

• theorem RCLike.sqrt_normSq_eq_norm {z : K} : √(normSq z) = ‖z‖ := by rw [normSq_eq_def', Real.sqrt_sq (norm_nonneg _)] "For any element $z$ in an RCLike field $K$ (which is either $\mathbb{R}$ or $\mathbb{C}$), the square root of its squared norm equals its norm, i.e.,
  $\sqrt{\text{normSq}(z)} = \|z\|.$" (score: 0.785)

• theorem RCLike.mul_self_norm (z : K) : ‖z‖ * ‖z‖ = normSq z := by rw [normSq_eq_def', sq] "For any element $z$ in an RCLike field $K$ (which is either $\mathbb{R}$ or $\mathbb{C}$), the product of the norm of $z$ with itself equals the squared norm of $z$, i.e.,
  $\|z\| \cdot \|z\| = \text{normSq}(z).$" (score: 0.779)

[Matthew Ballard]

@Wuyang Don't cross post

[Wuyang]

Matthew Ballard said:

Wuyang Don't cross post

No more! I just posted in general and new members. Hope that could be fine.

[Matthew Ballard]

I have removed your post in #new members. Don't cross post.

[Eric Wieser]

Some initial feedback; this output is way too verbose to be suitable for zulip; I suggest following the loogle bot and giving a one-line summary and a link to the webpage.

[Eric Wieser]

Showing the proof for each theorem is also very strange, as this is not relevant at all when trying to search for a theorem to apply.

[Wuyang]

@Eric Wieser Thank you very much for this valuable feedback! It took me some time to integrate this change.
I give an example below. Do you like this format?

[Wuyang]

@leanfinder Let L/K be a field extension and let x, y ∈ L be algebraic elements over K with the same minimal polynomial. Then the K-algebra isomorphism algEquiv between the simple field extensions K(x) and K(y) maps the generator x of K(x) to the generator y of K(y); i.e. algEquiv(x) = y.

[leanfinder]

Here’s what I found:

minpoly.algEquiv_apply (score: 0.868)

Let $L/K$ be a field extension and let $x, y \in L$ be algebraic elements over $K$ with the same minimal polynomial. Then the $K$-algebra isomorphism $\text{algEquiv}$ between the simple field extensions $K(x)$ and $K(y)$ maps the generator $x$ of $K(x)$ to the generator $y$ of $K(y)$, i.e.,
$\text{algEquiv}(x) = y.$

algEquiv_apply (score: 0.865)

Let $L/K$ be a field extension and let $x, y \in L$ be algebraic elements over $K$ with the same minimal polynomial. Then the $K$-algebra isomorphism $\text{algEquiv}$ between the simple field extensions $K(x)$ and $K(y)$ maps the generator $x$ of $K(x)$ to the generator $y$ of $K(y)$, i.e., $\text{algEquiv}(x) = y.$

minpoly.algEquiv (score: 0.844)

Given a field extension $L/K$ and two elements $x, y \in L$ that are algebraic over $K$ with the same minimal polynomial, there exists a $K$-algebra isomorphism between the intermediate fields $K(x)$ and $K(y)$. This isomorphism maps the generator $x$ of $K(x)$ to the generator $y$ of $K(y)$.

More Retrievals...

minpoly.exists_algEquiv_of_root (score: 0.798)

Let $L/K$ be a normal field extension, and let $x, y \in L$ be elements such that $y$ is algebraic over $K$ and $x$ is a root of the minimal polynomial of $y$ over $K$. Then there exists a $K$-algebra automorphism $\sigma: L \to L$ such that $\sigma(x) = y$.

algEquivOfEq_apply_root (score: 0.797)

Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials such that $p = q$. The algebra isomorphism $\text{algEquivOfEq}$ from $\text{AdjoinRoot}\,p$ to $\text{AdjoinRoot}\,q$ maps the adjoined root of $p$ to the adjoined root of $q$, i.e., $\text{algEquivOfEq}\,h_p\,h_{eq}(\text{root}\,p) = \text{root}\,q.$

exists_algEquiv_of_root (score: 0.795)

Let $L/K$ be a normal field extension, and let $x, y \in L$ be algebraic over $K$. If $x$ is a root of the minimal polynomial of $y$ over $K$, then there exists a $K$-algebra isomorphism $\sigma: L \simeq L$ such that $\sigma(x) = y$. This means $x$ and $y$ are Galois conjugates.

minpoly.exists_algEquiv_of_root' (score: 0.790)

Let $L/K$ be a normal field extension, and let $x, y \in L$ be elements such that $y$ is algebraic over $K$ and $x$ is a root of the minimal polynomial of $y$ over $K$. Then there exists a $K$-algebra automorphism $\sigma: L \to L$ such that $\sigma(y) = x$.

AdjoinRoot.algEquivOfEq_apply_root (score: 0.788)

Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials such that $p = q$. The algebra isomorphism $\text{algEquivOfEq}$ from $\text{AdjoinRoot}\,p$ to $\text{AdjoinRoot}\,q$ maps the adjoined root of $p$ to the adjoined root of $q$, i.e.,
$\text{algEquivOfEq}\,h_p\,h_{eq}(\text{root}\,p) = \text{root}\,q.$

exists_algEquiv_of_root' (score: 0.787)

Let $L/K$ be a normal field extension, and let $x, y \in L$ be algebraic over $K$. If $x$ is a root of the minimal polynomial of $y$ over $K$, then there exists a $K$-algebra isomorphism $\sigma: L \simeq L$ such that $\sigma(y) = x$. This means $x$ and $y$ are Galois conjugates, with the roles of $x$ and $y$ reversed.

[Wuyang]

@Eric Wieser One thing to note here is that we support more informative docstrings than mathlib. You may have noticed that many statements in mathlib have very short, or even no docstrings. This may confuse new members. Lean Finder will provide more detailed descriptions for all statements, which I have now put into the spoiler.

[Kenny Lau]

it feels like your queries are LLM-generated, is there a specific algorithm you used? is this available in Leanfinder? Leansearch also features an LLM feature called "augmentation"

[Wuyang]

@Kenny Lau Thanks!
You don't need to use LLM to augment your query.

Quantitatively, Lean Finder achieves higher retrieval rates on mathlib4 than Lean Search, even with their "augmentation" feature:

• LeanSearch: 0.487
• Lean Finder: 0.620

Below I am using another query, which came from a vote submitted by an active user.
@leanfinder Theorem to show that if n is a positive integer, then 1/n is positive

[leanfinder]

Here’s what I found:

lemma (score: 0.700)

For any element $a$ in a type with a multiplication operation and a partial order, if $a > 0$, then for all natural numbers $n$, the power $a^n$ is also positive, i.e., $a^n > 0$. This is established by induction: for $n = 0$, $a^0 = 1 > 0$; for $n + 1$, $a^{n+1} = a^n \cdot a > 0$ since both $a^n > 0$ and $a > 0$.

succ_ge_zero(k (score: 0.699)

For any natural number $k$, the reciprocal of $k+1$ is positive in the real numbers, i.e., $\frac{1}{k+1} > 0$. This follows from the fact that the successor of a natural number is always positive, and thus its reciprocal is also positive.

Nat.cast_pos (score: 0.699)

For any ordered semiring $\alpha$ that is nontrivial (i.e., contains at least two distinct elements), and any natural number $n$, the cast of $n$ in $\alpha$ is positive (i.e., $0 < (n : \alpha)$) if and only if $0 < n$ in $\mathbb{N}$.

More Retrievals...

Nat.one_div_pos_of_nat (score: 0.697)

For any natural number $n$ and any linear ordered semifield $\alpha$, the reciprocal of the cast of $n$ plus one is positive, i.e., $0 < \frac{1}{n + 1}$ where $n$ is interpreted in $\alpha$.

[high]](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.natCast_pos#doc) (score: 0.697)

For any natural number $n$, the integer cast of $n$ is positive if and only if $n$ is positive, i.e., $(0 : \mathbb{Z}) < n \leftrightarrow 0 < n$.

lemma (score: 0.697)

For any element $a$ in a type $G_0$, the inverse $a^{-1}$ is positive if and only if $a$ is positive. That is, $0 < a^{-1} \leftrightarrow 0 < a$. This relies on the involutive property of inversion and the reflection of strict order under left multiplication by nonnegative elements.

add_one_pos (score: 0.693)

For any natural number $n$, adding one to $n$ results in a number greater than zero, i.e., $0 < n + 1$. This follows from the fact that the successor of any natural number is positive.

Nat.one_div_cast_pos (score: 0.692)

For any natural number $n \neq 0$ and any ordered semifield $\alpha$, the reciprocal of the cast of $n$ in $\alpha$ is positive, i.e., $0 < \frac{1}{(n : \alpha)}$.

pow_pos (score: 0.692)

If $a$ is a positive number, then for any natural number $n$, the power $a^n$ is also positive, i.e., $a^n > 0$. This holds for $n = 0$ because $a^0 = 1 > 0$, and for $n + 1$ because $a^{n+1} = a^n \cdot a$ and both $a^n$ and $a$ are positive.

pow_pos (score: 0.692)

If $a$ is a positive number, then for any natural number $n$, the power $a^n$ is also positive. Formally, if $0 < a$, then $0 < a^n$ for all $n \in \mathbb{N}$. This is proven by induction: the base case $n = 0$ follows from $a^0 = 1 > 0$, and the inductive step uses $a^{n+1} = a^n \cdot a$ and the positivity of $a$ and $a^n$.

[Jireh Loreaux]

@Wuyang note that there is something screwy in the links (the first one is called "lemma" and links to docs#pow_pos, the second one is clearly misnamed too, and even more strangely, it links to a file in a completely different repository: https://github.com/optsuite/optlib/blob/26fcefb31b5aee7f7f5fc7194f462b437282675f/Optlib/Convex/ImageSubgradientClosed.lean, which contains a lemma succ_ge_zero)

[Wuyang]

@Jireh Loreaux Thanks!

1. The first one seems have some weird rendering issue, which I will dig more
2. Another feature of Lean Finder is that, it supports statements beyond mathlib. We can retrieve from more 3rd party contributions:

• SciLean (https://github.com/lecopivo/SciLean)
• A formalization of Borel determinacy in Lean (Manthe, 2025) (https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean)
• Optlib (Li et al., 2025a;b) (https://github.com/optsuite/optlib)
• Formalising Fermat’s Last Theorem for Exponent 3 (Monticone, 2024) (https://github.com/riccardobrasca/flt3)
• Formalisation of constructable numbers (Monnerjahn, 2024) (https://github.com/Louis-Le-Grand/Formalisation-of-constructable-numbers)

[Wuyang]

(deleted)

[Wuyang]

@leanfinder Theorem to show that if n is a positive integer, then 1/n is positive

[leanfinder]

Here’s what I found:

Nat.one_div_pos_of_nat (score: 0.762)

For any natural number $n$ and any linear ordered semifield $\alpha$, the reciprocal of the cast of $n$ plus one is positive, i.e., $0 < \frac{1}{n + 1}$ where $n$ is interpreted in $\alpha$.

Nat.one_div_cast_pos (score: 0.762)

For any natural number $n \neq 0$ and any ordered semifield $\alpha$, the reciprocal of the cast of $n$ in $\alpha$ is positive, i.e., $0 < \frac{1}{(n : \alpha)}$.

PNat.pos (score: 0.757)

For any positive natural number $n$, its canonical image in the natural numbers is strictly greater than zero, i.e., $0 < n$.

More Retrievals...

inv_pos_of_nat (score: 0.757)

For any natural number $n$ and any linear ordered semifield $\alpha$, the inverse of $n + 1$ (where $n$ is interpreted in $\alpha$) is positive, i.e., $0 < (n + 1)^{-1}$.

Nat.inv_pos_of_nat (score: 0.756)

For any natural number $n$ and any linear ordered semifield $\alpha$, the inverse of the cast of $n$ plus one is positive, i.e., $0 < (n + 1)^{-1}$ where $n$ is interpreted in $\alpha$.

Nat.cast_pos (score: 0.755)

For any ordered semiring $\alpha$ that is nontrivial (i.e., contains at least two distinct elements), and any natural number $n$, the cast of $n$ in $\alpha$ is positive (i.e., $0 < (n : \alpha)$) if and only if $0 < n$ in $\mathbb{N}$.

add_one_pos (score: 0.754)

For any natural number $n$, adding one to $n$ results in a number greater than zero, i.e., $0 < n + 1$. This follows from the fact that the successor of any natural number is positive.

one_div_pos_of_nat (score: 0.753)

For any natural number $n$ and any linear ordered semifield $\alpha$, the reciprocal of $n + 1$ (where $n$ is interpreted in $\alpha$) is positive, i.e., $0 < \frac{1}{n + 1}$.

one_div_pos (score: 0.751)

For any element $a$ in a type $\alpha$ with division and a partial order, the reciprocal $\frac{1}{a}$ is positive if and only if $a$ itself is positive, i.e., $0 < \frac{1}{a} \leftrightarrow 0 < a$.

one_div_pos (score: 0.749)

For any element $a$ in a type $\alpha$ with division and a partial order, the reciprocal $\frac{1}{a}$ is positive if and only if $a$ itself is positive, i.e., $0 < \frac{1}{a} \leftrightarrow 0 < a$.

[Wuyang]

@Jireh Loreaux now the rendering works :point_up:

[Jireh Loreaux]

Why are the scores different on this run versus the last one?

[Wuyang]

@Jireh Loreaux I think we have to call Lean Finder in separate messages instead of being mixed with other irrelevant text