We are pleased to invite you to submit presentation proposals for the ITP 2025 Lean Workshop, which will be held in Reykjavik, Iceland on 2 October 2025, as a satellite to the ITP conference, a member of the larger FroCoS/ITP/TABLEAUX ‘25 gathering.
This is the first time we have had a Lean Workshop at ITP, and we’re excited to see it develop. It brings together developers, contributors, and users of Lean and Mathlib.
The Lean Workshop aims to create a friendly and welcoming space where community members can connect, share experiences, and support one another. Whether you’re a seasoned contributor or just getting started with Lean, we encourage participation from all backgrounds and experience levels. The workshop fosters an open atmosphere where newcomers can learn from the community, experienced users can share their knowledge, and everyone can build lasting connections. Rather than serving as a venue for traditional research papers, the Lean Workshop is organized around informal presentations and discussions, supplemented with invited talks.
09:00-10:00: Joachim Breitner, Report from the FRO
10:10-10:30: Jhet Chan, Gödel Mirror: A Paraconsistent Calculus Mechanized in Lean 4 (online)
11:00-11:20: Mauricio Barba da Costa, Automatic Geometry Theorem Proving Using Polynomial Elaboration
11:20-11:40: Moritz Firsching, The Formal Conjectures repo (online)
11:40-12:00: Lukas Gerlach, Formalizing Possibly Infinite Trees of Finite Degree
12:00-12:30: Yulu Pan, Verifying a real-world regex implementation
16:00-16:20: Luc Duponcheel, Teaching Programming using Lean
16:20-16:40: Jesse Alama, Euler’s polyhedron formula à la Lean
16:40-17:00: Jovan Gerbscheid, Generalized Rewriting
17:00-17:30: Chase Norman, Canonical: simplify, monomorphize, destruct.
09:00-10:00: Joachim Breitner, Report from the FRO
For a bit over two years now, Lean development is in the hands of the the Lean FRO, and this led to a flurry of new developments. Joachim Breitner, Lean developer at the FRO, looks at the main developments and achievements of the last year, and gives a peek at what to expect next. He will also take any question about Lean, the FRO and everything else, and may actually answer some of them.
Ever since Joachim has found beauty and elegance in Functional Programming, he’s been working with and on functional programming languages, in particular Haskell. He’s also always been fascinated by Interactive Theorem Proving and his academic persona used Isabelle and Coq for formalize mathematics and verify programs. These two interests find their natural synthesis in the Lean programming language, and Joachim joined the Lean FRO to work on the Lean compiler itself. Besides such serious nerdery, you’ll find Joachim dancing Swing and Tango (in particular when traveling to conferences, so talk to him if you want to join), paragliding and unapologetically making bad puns.
10:10-10:30: Jhet Chan, Gödel Mirror: A Paraconsistent Calculus Mechanized in Lean 4
This talk presents the Gödel Mirror, a minimal formal system where self-referential paradox is not a bug, but the primary engine for computation. Inspired by Gödelian self-reference, the system is a small, paraconsistent term rewriting calculus that, when faced with a contradiction, initiates a deterministic cycle to metabolize the inconsistency into new, stable syntactic structures. This provides a formal, “non-explosive” model for contradiction-driven evolution.
The entire system, including its syntax, operational semantics, and meta-theory, has been mechanized in Lean 4. The formalization consists of a core inductive type for the calculus (MirrorSystem) and a set of verified theorems that guarantee its core properties, such as its controlled, three-step reaction to paradox. The project serves as a case study in using Lean 4 not just for verifying existing mathematics, but for designing, prototyping, and proving the correctness of novel computational models from the ground up.
I will walk through the core definitions, demonstrate the paradox resolution cycle with a runnable example, and briefly discuss the main theorems. This work aims to inspire discussion on using Lean as a tool for exploring foundational questions in AI and the theory of computation.
11:00-11:20: Mauricio Barba da Costa, Automatic Geometry Theorem Proving Using Polynomial Elaboration
Geometric reasoning is a unique domain of mathematics because it often requires diagrammatic reasoning. While much prior work has attempted to port Euclidean geometric theorems into Mathlib, the current EuclideanGeometry library remains slim. We make two contributions: (1) AlgebraicEuclid, a domain-specific language written in Lean 4 for expressing geometry theorems and (2) a tactic, algebraic_euclid, that automatically elaborates geometry theorems into systems of polynomial equations and solves them using Lean’s grind tactic. We formalize close to 100 existing theorems in the AlgebraicEuclid DSL, many of which are not yet in Mathlib, showing that this tool could greatly increase the corpus of the library’s geometry theorems. This is joint work with Fabian Zaiser, Cameron Freer, Katie Collins, Josh Tenenbaum, and Vikash Mansinghka.
Consider the following statement in AlgebraicEuclid, which expresses the converse of the Pythagorean Theorem.
theorem Proposition48
(h1 : |C - B|^2 = |B - A|^2 + |C - A|^2) :
(B - A) ⊥ (C - A) := by
algebraic_euclid
Because the definitions of lengths and orthogonality have been carefully constructed algebraically, the algebraic_euclid tactic can elaborate this statement into a system of polynomial equations:
\((C.x - B.x)^2 + (C.y - B.y)^2 =\) \((B.x - A.x)^2 + (B.y - A.y)^2 + (C.x - A.x)^2 + (C.y - A.y)^2 \rightarrow\) \((B.x - A.x) * (C.x - A.x) + (B.y - A.y) * (C.y - A.y) = 0\)
With this new representation, we can apply the Gröbner basis module of Lean’s grind tactic to automatically prove the geometry theorem.
Other prior work has also developed automatic methods for proving geometry theorems. For instance, JGEX is an application that offers a graphical user interface designed for expressing geometric theorems and proving them using a suite of techniques including deductive database methods and polynomial solvers. Even though the tool was developed decades ago, it continues to be used, for instance, for proving geometry IMO problems. Our work is novel in that it implements automatic geometric theorem proving in Lean 4, enabling formally verified correctness guarantees, facilitating the addition of new geometry theorems to Mathlib, and unsiloing many geometry theorems that had previously only been aggregated in JGEX. Further, AlgebraicEuclid supports several definitions and predicates such as angles, lengths, and concyclicity. Thanks to formalizations in Lean, we also discovered a soundness issue in JGEX: due to inconsistencies in the encoding, the equality of angles fails to be transitive.
Moreover, Mathlib’s geometry library is built on an algebraic foundation, in contrast with other Euclidean geometry projects in Lean that are based on synthetic axiomatizations. This has prevented the inclusion of many significant theorems found in external libraries. Our method can be integrated into the EuclideanGeometry library in Mathlib, allowing us to add many theorems not yet present, such as Pappus’ Theorem and Stewarts’ Theorem, which have a one-line proof in our framework.
11:20-11:40: Moritz Firsching, The Formal Conjectures repo (online)
Formal Conjectures is a growing collection of mathematical statements formalized in Lean. We explain the motivation behind this initiative and give an overview of the current scope and content of the Formal Conjectures repository, discussing the types of mathematical statements included and the criteria for their selection. The primary focus of our collection is on formalized statements with no (formal or informal) proof available. We will address the unique challenges encountered and the lessons learned during the process of accurately translating informal statements.
11:40-12:00: Lukas Gerlach, Formalizing Possibly Infinite Trees of Finite Degree
Lean does not support coinductive types directly, which makes formalizing infinite lists and infinite trees quite non-trivial. In one of our projects, where we work on formalizing essential properties of the so-called chase algorithm, we encounter exactly this problem. The chase is a bottom-up materialization procedure used in database theory and knowledge representation to reason with a first-order logic fragment called “tuple-generating dependencies” or “existential rules”. If disjunctions are allowed in such rules, the chase can be represented as a (possibly) infinite tree of finite degree. This creates the need for a general Lean formalization of such trees, which we provide in a small standalone library. In this talk, we reproduce the idea and present the tree definition from scratch. For characterizing termination behavior of the chase algorithm, we want to prove (among other things) that termination of each branch of the chase tree implies that there are only finitely many branches. Consequently, we show König’s Lemma for the general tree formalization as one of the main technical results of our infinite tree library.
12:00-12:30: Yulu Pan, Verifying a real-world regex implementation
We present lean-regex, a regular expression engine implemented and formally verified in Lean 4. Our goal is a practical, “ordinary” regex library, offering the features programmers expect, backed by machine-checked proofs of correctness. The engine parses a regex syntax using total parser combinators, compiles expressions to Nondeterministic Finite Automata (NFAs), and executes them via NFA simulation. The core of our work is an end-to-end proof of soundness and completeness, guaranteeing the engine finds a match if and only if one exists according to the formal semantics. This proof correctly handles essential features like capture groups, anchors, and repetition. Following the RE2 model, lean-regex avoids features requiring exponential-time backtracking, providing linear-time matching (this complexity guarantee itself is not verified). This talk presents lean-regex as a case study in integrating formal verification with efficient, performance-oriented engineering. We will share lessons from optimizing the implementation, such as using arrays for O(1) NFA node access and proving the correctness of a prefilter optimization that speeds up search. Despite these efforts, the engine is currently about 7x slower than an NFA implementation in Rust (and more than 1000x slower than rust-lang/regex!), and we will discuss our roadmap for closing this gap. Beyond performance, a key open verification challenge is disambiguation: policies like greedy semantics uniquely determine which match to return. While our library intends to provide greedy semantics, this is unverified and presents tricky edge cases ripe for formalization. Finally, we will reflect on the experience of building such a system in Lean. We’ll highlight its strengths, a smooth combination of programming and proving, expressive macros, and rich libraries, while also discussing the challenge of discovering unwritten “proof patterns” essential for productivity, such as using a ProofData-like structure to organize proofs. We want to invite the community to share more such patterns. While we already have excellent resources, there’s always room for more focused guidance that can make everyone’s Lean journey smoother.
16:00-16:20: Luc Duponcheel, Teaching Programming using Lean
I am working on a Lean based programming course, inspired by my progressive insight into what programming is all about.
What is special, both about Lean and about the course, is that the code of the course can be seen as a course for Lean itself!
Lean turns out to be a very demanding, but also very helpful student.
The course strictly separates program specifications from program implementations and corresponding program materializations.
The Lean binary type constructor classes involved specify what pointfree effectful functional programming is all about.
For more info about me and my talk: https://github.com/LucDuponcheelAtGitHub/PSBP.
I am a mathematics and functional programming veteran, nowadays mainly doing research as a hobby.
16:20-16:40: Jesse Alama, Euler’s polyhedron formula à la Lean
Euler’s polyhedron formula is the result that, for suitable polyhedra $p$, $V - E + F = 2$, where $V$, $E$, and $F$ are, respectively, the numbers of vertices, edges, and faces of $p$. More generally, the result asserts that the Euler characteristic $χ$ of a homological sphere $p$ of dimension $d$ equals $1 + (-1)^d$. We present a proof of Euler’s formula in Lean for arbitrary finite dimensions, leaning on Mathlib’s formalization of chain complexes and finite-dimensional linear algebra (rank-nullity theorems), and a number of hard-working type classes. I’ll give an overview of the formalization and sketch a program of further work in algebraic topology for Mathlib arising from Euler’s polyhedron formula.
16:40-17:00: Jovan Gerbscheid, Generalized Rewriting
I would like to talk about some contributions I have made to mathlib. In particular, the new grw tactic.
The rewrite tactic, rw, is the most used tactic in mathlib, so it should come as no surprise that grw, the generalized version of rw, is also a very useful tactic. Instead of rewriting with equalities (or if-and-only-if), grw can rewrite using any binary relation.
In 2023, various people, including me, had independently developed some version of a generalized rewriting tactic. However, it took until 2025 when I picked this project back up before a grw implementation got merged into mathlib.
The most used relation for generalized rewriting is ≤ (less than or equal to), but many more relations can be used, for example
<, less than (which does the same as ≤)→, implication⊆, subset∣, divisibility≡ [ZMOD n], congruence modulo n=ᶠ[ae μ], almost everywhere equality w.r.t. a measure μThe basic idea is that many functions are monotone or antitone in some of their arguments. For example the expression a - b becomes bigger if we make a bigger, and it becomes smaller if we make b bigger. This fact is proved by the lemma sub_le_sub : a ≤ b → c ≤ d → a - d ≤ b - c, and it is an example of a generalized congruence lemma. The generalized congruence tactic, gcongr, solves goals by iteratively applying these kinds of generalized congruence lemmas. grw works by first determining how to rewrite, and then calling gcongr to prove that the rewrite is valid. For example to rewrite using s ⊆ t in the goal s.Nonempty, it calls gcongr to prove that s.Nonempty → t.Nonempty. This always uses the implication relation →.
To tell gcongr/grw about generalized congruence lemmas, they need to be tagged with @[gcongr], and many such lemmas have been tagged in mathlib. gcongr lemmas can also have side conditions, such as for multiplication: a * b is only monotone in b if a is non-negative. These side conditions may be automatically discharged by the positivity tactic, or otherwise left as new goals to be proved.
Despite being very useful already, there are still many things we would like the grw tactic to be able to do in the future:
-2 * _, not just 2 * _.gcongr.gcongr to use a mix of congr and gcongr lemmas, so that it can reason better about the equality relation =.<, if the goal is of the form _ < _, we might want the goal to change to _ ≤ _, and vice versa in a hypothesis.17:00-17:30: Chase Norman, Canonical: simplify, monomorphize, destruct.
Canonical is a type inhabitation solver for dependent type theory, which can be invoked as a Lean tactic to prove theorems, synthesize programs, and construct objects.
In our ITP 2025 paper, we describe the process of encoding a Lean goal as a type inhabitation problem for Canonical. However, this basic encoding not account for three major subsystems of Lean: the simplifier, the typeclass inference system, and the structure environment extension. Over the past few months, the Lean tactic for Canonical has undergone great changes to support these systems, and ulitmately become more useful in a variety of contexts.
Simplify: Many Lean proofs depend on the simplifier to reduce the complexity of the problem. At launch, Canonical only had support for definitional reductions involving recursors and projections. Canonical now supports arbitrary reduction rules, allowing simp lemmas and equation compiler lemmas to be applied pervasively during search. When a proof using these reductions is found, it is converted into appropriate invocations of the simp tactic. This allows Canonical to reason more effectively about equalities, and eliminates the need to unfold all functions down to the level of recursors and projections.
Monomorphize: The typeclass inference system is essential for filling instance-implicit arguments of any Lean term. It is imperative that Canonical not be bogged down with reasoning about instances and their implementations. We released a new tactic monomorphize which eliminates typeclass instances from a problem. It does so by rewriting the goal in terms of local declarations that are already specialized to specific typeclass instances. The techniques used to determine which instances should be used are quite sophisticated, allowing them to be resolved in almost all cases.
Destruct: We released another new tactic, destruct, which eliminates structure types from a goal. Premises that are structure types are converted into multiple premises, and goals that are structure types are converted into multiple goals. Functions that return structure types are converted into functions that return each component. Even existential quantifiers can be unpacked, as in skolemization. This pre-processing stage greatly improves the fidelity of Canonical in reasoning about structure types.
The encodings produced by these new features are much more amenable to search-based automated theorem proving. This allows Canonical to be more applicable in a wider range of scenarios. Continued development on this front will be necessary to make proof search more effective for Lean.
25 August 2025 (UTC): ITP early registration deadline
8 September 2025 (AoE): Submission deadline
11 September 2025: Author notification
13 September 2025 (UTC): ITP late registration deadline
As the workshop is affiliated with ITP, attendees are required to register for the workshop through ITP registration. The workshop (as well as the conference) can be attended either online or in person. Please consult the ITP registration page for pricing information.
We will be using a lightweight submission and review process. Talk proposals should take the form of a plaintext or markdown abstract (100-500 words).
Proposals can be for short talks (20 minutes) or long talks (30 minutes), and proposals should include your preferred length (but we may not be able to satisfy all requests).
Relevant subject matter includes but is not limited to:
Workshop website: https://leanprover-community.github.io/itp-2025-lean-workshop/
Submission: Submit by email to: