Formalizing mathematics using proof assistants enables eliminating errors, encourages collaborative mathematics, and can lead to deeper understanding. This graduate course provides an introduction to using Lean proof assistant to formalize mathematical definitions and theorems. We will give an overview of foundations of formal proof and dependent type theory of Lean. We will also explore how to leverage proof tactics (such as simp, rw, ring, linarith) to automate up proof construction. In addition, we will explore how AI assistants based on large language models can make the formalization process more productive. Finally, in the second half of the course we will work on a formalization project (to be chosen in class) together.
- Professor: Thomas Bourgeat
- Professor: Friedrich Eisenbrand
- Professor: Viktor Kuncak
- Professor: Ola Nils Anders Svensson
- Professor: Maryna Viazovska
- Professor: Thomas Vidick
- Teacher: Jonathan Conrad
This course discusses mathematical methods of quantum error correction in the style via presentation and discussion of research papers. It covers basic algebraic and geometric properties of quantum error correcting codes and fault tolerance theory and prepares for research in this field.
- Quantum error correction theory: Conditions, Recoverability, Geometry.
- Semidefinite optimization of quantum error correcting codes.
- Stabilizer codes in finite and infinite dimensions: Symplectic lattices
- Invariants of quantum error correcting codes: Weight enumerators
- Coding theory: parameter bounds and existence results
- Code constructions: Kitaevs quantum double model, homological codes, the toric code.
- Application of Quantum error correction to complexity
- Professor: Jonathan Conrad
- Professor: Maryna Viazovska
- Professor: Thomas Vidick
- Professor: Aurèle Barrière
- Professor: Clément Pit-Claudel
- Teacher: Yawen Guan
- Teacher: Alexandre Pinazza
