Co-piloting proofs

2 PM, 26 Mar 2025

Dr Bhavik Mehta from Imperial College London gives an overview of Lean, the proof-assistant computer language used to formalize mathematics.

Dr. Bhavik Mehta is research fellow at Imperial College London, where he works with Prof. Kevin Buzzard, an expert on formal proof verification. Dr. Mehta did his PhD at Cambridge under the supervision of Prof. Timothy Gowers and later worked on Google DeepMind’s AlphaProof, which formulates problems in Lean. In a series of talks at the London Institute, he shows how Lean can verify proofs and even help find them.

Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs
Co-piloting proofs