Talks

You want proof? I'll give you proof! Mathematical arguments from Euclid to Lean
Slides: Google Slides, web page html
AI for mathematics
Slides: pdf
Mathematics and the formal turn
Slides: pdf
Automated reasoning for mathematics
Slides: pdf
Teaching with Lean
Slides: pdf
Verifying elliptic curve computations on blockchain
Slides: pdf
Proof assistants and mathematics education
Slides: pdf, Demo: Lean 4 Web
Mathematical structures in dependent type theory
Slides: pdf
Machine learning and symbolic AI for mathematics
Slides: pdf
Where the money is
Slides: pdf
A proof-producing compiler for blockchain applications
Slides: pdf
Machine learning, formal methods, and mathematics
Slides: pdf, Video: conference page (beginning of day 2)
Is mathematics obsolete?
Slides: pdf, Video: YouTube
Teaching undergraduate mathematicians and computer scientists how to formalize mathematics
Slides: pdf
The promise of formal mathematics
Slides: pdf
From Mathematical Components to mathlib
Slides: pdf
Varieties of mathematical understanding
Slides: pdf, Video: web page
The digital revolution in mathematics
Slides: pdf, Video: web page
Proof systems
Slides: pdf
Mathematical understanding
Slides: pdf
Formal assistants and mathematics education
Slides: pdf, Video: web page
Slides from a similar talk: pdf
A verified algebraic representation of Cairo program execution
Slides: pdf, Video: YouTube
Teaching Logic and Mechanized Reasoning with Lean 4
Slides: pdf, Video: mp4, YouTube
Formal mathematics, dependent type theory, and the Topos Institute
Slides: pdf, Video: YouTube
Conservativity of weak König's lemma (a proof from the book)
Slides: pdf, Video: YouTube
The Hoskinson Center inauguration
Slides: pdf, Video: YouTube
See also Hoskinson's presentation at the ceremony (YouTube) and the day after (YouTube)
The design of mathematical language
Slides: pdf, Video: YouTube
Another version: pdf
Methodology and metaphysics in Dedekind's theory of ideals
Slides: pdf, Video: YouTube
Interactive theorem proving and the Lean theorem prover
Slides: pdf, Video: YouTube
Teaching with proof assistants
Slides: pdf, Video: YouTube
Interactive theorem proving for the working logician
Slides: pdf
Progress on a perimeter surveillance problem
Slides: pdf
Formal methods and the epistemology of mathematics
Slides: pdf
Reliability of mathematical inference
Slides: pdf
Thoughts on "philosophy of mathematical practice"
Slides: pdf
Automated reasoning for the working mathematician
Slides: pdf, associated repository: github
Datatypes as quotients of polynomial functors
Slides: pdf
The mechanization of mathematics
Slides: pdf, Video: YouTube
Slides (another version): pdf
Mathematical language from a design perspective
Slides: pdf
The Lean theorem prover
Slides: pdf
Formal methods in mathematics and the Lean theorem prover
Slides: pdf
Modularity in mathematics
Slides: pdf
Mathematical understanding
Slides: pdf
A series of five lectures on the philosophy of mathematics:
Mathematical understanding: pdf
The history of Dirichlet's theorem on primes in an arithmetic progression: pdf
Formalization and interactive theorem proving: pdf
The role of the diagram in Euclid's Elements: pdf
Modularity in mathematics: pdf
The Lean theorem prover and homotopy type theory (with Floris van Doorn)
Slides: pdf
Interactive theorem proving, automated reasoning, and dynamical systems
Slides: pdf
Type theory and practical foundations
Slides: pdf
Homotopy type theory
Slides: pdf
Logic and interactive theorem proving
A presentation for undergraduates. Slides: pdf
Lean examples: lean
A series of lectures on proof theory and proof mining
Course page: html
A heuristic prover for real inequalities
Slides: pdf
A series of four lectures on formal methods in mathematics:
Formal methods in mathematics: pdf
Automated theorem proving: pdf
Interactive theorem proving: pdf
Formal methods in analysis: pdf
Mathematics and language
Slides: pdf
Uniform distribution and algorithmic randomness
Slides: pdf
The Lean theorem prover
Slides: pdf
Formal verification, interactive theorem proving, and automated reasoning
Slides: pdf
Computability and uniformity in ergodic theory
Slides: pdf
Approximate decidability and verification of hybrid systems.
Slides: pdf
Interactive theorem proving, automated reasoning, and mathematical computation
Slides: pdf
Computability and uniformity in analysis
Slides: pdf
Hilbert, Gödel, and metamathematics today
Slides: pdf
Computability, constructivity, and convergence in measure theory
Slides: pdf
Simplicity, extensionality, and functions as objects
Slides: pdf
Interactive theorem proving
A survey / tutorial, for logicians. Slides: pdf
Inverting the Furstenberg correspondence
A short overview of the paper with the same title. Slides: pdf
Type inference and finite group theory
Slides: pdf
Understanding, formal verification, and the philosophy of mathematics
See also the paper with the same title. Slides: pdf
Decision procedures, heuristic procedures, and formally verified mathematics
Slides: pdf
Mathematical simplicity
Slides: pdf
Formal verification of algorithms
An overview, for philosophers. Slides: pdf
Computability in ergodic theory
An overview. Slides: pdf
The computational content of classical arithmetic
An overview of the paper with the same title. Slides: pdf
Metastability in ergodic theory
A quick overview of results in "Local stability of ergodic averages" and "Metastability in the Furstenberg-Zimmer tower". Slides: pdf
The role of the diagram in Euclid's Elements
An overview of the paper "A formal system for Euclid's Elements". Slides: pdf
Computability in ergodic theory
An overview of the paper "Local stability of ergodic averages". Slides: pdf
Verifying real inequalities
An overview of the paper "Combining decision procedures for the reals". Slides: pdf
Methodology and metaphysics in the development of Dedekind's theory of ideals
Based on the paper with the same title. Slides: pdf
A formally verified proof of the prime number theorem
Based on a paper of the same title. Slides: pdf
Translating nonstandard proofs to constructive ones
Uses a nonstandard proof by Renling Jin to find an elementary proof of Steinhaus' theorem. Slides: pdf Additional notes: html
Proof mining
A three-lecture tutorial. Slides: pdf
Distances, projections, and the mean ergodic theorem in subsystems of second-order arithmetic
A preliminary presentation of some of the results in "Fundamental notions of analysis in subsystems of second-order arithmetic". Slides: pdf
Forcing in proof theory
A survey of applications of forcing to proof theory, based on the paper of the same title. Slides: pdf, pdf
Update procedures and the 1-consistency of arithmetic
An overview of the paper with the same title. Slides: pdf
Eliminating definitions and Skolem functions in first-order logic
An overview of the paper with the same title. Slides: pdf
Semantic approaches to ordinal analysis
Primarily an overview of "An ordinal analysis of admissible set theory using recursion on ordinal notations". Slides: pdf
Weak theories of nonstandard arithmetic and analysis
An overview of the paper with the same title. Slides: pdf
Between proof theory and model theory
An overview of "Saturated models of universal theories". Slides: pdf
Cut elimination revisited
An overview of "Algebraic proofs of cut elimination". Slides: pdf
Sheaf semantics and nonstandard intuitionistic arithmetic
An overview of "Transfer principles in nonstandard intuitionistic arithmetic," for classical logicians. Slides: pdf
Semantic methods in proof theory
A survey. Slides: pdf
Interpreting classical theories in constructive ones
An overview of the paper with the same title. Slides: pdf
A realizability interpretation for classical arithmetic
An overview of the paper with the same title. Slides: pdf
The combinatorics of propositional provability
An overview of "Plausibly hard combinatorial tautologies". Slides: pdf
Proof theory and subsystems of second-order arithmetic
A survey of some of my work in proof theory. Slides: pdf