Videos

Start date cannot be after end date.

Basics

Presenter
  • Johan Commelin
July 12, 2022
ICERM

Natural Number Game demo+exercises

Presenter
  • Kevin Buzzard
July 11, 2022
ICERM

Organizer Welcome / Introduction to Lean

Presenter
  • Jeremy Avigad
July 11, 2022
ICERM

Formally verifying numerics for differential equations

Presenter
  • Bhavik Mehta
May 14, 2026
ICERM

From Lean to Natural Language and Back: Interfaces for Formal Proofs

Presenter
  • Kyle Miller
April 26, 2025
ICERM

Verified Mathematical Reasoning with Lean and Language Models

Presenter
  • Robert Joseph George
April 26, 2025
ICERM

Proof Discovery as Monte Carlo Tree Search

Presenter
  • Leni Aniva
April 25, 2025
ICERM

Formalizing de Rham cohomology in Lean

Presenter
  • Yury Kudryashov
May 12, 2026
ICERM

Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification

Presenter
  • Kaiyu Yang
April 26, 2025
ICERM
Leonardo de Moura - The Lean proof assistant: introduction and challenges - IPAM at UCLA Thumbnail

Leonardo de Moura - The Lean proof assistant: introduction and challenges - IPAM at UCLA

Presenter
  • Leonardo de Moura
February 14, 2023
IPAM

How to design tools for formalization

Presenter
  • Robert Lewis
May 13, 2026
ICERM
Graph Induced Complex: A Data Sparsifier for Homology Inference Thumbnail

Graph Induced Complex: A Data Sparsifier for Homology Inference

Presenter
  • Tamal Dey
October 30, 2013
IMA