We are pleased to invite you to submit presentation proposals for the ITP 2025 Lean Workshop, which will be held in Reykjavik, Iceland on 2 October 2025, as a satellite to the ITP conference, a member of the larger FroCoS/ITP/TABLEAUX ‘25 gathering.
This is the first time we have had a Lean Workshop at ITP, and we’re excited to see it develop. It brings together developers, contributors, and users of Lean and Mathlib.
The Lean Workshop aims to create a friendly and welcoming space where community members can connect, share experiences, and support one another. Whether you’re a seasoned contributor or just getting started with Lean, we encourage participation from all backgrounds and experience levels. The workshop fosters an open atmosphere where newcomers can learn from the community, experienced users can share their knowledge, and everyone can build lasting connections. Rather than serving as a venue for traditional research papers, the Lean Workshop is organized around informal presentations and discussions, supplemented with invited talks.
25 August 2025 (UTC): ITP early registration deadline
8 September 2025 (AoE): Submission deadline
11 September 2025: Author notification
13 September 2025 (UTC): ITP late registration deadline
As the workshop is affiliated with ITP, attendees are required to register for the workshop through ITP registration. The workshop (as well as the conference) can be attended either online or in person. Please consult the ITP registration page for pricing information.
We will be using a lightweight submission and review process. Talk proposals should take the form of a plaintext or markdown abstract (100-500 words).
Proposals can be for short talks (20 minutes) or long talks (30 minutes), and proposals should include your preferred length (but we may not be able to satisfy all requests).
Relevant subject matter includes but is not limited to:
Workshop website: https://leanprover-community.github.io/itp-2025-lean-workshop/
Submission: Submit by email to: