Completed
Hypertree proof search
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
The Lean Proof Assistant - Introduction and Challenges - IPAM at UCLA
Automatically move to the next video in the Classroom when playback concludes
- 1 Introduction
- 2 How to install
- 3 Meta programming
- 4 Simple example
- 5 Should we trust
- 6 Magical Library
- 7 Perfectoid Spaces
- 8 Ecosystem
- 9 Olympic channel
- 10 Mathematical Library
- 11 Cancer Experiment
- 12 Impacts of formal mathematics
- 13 Extensions
- 14 Performance
- 15 Syntax
- 16 Domainspecific languages
- 17 Framework
- 18 Case analysis
- 19 Challenges
- 20 Overhead factor
- 21 Scalability
- 22 Accessibility
- 23 Trace messages
- 24 Visualizations
- 25 AI in mathematics
- 26 Hypertree proof search
- 27 Marketplace
- 28 Interactive process
- 29 Engineering
- 30 Tower of Babel
- 31 Community excitement
- 32 Manufacturing originalization
- 33 The main message
