Hola! I'm Pepa. I make mathematics compile

I contributed to the Quotient Manifolds project ↗ during ItaLean 2025 ↗, and kept going afterward. That work has since grown into a series of contributions to Mathlib ↗.

During the conference, my peers and I formalized a core fact: if a group acts freely and properly discontinuously on a charted space, the quotient space inherits a charted space structure.

That result became #35653, now merged and living in Mathlib (see the documentation ↗):

/-- The induced charted space structure on the quotient of a charted space by a free, properly
discontinuous group action. -/
@[expose, to_additive]
instance instChartedSpaceQuotient : ChartedSpace H (orbitRel.Quotient G M) :=
  isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul.isCoveringMap
    |>.isLocalHomeomorph.chartedSpace Quotient.mk_surjective

I later gave a talk walking through the PR. The slides ↗ are online if you'd like a closer look.

The next step is extending this to full manifolds, which also requires the action to be smooth. This work is still open in #40727, a large PR I've been splitting into smaller pieces that are undergoing review:

• #41832 adds Diffeomorph.smul: if a group acts on a manifold by $C^n$ diffeomorphisms, scalar multiplication by any element is itself a diffeomorphism of the manifold.
• #41835 adds orbitRel.Quotient.quotient_smul_eq (⟦g • a⟧ = ⟦a⟧ in the quotient by MulAction.orbitRel, for any g) and Homeomorph.smul_symm (the inverse of Homeomorph.smul g is Homeomorph.smul g⁻¹).
• #42436 adds StructureGroupoid.restr_mem_of_eqOn: if a partial homeomorphism agrees with a groupoid member on an open set, its restriction to that set is also in the groupoid.
• #42502 adds symm_trans_trans_mem_maximalAtlas_of_contMDiffOn and symm_trans_trans_mem_contDiffGroupoid_of_contMDiffOn: conjugating a self-diffeomorphism $f$ by two charts from the maximal atlas produces a map that lies in the maximal atlas and satisfies the contDiffGroupoid n I compatibility condition, respectively.
• more to come :)

Plenty more differential geometry contributions to Mathlib on the way!

Main Ideas

To construct the charted structure of $M/G$, the main idea is to transfer the structure of $M$ via the projection $\pi$. For each $q\in M/G$, we choose a representative $p\in M$ and use the fact that $\pi$ is locally invertible near $p$ to pull a neighborhood of $q$ back into $M$, where $p$ has a chart ${\phi }_p$. The composition ${\phi }_q={\phi }_p\circ {\pi }_p^{-1}$ then gives a chart around $q$, and collecting these charts for all points of $M/G$ yields an atlas, making the quotient a charted space.

For the manifold structure, you must show the composition of charts is smooth, that is, ${\phi }_{q^{\prime }}\circ {\phi }_q^{-1}={\phi }_{p^{\prime }}\circ {\pi }_{p^{\prime }}\circ {\pi }_p^{-1}\circ {\phi }_p^{-1}\in C^n$.

The key idea for this is to realize that, under certain conditions, this composition behaves as ${\phi }_{p^{\prime }}\circ \rho \circ {\phi }_p^{-1}$ for $\rho$ the action by some chosen element $g\in G$.

As part of my Bachelor's thesis, I completed an original formal proof of Urysohn's lemma. This was the first big project I ever completed in Lean.

The full report can be seen online in Verso ↗, and the code is available in this repository ↗.

lemma Urysohn {X : Type} {Y : Set ℝ}
    (T : TopologicalSpace X) [T' : TopologicalSpace ℝ] (hT' : T' = UsualTopology)
    {R : TopologicalSpace Y} {hY : Y = Set.Icc 0 1} {hR : R = TopoSubspace T' Y} :
    NormalSpace X ↔ ∀ C1 : Set X, ∀ C2 : Set X, C1 ≠ ∅ → C2 ≠ ∅ → IsClosed C1 → IsClosed C2 →
      Disjoint C1 C2 → ∃ f : X → Y, Continuous f ∧
        f '' C1 = ({⟨0, by simp [hY]⟩} : Set Y) ∧ f '' C2 = ({⟨1, by simp [hY]⟩} : Set Y) := by

The main difficulty of formalizing the proof of Urysohn's Lemma is best explained in Mathlib's documentation ↗:

Most paper sources prove Urysohn's lemma using a family of open sets indexed by dyadic rational numbers on [0, 1]. There are many technical difficulties with formalizing this proof (e.g., one needs to formalize the "dyadic induction", then prove that the resulting family of open sets is monotone). So, we formalize a slightly different proof.

My supervisor ↗ suggested I formalize this without looking at Mathlib's version, following Willard's General Topology instead. Therefore, I ran into the problems mentioned above and had to overcome them in different ways. As a result, my proof is different than the one currently in Mathlib.

Proof Sketch

The main idea for the proof is building a nested family of open sets indexed by $\mathbb{Q}\cap [0,1]$ (rather than the dyadic rationals); starting from two closed sets $C_1$ and $C_2$, normality repeatedly produces a new open set squeezed strictly between any two already placed: $U_0$ between $C_1$ and $C_2^c$, then another between $U_0$ and $C_2^c$, and so on. The resulting family satisfies $U_p\subseteq U_q$ whenever $p<q$.

Extending that family to all of $\mathbb{Q}$ gives a function $G:\mathbb{Q}\to \mathcal{P}(X)$; from there, $F(x)$ collects every rational $p$ with $x\in G(p)$, and finally $f(x)=\inf F(x)$ is the separating function itself. Once $G$ exists, showing $f$ lands in $[0,1]$, is continuous, and separates $C_1$ from $C_2$ is comparatively easy. Nearly all the real difficulty is in constructing $G$ and proving it monotone.

Building each $U_p$ is itself an induction, which meant inducting on the rationals. For this we fix a bijection $\mathbb{N}\simeq \mathbb{Q}\cap [0,1]$ and apply induction on the natural index instead. Proving monotonicity needed induction on two indices at once, which we get from the lexicographic order on $\mathbb{N}\times \mathbb{N}$: a well-founded relation Lean can induct on directly.

The real challenge wasn't the topology, but finding the right Lean objects to carry the argument: countability of the rationals, the lexicographic order, and non-standard recursive definitions.

Formalizing this proof was the hardest part of the whole project. The monotonicity property, which every source waves through as obvious, took me months to get right in Lean, and even after refactoring, my proof is still hundreds of lines longer than Mathlib's. Along the way I tackled problems like writing several different induction lemmas, and reworking my separating function to land in $\mathbb{R}$ instead of $\mathbb{Q}$ so I could take its infimum.

This project was an amazing way to consolidate my topology knowledge, but above all it taught me a lot about how to actually think in Lean.

After meeting at ItaLean ↗, my peers and I realized there was no regular Lean meetup in Madrid, so we started one! MadLean ↗ was born, and I've been co-organizing it since.

We prepare talks, host visiting speakers, and work together on shared projects. I've given a few of these talks myself, including one walking through the quotient manifolds PR described above.

Teaching is where most of our energy goes. We've been teaching newcomers informally ↗ for a while, and with the growing interest we're now preparing a 10-hour introductory course at CompuMates ↗ (UCM) for the winter semester of 2026, supervised by my thesis supervisor.

-- Exercise 3: use `left` and `right`

example : P → (P ∨ Q) := by
  sorry

example : (P ∨ Q) → (Q ∨ P) := by
  sorry

I actually took this same course back in 2024, as part of my own path into Lean. Now I get to help renew it and give it new life.

I also keep the MadLean website ↗ updated with weekly posts!

In July 2026 I participated in a workshop for the FLT project ↗, Kevin Buzzard's effort to formalize Fermat's Last Theorem in Lean by 2029. For a week, around twenty mathematicians and Lean experts gathered in London to push the formalization forward. The workshop was centered around using AI assistants to autoformalize results known in the 1980s.

Frontier models can now draft compiling Lean proofs of graduate-level mathematics, but what they produce is rarely clean enough to keep. So I took on the job of golfing and simplifying proofs written by an AI model on the topic of the Tate curve. The result was FLT #1091, a golf pass over TateCurveConstruction.lean making it about 200 lines shorter.

While cleaning that file, I also found results that didn't really belong in FLT, but in Mathlib ↗. I extracted and generalized them into standalone PRs:

• #41502 adds HasProd/HasSum lemmas for transferring infinite products and sums between ${\mathbb{N}}^{+}$ and $\mathbb{N}$. The additive versions turn three private FLT lemmas, stated there for $\mathbb{C}$ only, into one-line applications of general Mathlib API. I then went back to clean-up in FLT: FLT #1173.
• #41498 computes ${\sum }_n{n}^k{r}^n$ for $\Vert r\Vert <1$ in closed form via Stirling numbers of the second kind, generalizing a special case proved in FLT.

@[to_additive]
theorem hasProd_pnat_iff [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} {a : G} :
    HasProd (fun x : ℕ+ ↦ f x) a ↔ HasProd f (a * f 0) := by
  simp [hasProd_pnat_iff_hasProd_succ, hasProd_nat_add_iff]

The workshop was my first hands-on experience with autoformalization: the newest models and tools had just come out, and we spent the week testing them on commutative algebra, representation theory and elliptic curves, learning how to prompt them, where they break, and how to review what they hand back.

I hope to keep contributing to FLT; there's plenty left to formalize before 2029!