Course

CS-643: Formal Mathematics with Lean and AI

Summary

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.

Lectures

Instructors (3)

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Maryna Viazovska

Maryna Viazovska did her bachelor studies at the Kyiv National Taras ShevchenkoUniversity and completed her MSc at the Technical University Kaiserslautern.She obtained her PhD in 2013 in Bonn.She was a postdoctoral researcher at the Institut des Hautes Etudes Scientifiquesand at the Humboldt University of Berlin, and in 2017 was a Minerva DistinguishedVisitor at Princeton University. She joined EPFL in 2017 as Tenure-Track AssistantProfessor and was promoted Full Professor in 2018.

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 para

Official source

Moodle Page

http://go.epfl.ch/CS-643

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.