Welcome

Research

Papers

Books

Reviews

Talks

Outreach

Teaching

Students

Talks

• Institute for Computer-Aided Reasoning in Mathematics
  Slides: pdf.
• Is mathematics obsolete?
  A talk based on an essay with the same title.
  Slides: pdf.
• Tarski lectures (2025): How mathematics works
  Euclid's Elements and diagrammatic reasoning in geometry: pdf
  Dirichlet's theorem on primes in an arithmetic progression and functions as objects: pdf
  Dedekind's theory of ideals and modern algebraic abstraction: pdf
  
• AI for mathematicians
  Slides: pdf
• You want proof? I'll give you proof! Mathematical arguments from Euclid to Lean
  Slides: Google Slides, web page html, Video: YouTube
• 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
• Formalizing mathematical structures
  Slides: pdf, Another version: pdf, a fragment of the hierarchy: 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
• Philosophy of mathematics as a design science
  Slides: pdf, Video: YouTube
• 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