SMS Spring Meeting: Formalization and Proof Assistants

UniDistance will be hosting a 3-day workshop (Wednesday 25th-Friday 27th March 2026) on “Formalization and Proof Assistants”. This is combined with the spring meeting of the Swiss Mathematical Society on the afternoon of Friday 27th.

Proof assistants, such as Lean, Isabelle, and Coq, are software systems for checking the correctness of mathematical proofs. They have now advanced to the point that “ordinary” mathematicians (without specialist training in logic or computer science) can easily learn to write proofs that the computer can check; and recently AI systems, such as AlphaProof, Gauss and Aristotle, have been developed which can automatically generate formally-verified proofs. In this conference, we'll be hearing from experts in both interactive and automated theorem proving.

Speakers

David Angdinata (University of East Anglia)
Oliver Dressler (FFHS / Math, Inc.)
Floris van Doorn (Bonn University)
Manuel Eberl (Innsbruck University)
Moritz Firsching (Google)
Sidharth Hariharan (Carnegie Mellon University)
Sina Hazratpour (Cambridge University)
Chi-Yun Hsu (Santa Clara University)
Stefan Kebekus (Freiburg University
Alessandro Iraci (Università Telematica Pegaso)
Auguste Poiroux (EPFL / Math, Inc.)
Michael Stoll (Universität Bayreuth)
Hang Lu Su (ICMAT Madrid)
Johannes Überberg (MathGarden)
Maryna Viazovska (EPFL)
Goran Zuzic (Google)

Abstracts

For any questions, please contact david.loeffler@unidistance.ch.

In partnership with

Schedule

Wednesday

8.45 - 9.30	[Welcome & Coffee]
9.30 - 10.00	David Loeffler, "First steps in formalization I: what is formalization?"
10.15 - 11.00	Moritz Firsching, "The Formal Conjectures Project"
	[Break]
11.30 - 12.15	Stefan Kebekus, "Project VD: Formalizing Value Distribution Theory"
	Lunch on campus
13.30 - 14.15	Goran Zuzic, "AlphaProof: RL for Math, Gold Medals for Gemini, and Beyond"
14.30 - 15.15	Chi-Yun Hsu, "Bijective vs Analytic: Formalizing Euler’s Partition Identity"
	[Break]
15.45 - 16.30	Oliver Dressler, "lean-lsp-mcp: A toolbox for agents to interact with Lean"
16.45 - 17.30	Sina Hazratpour, "Formalization of polynomial functors in Lean 4"

-

Thursday

9.30 - 10.15	Michael Stoll, "Heights in arithmetic geometry"
10.30 - 11.15	David Angdinata, "Torsion subgroups of elliptic curves in Lean"
	[Break]
11.45 - 12.15	Manuel Eberl, "First steps in formalization II: intro to Isabelle"
	[Lunch on campus]
13.30 - 14.15	Alessandro Iraci, "Machine Discovery in Combinatorics"
14.30 - 15.15	Hang Lu Su, "Formalizing finitely presented groups"
	[Break]
15.45 - 16.30	Johannes Überberg, "Naivle: A Proof Verification System for Textbook-Style Mathematics"
16.45 - 17.30	Manuel Eberl, "Formalising Complex Analysis in Isabelle/HOL"

-

Friday

9.15 - 9.45	David Loeffler, "First steps in formalization III: using AI"
10.00 - 10.45	Maryna Viazovska
	[Coffee break]
11.15 - 12.00	Sidharth Hariharan, "Formalising Sphere Packing"
	[Lunch on campus]
13.15 - 14.00	Auguste Poiroux, "Autoformalization of the strong Prime Number Theorem"
	[Break]
14.30 - 15.30	Colloquium talk: Floris Van Doorn, "Lean: Collaboration using Formalization"
	[Break]
16.00 - 18.00	Swiss Mathematical Society General Assembly // Poster session
From 17.45	Drinks Reception