Formalizing Theoretical Computer Science in Lean
Venkatesan Guruswami, Professor
Electrical Engineering and Computer Science
Applications for Fall 2024 are closed for this project.
Computer-assisted and automated theorem proving has been a longstanding goal of artificial intelligence and has gained increasing importance in recent years. Despite notable advancements, such as AlphaProof from Google DeepMind, which achieves silver-medal standard in solving International Mathematical Olympiad problems, challenges persist in obtaining machine-verifiable theorems and proofs for training AI systems.
This project addresses these challenges by focusing on building a theoretical computer science library in Lean, an interactive theorem prover known for its capability to verify proofs. Lean's popularity in the mathematics community stems from its robust support for formalizing intricate mathematical concepts and its expanding set of tactics and libraries that streamline the formalization process. By creating a comprehensive theoretical computer science library in Lean, this project will provide a formal and rigorous foundation for theoretical computer science (TCS), facilitating the verification of crucial theorems and the development of new algorithms. This library will not only benefit researchers and educators in TCS but also contribute to the broader goal of enhancing computer-assisted and automated theorem proving in artificial intelligence.
Role: The successful candidates will start by reading relevant books and learning about the Lean language. Then the candidate will formalize essential mathematical theorems in theoretical computer science, such as asymptotic theorems, graph theory, and finite-dimensional field theory. Building on the foundational work, the candidates will extend the formalization efforts to cover advanced topics in theoretical computer science, including coding theory, information theory, complexity theory, and cryptography. At the start of the project, we will mainly focus on coding theory.
Qualifications: Candidates should have experience in reading and writing formal proofs, with a solid understanding of linear algebra over finite fields. Familiarity with at least one programming language is essential. While knowledge of Lean or other formal proof languages is desirable, it is not required. However, candidates must be fast learners, as they will be expected to learn how to write proofs in Lean during the first month.
It is strongly recommended that candidates have taken at least one theoretical computer science course, such as CS 170, 172, 174, 191, or 194.
Day-to-day supervisor for this project: Shilun Li, Graduate Student
Hours: to be negotiated
Mathematical and Physical Sciences