ABSTRACT. LLM coding agents are already highly capable Lean copilots, but using them effectively on a large formalization requires more than a strong model. They may reprove existing Mathlib lemmas, miss feedback from Lean’s elaborator, introduce fragile local workarounds, or continue pursuing proof paths that have stopped making progress. In this talk I will describe `lean4-skills`, a toolkit for Lean coding agents that combines prompts, references, workflows, and tool-use guidance intended to make such agents easier to steer. The toolkit works at three levels. First, it includes Lean-specific prompting and reference material that records conventions, useful patterns to follow, and recurring pitfalls to avoid. Examples include searching before proving, carefully managing competing typeclass instances, and preferring established Mathlib idioms over ad hoc local alternatives. Second, it adds control-flow structure through slash commands, subagents, hooks, and scripts. These organize common tasks such as drafting formal statements, proving, reviewing, refactoring, golfing, and checkpointing into more explicit workflows, with bounded proof attempts and natural opportunities for human review. Third, it helps agents make systematic use of `lean-lsp-mcp`, which exposes both Mathlib search methods and Lean language-server information, allowing agents to inspect goal states, read diagnostics, use hover text, and test tactics analogously to the feedback loop available to humans in the Lean InfoView. I will discuss how I initially developed `lean4-skills` in tandem with a large AI-assisted formalization of de Finetti's theorem. The recurring difficulties that I encountered there, especially those involving conditional expectation, σ-algebra bookkeeping, avoiding elaboration timeouts, and Mathlib discovery, provided many of the example patterns and antipatterns that were later distilled into reusable guidance. The toolkit also includes a `learn` workflow for interactive teaching and Mathlib exploration. This helps keep the user involved when agents fill in more of the proof-writing, by making it easier to ask what the agent is doing, why a lemma applies, and how the surrounding Lean infrastructure is organized. It can also support informal mathematical learning, using Mathlib and the local development as checked sources of definitions and theorems, and using Lean to test formal versions of claims before explaining them informally. More broadly, improving AI assistance for Lean is not only a matter of using stronger models. It also requires shared practical knowledge about how Lean formalization proceeds: what to look up, how to interpret common errors, when to inspect the goal state, when to stop and replan, and which proof patterns tend to survive review. Through open projects like `lean4-skills`, the Lean community can benefit from treating this kind of agent-facing guidance as shared infrastructure rather than project-specific prompting notes. https://github.com/cameronfreer/lean4-skills Format: Long talk, 30 minutes

ABSTRACT. At ITP 2025, I introduced Canonical, a type inhabitation solver for dependent type theory, and an associated Lean tactic. But, how do you go about implementing such an algorithm? How does Canonical tame the combinatorial explosion, and why does it need a new representation of types and terms? How can Canonical be complete in the face of undecidable unification? To answer these questions, I developed Canonical-min, a simplified implementation of the core algorithm in 185 lines of Lean code. In this talk, I'll show that type inhabitation is easy if you look at it from the right perspective. What makes Canonical-min so special is its deep integration of Lean's monadic functional programming paradigm. The most important part of Canonical-min, the type checker, appears simple at a mere 18 lines. However, under the continuation monad, it becomes the core solver component which defines the search tree, enforcing all typing and unification constraints. I hope that Canonical-min (and this talk) can help foster understanding of general proof automation in dependent type theory, can help serve as the basis for the development and extension of the technique, and can one day lead to the formal verification of the algorithm. I am requesting 30 minutes for my talk.

ABSTRACT. Detailed and rigorous specifications of programming languages are highly valuable, since they facilitate precise reasoning about program behaviours and language properties. However, many mainstream languages remain unspecified, or are only specified in prose, which can be ambiguous and error-prone. We argue that this is partly due to a lack of good tooling for creating programming language specifications. Ideally, such tools should make the creation of specifications easier by automatically generating boilerplate and detecting inconsistencies, while also producing useful artifacts such as parsers, documentation, and proof assistant definitions. Though existing tools such as [Ott](https://github.com/ott-lang/ott) and [Lem](https://github.com/rems-project/lem) address some of these needs, they all have notable limitations. This talk introduces a new specification tool, currently in development, built using Lean’s metaprogramming features. Our tool enables users to define syntax through grammars and semantics via judgments, which are then automatically transformed into Lean inductive types and LaTeX figures for documentation. It also provides automated support for handling the complexities of variable binding. By leveraging Lean's metaprogramming capabilities, we achieve a high degree of integration that eliminates external dependencies and provides real-time error reporting by Lean's editor integration. Finally, we will discuss our roadmap for an enhanced version of the tool. A primary focus is extensibility, both in terms of the tool's architecture and the specifications themselves. By incorporating modularity principles from prior proof assistant research, we aim to allow users to extend and combine specifications, a crucial requirement for modeling modular architectures such as RISC-V and MLIR. (Preferred length: 30 minutes, though this isn't a strong preference.)

ABSTRACT. Nonlinear real arithmetic is a fundamental theory for modeling real world systems, but it currently has very limited support in proof assistants due to the intricacy of its decision procedures. Existing Lean tactics can handle some nonlinear goals, but even in simpler cases, such as with univariate goals, it is often the case that no existing tactic alone can currently solve. We present a new tactic that addresses this gap for the univariate case by leveraging the SMT solver cvc5 through lean-smt. Our approach is based on Cylindrical Algebraic Decomposition (CAD), a classical decision procedure for the theory of real closed fields. In the univariate case, this procedure splits the real line in the intervals separated by the roots of the polynomials from the input and tries to find a solution to the problem in each one of them. We instrumented cvc5 so that, when it solves a univariate nonlinear problem using CAD, it produces a certificate that can be independently verified. The tactic uses this certificate to build a proof term for the original goal. This process relies on two key components: first, a computable library for real algebraic numbers (RANs) with support for comparing the magnitude of two RANs and computing the sign of a polynomial evaluated at a RAN. This library was necessary since our tactic requires these operations on roots of polynomials on a real variable, which can be represented as RANs. Second, a formalization of Sturm's theorem, which provides a method to count the real roots of a polynomial in any given interval, ensuring that all roots have been found by the solver. Together, these components allow us to verify that the solver's decomposition of the real line is correct and that the original constraints are unsatisfiable in each resulting interval. Beyond its use as a Lean tactic, this work also serves as an independent proof checker for cvc5 in this logical fragment. By reconstructing solver certificates in Lean's type theory, we can verify the correctness of cvc5's results without trusting its codebase, which comprises hundreds of thousands of lines of code. Since our tactic is built on top of lean-smt, it benefits from the broader infrastructure that lean-smt provides for interacting with cvc5. Goals that combine nonlinear real arithmetic with other theories for which cvc5 has support for producing proofs — such as uninterpreted functions and datatypes — can also be discharged. We will also discuss directions for extending this work to the multivariate case, where Cylindrical Algebraic Decomposition operates by projecting polynomials onto lower dimensions and lifting solutions back. We outline the main challenges that arise in reconstructing proofs for this setting and possible strategies for addressing them.

ABSTRACT. The Mathlib Initiative launched in September 2025. Our mission is to support the growth and maintenance Lean's Mathlib library, as well as the broader ecosystem and community. I will explain how the Mathlib Initiative came to be and how we are working to achieve these goals.

ABSTRACT. Drinfeld modules are a central object of study in the arithmetic of function fields. In this talk, I will present an ongoing project, joint with María Inés de Frutos Fernández, to formalize Drinfeld modules in Lean. In order to formalize the general definition of Drinfeld modules, we first needed to formalize a substantial amount of missing number-theoretic prerequisites. In this presentation, I will discuss the formalization hurdles encountered along the way, how they were solved, and the API design decisions required to build this foundational mathematics. Specific technical highlights of this work include: * The definition and development of `SkewMonoidAlgebra` and `SkewPolynomial`. * Formalizing fundamental results about function fields, including Ostrowski's theorem for $K(t)$. Beyond the specific case of Drinfeld modules, I will highlight how this project has served as a broader driver for library development, resulting in over 50 merged pull requests to `mathlib` to date. I will share insights from this journey that are applicable to anyone structuring large mathematical formalizations and developing comprehensive APIs in Lean 4.

ABSTRACT. We present a Lean library that uses effective transversality for certified root finding in multivariate polynomial systems. We formalize dyadic intervals, interval arithmetic, and a Newton-like method called the Krawczyk method, establishing their key correctness properties. Building on this foundation, we implement a recursive branch-and-bound algorithm that subdivides an initial interval vector to either isolate regions containing unique roots or certify the absence of roots. Finally, we introduce custom syntax and a tactic that automatically searches for suitable parameters to certify the existence, uniqueness, or non-existence of roots. (Short talk)

ABSTRACT. We formalize the Wu-Ritt characteristic set method for the triangular decomposition of polynomial systems in the Lean 4 theorem prover. Our development includes the core algebraic notions of the method, such as polynomial initials, orders, pseudo-division, pseudo-remainders with respect to a polynomial or a triangular set, and standard and weak ascending sets. On this basis, we formalize algorithms for computing basic sets, characteristic sets, and zero decompositions, and prove their termination and correctness. In particular, we formalize the well-ordering principle relating a polynomial system to its characteristic set and verify that zero decomposition expresses the zero set of the original system as a union of zero sets of triangular sets away from the zeros of the corresponding initials. This work provides a machine-checked verification of Wu-Ritt's method in Lean 4 and establishes a foundation for certified polynomial system solving and geometric theorem proving.