AI for Mathematics and Theorem Proving
Dawn Song, Professor
Electrical Engineering and Computer Science
Applications for Spring 2025 are closed for this project.
Artificial Intelligence has the potential to revolutionize the field of mathematics by automating theorem proving and assisting in complex mathematical research. This project explores the application of AI techniques to enhance automated reasoning and support mathematicians in their work.
Areas of investigation include:
- Automated Theorem Proving: Developing AI models that can autonomously prove mathematical theorems or suggest proof strategies.
- Mathematical Knowledge Representation: Creating representations of mathematical concepts that AI systems can effectively utilize for reasoning tasks.
- Interactive Theorem Proving Assistants: Building tools that collaborate with human mathematicians, providing suggestions and verifying proof steps in real-time.
- Integration with proof assistants: Enhancing existing proof assistants (e.g., Coq, Lean) with AI capabilities to improve their functionality and usability.
Role: The project combines theoretical research in automated reasoning with practical implementations to create tools that can aid in mathematical discovery and verification.
Qualifications: - Strong background in mathematics and computer science.
- Experience with formal methods and theorem proving software is desirable.
- Proficient in programming languages such as Python, OCaml, Coq, Lean.
- Interest in artificial intelligence and formal verification.
Day-to-day supervisor for this project: Jingxuan He
Hours: 12 or more hours
Engineering, Design & Technologies