University of Cambridge > Talks.cam > HEP phenomenology joint Cavendish-DAMTP seminar > PhysLean: Digitalizing physics into Lean

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

PhysLean: Digitalizing physics into Lean

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Average on weekdays: 9211.868 kWh Klug Seminar Room, Level 2 2A180, MRC LMB McDonald Institute Seminar Room, Department of Archaeology

Other talks

Online Causal Inference Seminar TBC Rothschild Public Lecture: Forty years of causal inference: Report of a great-grandfather Afternoon Break Title TBC The LMC-SMC System: A New Laboratory for Galaxy Evolution, Dynamics and Dark Matter
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity