Talks
- 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