SMS Spring Meeting: Formalization and Proof Assistants

Name: SMS Spring Meeting: Formalization and Proof Assistants
Start: 2026-03-25T09:15:00+01:00
End: 2026-03-27T18:00:00+01:00

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

Registration form

Please fill in the form below to register for the workshop and/or SMS General Assembly

Your contact details

Your name *

Your email address *

University or other affiliation *

I wish to attend:

The 3-day "formalization and proof assistants" workshop

Only the Friday afternoon (featuring a colloquium talk by Floris Van Doorn and the SMS General Assembly)

Travel and lodging

Note that the meeting will start at 9.30am Wed 25th March, and finish at approx 6pm on Fri 27th.

Planned arrival date *

Planned departure date *

(We regret that we are unable to offer financial support for participants registering after 1st March.)

Scientific programme

How familiar are you with proof assistants? *

Would you be interested in giving a talk? *

Yes

No

Summary of proposed talk topic (max 300 characters)

SMS Spring Meeting: Formalization and Proof Assistants

SMS Spring Meeting: Formalization and Proof Assistants

Speakers

Abstracts

Schedule

-

-

Registration form

Your contact details

Travel and lodging

Scientific programme

Information webinar on the Bachelor of Science in Mathematics programme

50 years in probability - A workshop in honor of Erwin Bolthausen

3rd Brig Workshop on Dissipativity in Systems and Control

Number Theory Seminar: Abinhandan

Number Theory Seminar: Martin Ortiz

Number Theory Seminar: Luca Mastella

Information webinar on the Master of Science in Artificial Intelligence

Flowers: A Warp Drive for Neural PDE Solvers

Ignacio Muñoz Jiménez: Gross points in ordinary families of Hilbert modular forms