Thomas Georges Pierre Vidick

Teaching & PhD PhD Students Itammar Steinberg, Aviv Taller Courses Formal Mathematics with Lean and AI CS-643 This graduate course provides an introduction to using Lean proof assistant to formalize mathematical definitions and theorems. We will have lectures on foundations (formal proofs, dependent type theory), learn about practice (proof tactics, use of AI, etc) and work on a formalization project. Introduction to quantum computation CS-308 The course introduces the paradigm of quantum computating in an axiomatic way. We introduce the notions of quantum bits, gates, and circuits. We introduce themost important quantum algorithms. We also touch upon error-correcting codes. This course is independent of COM-309. Introduction to quantum cryptography COM-440 This course describes, at a rigorous mathematical level, a range of such tasks, each time identifying the fundamental property of quantum information that makes it possible, its strengths, and its limits. Methods in Quantum Error Correction CS-632 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.