Datatypes as quotients of polynomial functors

Slides: pdf.The mechanization of mathematics

Slides: 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: leanA 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: pdfMathematics 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.Dirichlet's theorem on primes in an arithmetic progression.

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.