Loading...
Organizing Committee
Brown University
Southern Illinois University Edwardsville
Imperial College London
Université Paris-Saclay at Orsay
UCLA
Abstract
Formalization of mathematics is the process by which pen-and-paper mathematics is translated into a strict chain of logical deductions down to the axioms of mathematics. The subject has seen renewed interest in the last decades thanks to the development of computer systems called proof assistants, which make this feasible in practice.
There have now been several examples of high-profile mathematical results which have been formalized. In principle, any mathematical domain is accessible. However, existing projects are skewed towards algebra instead of analysis. Notable exceptions are a project which formalized enough of Gromov’s convex integration theory to deduce Smale’s sphere eversion theorem and the ongoing project to formalize Carleson’s convergence theorem for Fourier series.
This workshop will bring together formalization experts and interested mathematicians to give a new impulse to formalization of analysis (in a very broad sense), and to develop abstractions and tools to deduplicate effort.
The deadline to apply for this workshop has been extended to January 24, 2026
There have now been several examples of high-profile mathematical results which have been formalized. In principle, any mathematical domain is accessible. However, existing projects are skewed towards algebra instead of analysis. Notable exceptions are a project which formalized enough of Gromov’s convex integration theory to deduce Smale’s sphere eversion theorem and the ongoing project to formalize Carleson’s convergence theorem for Fourier series.
This workshop will bring together formalization experts and interested mathematicians to give a new impulse to formalization of analysis (in a very broad sense), and to develop abstractions and tools to deduplicate effort.
The deadline to apply for this workshop has been extended to January 24, 2026
Loading...
Loading participant list in background...
Workshop Schedule
Monday, May 11, 2026
8:30 - 8:50 AM EDT
Check In
11th Floor Collaborative Space
8:50 - 9:00 AM EDT
Welcome from ICERM Director
Welcome - 11th Floor Lecture Hall
Brendan Hassett, ICERM/Brown University
9:00 - 9:15 AM EDT
Organizer Welcome
Welcome - 11th Floor Lecture Hall
Javier Gomez Serrano, Brown University
Jireh Loreaux, Southern Illinois University Edwardsville
Heather Macbeth, Imperial College London
Patrick Massot, Université Paris-Saclay at Orsay
Terence Tao, UCLA
9:15 - 10:00 AM EDT
Analysis for classical differential geometry
11th Floor Lecture Hall
Speaker
Oliver Nash, Mathlib Initiative
Session Chair
Patrick Massot, Université Paris-Saclay at Orsay
Abstract
Using some results from classical differential geometry, I will collect a wish list of necessary analytical results. I will also explore which of these already exist within Mathlib, which are close, and speculate on how we might approach those that are not.
10:15 - 10:45 AM EDT
Coffee Break
10th Floor Collaborative Space
11:00 - 11:45 AM EDT
Towards the formalisation of PDEs in analysis
11th Floor Lecture Hall
Speaker
Michael Rothgang, Universität Bonn
Session Chair
Patrick Massot, Université Paris-Saclay at Orsay
Abstract
I will give an overview of the state of formalising differential equations in mathlib: while results about PDEs themselves are still in its infancy, the ODE side looks much better, and many prequisites about PDEs are coming into place right now. I will comment on some challenges for formalisation in analysis and what we can do to improve the situation. As a concrete example, I will discuss the formalisation of Sobolev spaces (using classical distributions and weak derivatives); this is ongoing work with Filippo Nuccio and Floris van Doorn.
12:00 - 12:45 PM EDT
The Sobolev embedding theorem via Fourier analysis
11th Floor Lecture Hall
Speaker
Moritz Doll, University of Melbourne
Session Chair
Patrick Massot, Université Paris-Saclay at Orsay
Abstract
We report on progress formalizing the basics of Sobolev spaces based on Fourier analysis using tempered distributions. This formalization includes a simple version of the Sobolev embedding theorem and the trace theorem, as well as elementary mapping properties of constant coefficient differential operators. The main challenge in the formalization is to define various objects on different spaces and find the right abstractions and notations to maintain readability and to avoid code duplication.
1:00 - 2:30 PM EDT
Lunch/Free Time
2:30 - 3:30 PM EDT
Open Problems Discussion Session
Problem Session - 11th Floor Lecture Hall
Session Chair
Terence Tao, UCLA
3:30 - 4:00 PM EDT
Coffee Break
11th Floor Collaborative Space
4:00 - 5:00 PM EDT
Group Work
Assigned group work locations
5:00 - 6:30 PM EDT
Reception
11th Floor Collaborative Space
Tuesday, May 12, 2026
9:00 - 9:45 AM EDT
Formalizing de Rham cohomology in Lean
11th Floor Lecture Hall
Speaker
Yury Kudryashov, Harmonic
Session Chair
Jireh Loreaux, Southern Illinois University Edwardsville
Abstract
I will discuss the current progress of formalizing de Rham cohomology in Lean. As this is an ongoing project, I will cover the milestones achieved, the objectives currently within reach, and the specific challenges we have encountered.
10:00 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:15 AM EDT
Spaces of classical distributions and locally convex spaces in Mathlib
11th Floor Lecture Hall
Speaker
Anatole Dedecker, Université Paris-Cité
Session Chair
Jireh Loreaux, Southern Illinois University Edwardsville
Abstract
The formalization of the theory of locally convex vector spaces in Mathlib was launched in 2022, when Moritz Doll and I formalized the two standard definitions. From the very beginning, we intended to use it to start working on the theory of distributions (tempered and classical). I will start by giving an overview of what Mathlib knows about locally convex spaces and outlining some plans for future projects. I will then describe joint work with Luigi Massaci where, starting from the general theory, we defined the space of vector-valued classical distributions, and proved continuity of the differentiation of distributions. A key objective of the talk will be to outline the many design choices in this area of Mathlib, with the hope to help the audience understand the API.
11:30 AM - 12:15 PM EDT
Computing Derivatives
11th Floor Lecture Hall
Speaker
Tomas Skrivan, SideFX
Session Chair
Jireh Loreaux, Southern Illinois University Edwardsville
Abstract
This talk presents an upcoming extension to the tactic `fun_prop` that is capable of computing derivatives. More generally, `fun_prop` gains the ability to solve goals with metavariables like `HasFDerivAt k f ?f' x` by finding the appropriate derivative `f'` and providing a proof that it is indeed the derivative. We will show how to correctly set up `fun_prop` for `HasFDerivAt`, demonstrate its usage on simple and more advanced derivative computations, and show how to extend `simp` to simplify expressions involving `fderiv`.
At the end, we will discuss how to compute gradients using `HasGradientAt` and point out certain technical difficulties preventing us from actually using `fun_prop` in this case. These difficulties can be mitigated and they have been as part of PhysLib. If time allows, we will briefly discuss the formalization of variational calculus in PhysLib, such as the derivation of Euler-Lagrange equations, and what it would take for `fun_prop` to fully automate these calculations as well.
12:30 - 2:00 PM EDT
Lunch/Free Time
2:00 - 2:45 PM EDT
ODEs and Integral Curves on Manifolds
11th Floor Lecture Hall
Speaker
Winston Yin, UC Berkeley
Session Chair
Jireh Loreaux, Southern Illinois University Edwardsville
Abstract
I will give an overview of the current state of ODE theory in Mathlib and a mirrored theory for integral curves on manifolds. I will share some insights from the ongoing formalisation of the smoothness theorem for flows of ODEs, as well as some exciting developments in AI-assisted autoformalisation and library management.
3:00 - 5:00 PM EDT
Group Work
Assigned group work locations
3:30 - 4:00 PM EDT
Coffee Break
11th Floor Collaborative Space
Wednesday, May 13, 2026
9:00 - 9:45 AM EDT
How to design tools for formalization
11th Floor Lecture Hall
Speaker
Robert Lewis, Brown University
Session Chair
Heather Macbeth, Imperial College London
Abstract
One activity at this meeting will be to brainstorm tools (broadly construed) that will help with the formalization of analysis. Tools are not themselves formal proofs in Lean; often they take the form of *metaprograms*, pieces of code that interact with Lean expressions in various ways. (Tactics are the most familiar kind of metaprogram to most Lean users.) In this talk I will introduce the basic components of a Lean metaprogram and describe different tactic design strategies, including proof by reflection and proof by certificate. Better understanding of the basic building blocks of Lean tooling will help brainstorm new ideas and applications.
10:00 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:15 AM EDT
TBA
11th Floor Lecture Hall
Speaker
Bogdan Georgiev, Google Deepmind
Session Chair
Heather Macbeth, Imperial College London
11:30 AM - 12:15 PM EDT
Obstacles and opportunities in the formalization of operator algebras
11th Floor Lecture Hall
Speaker
Jireh Loreaux, Southern Illinois University Edwardsville
Session Chair
Heather Macbeth, Imperial College London
Abstract
Operator algebras, and functional analysis more generally, is still in early stages with regards to formalization. In some aspects we have made reasonable progress, but in others we are stymied by various obstacles. We will highlight some of these successes and difficulties and discuss how we might turn these into opportunities to improve the library, especially places where bespoke tactics may be particularly effective.
12:25 - 12:30 PM EDT
Group Photo (Immediately After Talk)
11th Floor Lecture Hall
12:30 - 2:30 PM EDT
Lunch/Free Time
2:30 - 5:00 PM EDT
Group Work
Assigned group work locations
3:30 - 4:00 PM EDT
Coffee Break
11th Floor Collaborative Space
Thursday, May 14, 2026
9:00 - 9:45 AM EDT
Complex Analysis in PNT+ and Real Analysis as a Game
11th Floor Lecture Hall
Speaker
Alex Kontorovich, Rutgers University
Session Chair
Patrick Massot, Université Paris-Saclay at Orsay
Abstract
We will discuss some lessons learned from the PNT+ Project (complex analysis, large collaborative formalization, interactions with AI systems), and the Real Analysis Game (pedagogical aspects, technical aspects).
10:00 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:15 AM EDT
Formally verifying numerics for differential equations
11th Floor Lecture Hall
Speaker
Bhavik Mehta, Imperial College London
Session Chair
Patrick Massot, Université Paris-Saclay at Orsay
Abstract
The method of radii polynomials provides rigorous proofs for solutions of ODEs and PDEs by combining numerical solutions with interval arithmetic and the Banach fixed-point theorem. We present an ongoing project towards a general Lean framework for formally verifying these proofs. Joint work with Heather Macbeth and Mario Carneiro.
11:30 AM - 12:30 PM EDT
Group Work
Assigned group work locations
12:30 - 2:30 PM EDT
Lunch/Free Time
2:30 - 5:00 PM EDT
Group Work
Assigned group work locations
3:30 - 4:00 PM EDT
Coffee Break
11th Floor Collaborative Space
Friday, May 15, 2026
9:00 - 9:45 AM EDT
Autoformalization at Scale
11th Floor Lecture Hall
Speaker
Jared Duker Lichtman, Stanford University
Session Chair
Javier Gomez Serrano, Brown University
Abstract
Autoformalization has seen remarkable progress very recently. In particular, Math, Inc’s agent Gauss has scaled up code generation by three orders of magnitude in the past year. Notably, Gauss assisted Viazovska-Hariharan’s led team to formalize the Fields Medal proof of Sphere Packing in dimensions 8. In the subsequent week, Gauss autoformalized dimension 24, as the single largest Lean proof in history. We are also pleased to share OpenGauss as an open-source tool for the community.
10:00 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:15 AM EDT
Formalizing variation estimates for commuting transformations
11th Floor Lecture Hall
Speaker
Floris van Doorn, University of Bonn
Session Chair
Javier Gomez Serrano, Brown University
Abstract
An important question studied in Ergodic theory is the time average behavior of transformation on a measure space. A generalization of this considers multiple pairwise commuting transformations of a space, for which pointwise convergence is still an open conjecture, but for the weaker notion of norm convergence this is known. Variation estimates of norms give a notion that is weaker than pointwise convergence, but stronger than convergence in norm, and it is an ongoing project to prove variation estimates for commuting transformations.
In this talk, I will describe progress towards formalizing these variation estimates for commuting transformations. This will require tools from analysis such as multilinear interpolation theory, the Calderón transference principle, and some refactors of Mathlib.
11:30 AM - 12:15 PM EDT
The Integrated Explicit Analytic Number Theory Network : a progress report
11th Floor Lecture Hall
Speaker
Terence Tao, UCLA
Session Chair
Javier Gomez Serrano, Brown University
Abstract
We report on the ongoing Integrated Explicit Analytic Number Theory Network (IEANTN) project (hosted as part of the Prime Number Theory and More (PNT+) project), which aims to formalize and combine a large number of results in explicit analytic number theory into a unified artefact that allows for bounds to be updated and propagated by AI-assisted, formally verified means in an automated, near-real-time fashion.
Request Reimbursement
This section is for general purposes only and does not indicate that all attendees receive funding. Please refer to your personalized invitation to review your offer.
- ORCID iD
- As this program is funded by the National Science Foundation (NSF), ICERM is required to collect your ORCID iD if you are receiving funding to attend this program. Be sure to add your ORCID iD to your Cube profile as soon as possible to avoid delaying your reimbursement.
- Acceptable Costs
- 1 roundtrip between your home institute and ICERM
- Flights on U.S. or E.U. airlines – economy class to either Providence airport (PVD) or Boston airport (BOS)
- Ground Transportation to and from airports and ICERM.
- Unacceptable Costs
- Flights on non-U.S. or non-E.U. airlines
- Flights on U.K. airlines
- Seats in economy plus, business class, or first class
- Change ticket fees of any kind
- Multi-use bus passes
- Meals or incidentals
- Advance Approval Required
- Personal car travel to ICERM from outside New England
- Multiple-destination plane ticket; does not include layovers to reach ICERM
- Arriving or departing from ICERM more than a day before or day after the program
- Multiple trips to ICERM
- Rental car to/from ICERM
- Flights on a Swiss, Japanese, or Australian airline
- Arriving or departing from airport other than PVD/BOS or home institution’s local airport
- 2 one-way plane tickets to create a roundtrip (often purchased from Expedia, Orbitz, etc.)
- Travel Maximum Contributions
- New England: $350
- Other contiguous US: $850
- Asia & Oceania: $2,000
- All other locations: $1,500
- Note these rates were updated in Spring 2023 and supersede any prior invitation rates.
- Reimbursement Requests
Request Reimbursement with Cube
Refer to the back of your ID badge for more information. Checklists are available at the front desk and in the Reimbursement section of Cube.
- Reimbursement Tips
- Scanned original receipts are required for all expenses
- Airfare receipt must show full itinerary and payment
- ICERM does not offer per diem or meal reimbursement
- Allowable mileage is reimbursed at prevailing IRS Business Rate and trip documented via Google Maps PDF
- Keep all documentation until you receive your reimbursement!
- Reimbursement Timing
6–8 weeks after all documentation is sent to ICERM. All reimbursements are reviewed by multiple Brown University offices.
- Reimbursement Deadline
Submissions must be received within 30 days of ICERM departure to avoid applicable taxes. No submissions are accepted after six months.