Talks

These are slides from public lectures that I have given.

• 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.
• 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.