Completed
Ad hoc inference
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Georges Gonthier - Computer Proofs - Teaching Computers Mathematics, and Conversely
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Is formalization a formality?
- 3 Some computer proof landmarks
- 4 An old puzzle's story
- 5 Saved by the computer?
- 6 The whole proof
- 7 Proof Algorithms
- 8 Reflecting reducibility
- 9 Building a square
- 10 Building configurations
- 11 Colouring interpretation
- 12 The Poincaré principle
- 13 Minimal logic
- 14 Functions in logic The Moderns
- 15 Crafting map descriptions
- 16 Proof by folklore
- 17 Size matters
- 18 The Odd Order Theorem
- 19 All finite groups of odd order are solvable. Proof: Let G be a minimal counter-example...
- 20 A mathematical library shelf
- 21 Textbook vs. digital formal text
- 22 Interactive Math
- 23 Algebraic Notation
- 24 Implementing notation
- 25 Algebra interfaces Equality
- 26 Inferring notation
- 27 Basic interfaces and objects bool
- 28 Ad hoc inference
- 29 Interfacing big operators
- 30 Coprime cycle coherence
- 31 A dot product matrix puzzle
- 32 An integer norm problem
- 33 Sorting a combinatorial mess
- 34 Homotopy type theory Type A
- 35 Synthetic Homotopy Type Theory
- 36 Cubical Type Theory
- 37 Conclusion
