0 2026/update-0602 Hi! It has been quite a while since I last wrote a blog post, but I wanted to write an update about what I’ve been up to for the past little while. In this post, I want to talk about all the Lean4 stuff I’ve done, and after this quarter is over I will probably post some class projects and notes for anything marginally interesting. As I’m writing this though, there is still 1 more week until finals…
I first got into lean back in fall quarter, when I was taking MATH 208 (Linear Algebra) with Prof. Bianca Viray. In that class, Professor Viray had a cool bonus assignment to prove something in Lean, and I decided to prove that the span of a set of vectors is a vector space. The next quarter, she kindly invited me to join her Math AI Lab project, formalizing the fact that finite etale extensions of local rings are monogenic.
I had a ton of fun working with George Peykanu, Bryan Boehnke, and John Leo on this project, and our code is at github:uw-math-ai/monogenic-extensions. We formalized lemmas 3.1 and 3.2 of Professor Viray’s paper “Number fields generated by points in linear systems on curves” (arXiv:2503.07846). Statements of the lemmas are below, and you can see the project structure with all the helper lemmas in the lean blueprint for this project.
Lemma 3.2: Let (R, \mathfrak m_R) be a local ring and let (S, \mathfrak m_S) be a local finite extension of R. If R\to S is etale, then there exists a \beta \in S such that R[\beta] = S. Furthermore, if f(z) \in R[z] is the minimal polynomial of \beta, then f'(\beta) \in S^\times.
namespace IsLocalRing
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
[IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S]
theorem exists_adjoin_eq_top [Algebra.FormallyUnramified R S] :
∃ β : S, Algebra.adjoin R {β} = ⊤ := sorry
lemma isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
[Algebra.Etale R S] {β : S}
(hadj : Algebra.adjoin R {β} = ⊤) :
IsUnit (aeval β (minpoly R β).derivative) := sorryLemma 3.1: Let (R, \mathfrak m_R) be a regular local ring and let (S, \mathfrak m_S) be a regular local finite extension of R. If there exists a height 1 prime \mathbf q_0 \subset S such that R/\mathbf q_0 \cap R \to S / \mathbf q_0 is etale, then S is monogenic of R, i.e. there exists a \beta \in S such that R[\beta] = S.
theorem exists_isAdjoinRootMonic_of_quotientMap_etale
[IsDomain R] [IsDomain S] [IsIntegrallyClosed R]
[UniqueFactorizationMonoid S] [Algebra R S]
[FaithfulSMul R S] [Module.Finite R S]
(q : Ideal S)
[hq_prime : q.IsPrime] (hq_height : q.height = 1)
(hétale : (Ideal.quotientMap q (algebraMap R S) le_rfl).Etale) :
∃ f : R[X], Nonempty (IsAdjoinRootMonic S f) := sorryAll of these results have been fully formalized, and we whittled it down to a little less than 700 lines of Lean. From our work, we got two mathlib pull requests merged: add mkOfAdjoinEqTop' #36421 and Finite étale extensions of local rings are monogenic #37527. Lemma 3.2 can now be found in Mathlib at Mathlib.RingTheory.LocalRing.Etale! Many thanks to our reviewers, Artie Khovanov and Riccardo Brasca.
The second PR (#37527) is simply the file Etale.lean containing the two parts of lemma 3.2, but the first PR (#36421) adds a couple of missing results across the mathlib API to prove that Algebra.adjoin R {β} = ⊤ implies IsAdjoinRootMonic S (minpoly R β) if S is free as an R-module. Artie wrote a couple of sibling PRs (embeddings of free modules #37919 and strengthen Cayley-Hamilton #37872), extending mathlib’s Cayley-Hamilton result to prove a more general version of minpoly.natDegree_le, and also adding a nice API for the fact that a free module embeds into another module iff that module has a higher rank. Thus, other parts of mathlib were improved, beyond just adding a couple of new results! Open source is pretty cool.
AI tools like Claude code were extremely helpful in this project, if not a little scary. I’m not going to pretend I am any closer to knowing what etale means, but I was able to accomplish a lot just by looking through existing results in mathlib and with Claude. One of the coolest takeaways for me was how similar using mathlib was to using any other software library— it’s just that instead of calling a function to do a HTTP GET request, I am calling proofs (which really are functions by the Curry-Howard isomorphism). To me, this is such a cool way to reframe the problem, and reading through mathlib code and searching through documentation to find the correct ways to accomplish things was eerily similar to using traditional, non-math software libraries.
Last month, I also had the opportunity to participate in the first-ever UW Lean Hackathon, where I won first place with Brian Nugent and Leopald Mayer! Our project was cat-rw, a new tactic similar to grw and rw that works on data types in addition to propsition types, allowing mathematicians to treat isomorphisms as if they were strict equalities. The tactic takes an isomorphism like h : a ≅ a', and it uses isomorphism lemmas (e.g. a ≅ a' and b ≅ b' implies that a ⨯ b ≅ a' ⨯ b') to allow you to substitute a for a', even if it is deeply nested in some structure. The code is at github:leomayer1/cat-rw.
This was a really fun 2-day event over the weekend. With the help of Gemini to figure out how the heck Lean metaprogramming works, I wrote the general algorithm that performs rewrites on data given any arbitrary transitive and reflexive binary relations. The user just has to tell the tactic about the binary relation and tag isomorphism lemmas with @[cat_rw], and the tactic will try to figure out a rewrite, even if it has to mix multiple different binary relations. Here is the pseudocode I wrote for the core rewriting logic:
grw (r₂) (rule : r₁ X X') (expr) : Option (r₂ expr expr') :=
if rule.lhs matches expr
return some (rule)
for each (
lemma (h₁ : r₃ A A') (h₂ : r₃ B B') ... :
r₂ (f A B ...) (f A' B' ...)
) {
if (lemma.lhs matches expr) {
intro metavars for h₁ h₂ ...
let mut rewrote := false
for each hᵢ {
if let some(e) := grw r₃ rule hᵢ.lhs
hᵢ = e; rewrote = true
else
hᵢ = refl on r₃
}
if rewrote
return some (lemma h₁ h₂ ...)
} else
-- consider bailing out here instead of keep trying.
}
return noneThis function uses a binary relation r₂ and some rule (which is an instance of that binary relation) to rewrite an expression expr into a new expr', returning the data that expr and expr' are also related by r₂. For example, if we take r₂ := Equals and rule : a = b, then trying to rewrite f a should return f a = f b. In general though, our relation can be isomorphisms or inequalities, and the r₂ expr expr' type does NOT have to be a proposition! To perform rewrites, we simply look for lemmas/definitions that return a r₂ type where the left-hand side of the relation matches our expression.
Then, we simply apply that lemma and recurse down into rewriting the hypotheses that went into the lemma, falling back to using reflexivity if we cannot perform a rewrite on any hypothesis. For example, say our expr was a ⨯ b and we are applying the lemma binary_prod (h₁ : x ≅ x') (hy₂ : y ≅ y') : x ⨯ y ≅ x' ⨯ y' to rewrite with the rule a ≅ a'. Note that x x' y and y' at this point are all metavariables that we need to unify with the real variables a b and a'.
First, we match the left hand side of the result type to our expression, so we unify x ⨯ y with a ⨯ b (x is now a and y is b). Now we recurse to rewrite the left hand side of h₁ : a ≅ x' using our rule a ≅ a'. In the recursive call we just use the rule directly to rewrite a, so we get back h₁ : a ≅ a', i.e. x' becomes a'. We recurse again to try to rewrite b in h₂ : b ≅ y', but we cannot rewrite b with our rule about a so we just use reflexivity for b as h₂. Thus, y' is b, and h₂ : b ≅ b. Overall, binary_prod h₁ h₂ : a ⨯ b ≅ a' ⨯ b, and we have performed the expected rewrite!
Note that in the general case, we can mix different binary relations. With this primitive, we can implement some basic logic to be able to rewrite goals:
tactic_impl (rule : r₁ X X') (goal) :=
if goal matches some r₂ A B
rhsrw := grw r₂ rule B
lhsrw := if (r₂ is symmetric) then
(grw r₂ rule A).symm else none
if (rhsrw and lhsrw are both none)
throw error
newGoal ← intro new mvar
goal.assign (rhsrw ∘ newgoal ∘ lhsrw)
return [newGoal]
if r₂ is not symmetric
throw error
for every relation r₂
if let some(e) := grw r₂ rule goal
newGoal ← intro new mvar
goal.assign (e.symm newGoal)
return [newGoal]
throw errorThis pseudocode version is a bit incomplete, as the real implementation allows you to have finer control to do the nth rewrite or rewrite at a hypothesis instead of rewriting a tactic goal. Those were details I let Gemini figure out though lol.
This project currently lacks a lot of polish, but I think it has a lot of potential to be useful (and evidently our judges thought so too!). In the future, we would probably like to discuss this with the Lean zulip to see if people more broadly are interested.