Mathematics in Lean session at ICMS 2026

Stream: general

[Rémy Degenne]

Discussion thread for #announce > Mathematics in Lean session at ICMS 2026

[Rémy Degenne]

I'd like to advertise a second (and last) time the Mathematics in Lean session at ICMS 2026.
We have extended the deadline of short abstracts to match the one shown on the ICMS main page: it is now March 1.

Dear colleagues,

We invite submissions of short abstracts (≈200 words) for contributed talks in the Mathematics in Lean session at ICMS 2026 (20–23 July, Waterloo, Canada). The session focuses on all aspects of doing, formalizing, and supporting mathematics in the Lean theorem prover and its mathematical library Mathlib.

Topics of interest include:

• Formalization of mathematical theories
• Developments in Mathlib
• Tools and automation for Lean
• Interactions with other proof assistants or CAS
• Educational uses and case studies of Lean in research or teaching

Deadline for short abstract submission: March 1, 2026.

Talks follow the ICMS format (25+5 minutes). Accepted abstracts are posted on the session website as they are received.

Note: this is an in-person event and we expect physical attendance at the conference.

To submit an abstract or ask questions, please contact any of the organizers:
Matthew Ballard , Rémy Degenne , Damiano Testa .

We look forward to your contributions!