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.
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.
8 September 2025 (AoE): Submission deadline
15 September 2025: Author notification
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: