Completed
Andrej Bauer - Formalizing invisible mathematics - IPAM at UCLA
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Machine Assisted Proofs in Mathematics Workshop 2023
Automatically move to the next video in the Classroom when playback concludes
- 1 Andrej Bauer - Formalizing invisible mathematics - IPAM at UCLA
- 2 Leonardo de Moura - The Lean proof assistant: introduction and challenges - IPAM at UCLA
- 3 Patrick Massot - Formal mathematics for mathematicians and mathematics students - IPAM at UCLA
- 4 Tony Wu - Autoformalization with Large Language Models - IPAM at UCLA
- 5 Geordie Williamson - What can the working mathematician expect from deep learning? - IPAM at UCLA
- 6 Jason Rute - Deep learning in interactive theorem proving - IPAM at UCLA
- 7 Adam Wagner - Finding counterexamples to conjectures via reinforcement learning - IPAM at UCLA
- 8 Heather Macbeth - Algorithm and abstraction in formal mathematics - IPAM at UCLA
- 9 John Harrison - Formalization and Automated Reasoning: A Personal and Historical Perspective
- 10 Marc Lackenby - Using machine learning to formulate mathematical conjectures - IPAM at UCLA
- 11 Adam Topaz - The Liquid Tensor Experiment - IPAM at UCLA
- 12 James Davenport - How to prove a calculation correct? - IPAM at UCLA
- 13 Anne Baanen - Computing with or despite the computer - IPAM at UCLA
- 14 Haniel Barbosa - Better SMT proofs for certifying compliance and correctness - IPAM at UCLA
- 15 Benedikt Ahrens - Univalent Foundations and the UniMath library - IPAM at UCLA
- 16 Johnathan Hanke - Computer-Assisted Proofs in the Arithmetic of Quadratic Forms - IPAM at UCLA
- 17 Bohua Zhan - Verifying symbolic computation in the HolPy theorem prover - IPAM at UCLA
- 18 Petra Hozzova - Automation of Induction in Saturation - IPAM at UCLA
- 19 Pascal Fontaine - SMT: quantifiers, and future prospects - IPAM at UCLA
- 20 Maria Ines de Frutos Fernandez - Formalizing Norm Extensions and Applications to Number Theory
- 21 Micaela Mayero - Overview of real numbers in theorem provers: application with real analysis in Coq
