A verified algebraic representation of Cairo program execution

Slides: pdfTeaching Logic and Mechanized Reasoning with Lean 4

Slides: pdf, Video: mp4Formal mathematics, dependent type theory, and the Topos Institute

Slides: pdf, Video: YouTubeConservativity of weak König's lemma (a proof from the book)

Slides: pdfThe 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: YouTubeMethodology and metaphysics in Dedekind's theory of ideals

Slides: pdf, Video: YouTubeInteractive theorem proving and the Lean theorem prover

Slides: pdf, Video: YouTubeTeaching with proof assistants

Slides: pdf, Video: YouTubeInteractive theorem proving for the working logician

Slides: pdfProgress on a perimeter surveillance problem

Slides: pdfFormal methods and the epistemology of mathematics

Slides: pdfReliability of mathematical inference

Slides: pdfThoughts on "philosophy of mathematical practice"

Slides: pdfAutomated reasoning for the working mathematician

Slides: pdf, associated repository: githubDatatypes as quotients of polynomial functors

Slides: pdfThe mechanization of mathematics

Slides: pdf, Video: YouTube

Slides (another version): pdfMathematical language from a design perspective

Slides: pdfThe Lean theorem prover

Slides: pdfFormal methods in mathematics and the Lean theorem prover

Slides: pdfModularity in mathematics

Slides: pdfMathematical understanding

Slides: pdfA 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: pdfInteractive theorem proving, automated reasoning, and dynamical systems

Slides: pdfType theory and practical foundations

Slides: pdfHomotopy type theory

Slides: pdfLogic and interactive theorem proving

A presentation for undergraduates. Slides: pdf

Lean examples: leanA series of lectures on proof theory and proof mining

Course page: htmlA heuristic prover for real inequalities

Slides: pdfA 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: pdfUniform distribution and algorithmic randomness

Slides: pdfThe *Lean*theorem prover

Slides: pdfFormal verification, interactive theorem proving, and automated reasoning

Slides: pdfComputability and uniformity in ergodic theory

Slides: pdfApproximate decidability and verification of hybrid systems.

Slides: pdfInteractive theorem proving, automated reasoning, and mathematical computation

Slides: pdfComputability and uniformity in analysis

Slides: pdfHilbert, Gödel, and metamathematics today

Slides: pdfComputability, constructivity, and convergence in measure theory

Slides: pdfSimplicity, extensionality, and functions as objects

Slides: pdfInteractive theorem proving

A survey / tutorial, for logicians. Slides: pdfInverting the Furstenberg correspondence

A short overview of the paper with the same title. Slides: pdfType inference and finite group theory

Slides: pdfUnderstanding, formal verification, and the philosophy of mathematics

See also the paper with the same title. Slides: pdfDecision procedures, heuristic procedures, and formally verified mathematics

Slides: pdfMathematical simplicity

Slides: pdfFormal verification of algorithms

An overview, for philosophers. Slides: pdfComputability in ergodic theory

An overview. Slides: pdfThe computational content of classical arithmetic

An overview of the paper with the same title. Slides: pdfMetastability in ergodic theory

A quick overview of results in "Local stability of ergodic averages" and "Metastability in the Furstenberg-Zimmer tower". Slides: pdfThe role of the diagram in Euclid's *Elements*

An overview of the paper "A formal system for Euclid's*Elements"*. Slides: pdfComputability in ergodic theory

An overview of the paper "Local stability of ergodic averages". Slides: pdfVerifying real inequalities

An overview of the paper "Combining decision procedures for the reals". Slides: pdfMethodology and metaphysics in the development of Dedekind's theory of ideals

Based on the paper with the same title. Slides: pdfA formally verified proof of the prime number theorem

Based on a paper of the same title. Slides: pdfTranslating nonstandard proofs to constructive ones

Uses a nonstandard proof by Renling Jin to find an elementary proof of Steinhaus' theorem. Slides: pdf Additional notes: htmlProof mining

A three-lecture tutorial. Slides: pdfDistances, 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: pdfForcing in proof theory

A survey of applications of forcing to proof theory, based on the paper of the same title. Slides: pdf, pdfUpdate procedures and the 1-consistency of arithmetic

An overview of the paper with the same title. Slides: pdfEliminating definitions and Skolem functions in first-order logic

An overview of the paper with the same title. Slides: pdfSemantic approaches to ordinal analysis

Primarily an overview of "An ordinal analysis of admissible set theory using recursion on ordinal notations". Slides: pdfWeak theories of nonstandard arithmetic and analysis

An overview of the paper with the same title. Slides: pdfBetween proof theory and model theory

An overview of "Saturated models of universal theories". Slides: pdfCut elimination revisited

An overview of "Algebraic proofs of cut elimination". Slides: pdfSheaf semantics and nonstandard intuitionistic arithmetic

An overview of "Transfer principles in nonstandard intuitionistic arithmetic," for classical logicians. Slides: pdfSemantic methods in proof theory

A survey. Slides: pdfInterpreting classical theories in constructive ones

An overview of the paper with the same title. Slides: pdfA realizability interpretation for classical arithmetic

An overview of the paper with the same title. Slides: pdfThe combinatorics of propositional provability

An overview of "Plausibly hard combinatorial tautologies". Slides: pdfProof theory and subsystems of second-order arithmetic

A survey of some of my work in proof theory. Slides: pdf