PhysLean: Digitalizing physics into Lean

Add to your list(s) Download to your calendar using vCal

• Joseph Tooby-Smith (Reykjavik University)
• Friday 17 October 2025, 16:00-17:00
• MR19 (Potter Room, Pavilion B), CMS.

If you have a question about this talk, please contact Nico Gubernari.

Lean is an interactive theorem prover, that is, a programming language in which you can write down mathematical definitions, theorems and their proofs, and it will use its mathematical foundation of type theory to check for mathematical correctness. Lean and its library of mathematics results, Mathlib, are increasingly being used by AI companies to reason about mathematics and automatically proof and state theorems. This talk is about PhysLean, the quest to build the lean library for physics results. In this talk I will demonstrate Lean’s potential in physics, discuss the motivations behind the project PhysLean and its current content.

This talk is part of the HEP phenomenology joint Cavendish-DAMTP seminar series.

This talk is included in these lists:

• All CMS events
• All Cavendish Laboratory Seminars
• All Talks (aka the CURE list)
• CMS Events
• Centre for Health Leadership and Enterprise
• DAMTP info aggregator
• Featured lists
• HEP phenomenology joint Cavendish-DAMTP seminar
• HEP web page aggregator
• Interested Talks
• ME Seminar
• MR19 (Potter Room, Pavilion B), CMS
• Neurons, Fake News, DNA and your iPhone: The Mathematics of Information
• School of Physical Sciences
• School of Technology
• Thin Film Magnetic Talks
• bld31
• few29

Note that ex-directory lists are not shown.