Projects

Project Description

The purpose of this project is to twofold. On the one hand, we want to explore how well Chatbots like ChatGPT, Google Bard, and others, can write proofs of known mathematical statements (like the fact that there are infinitely many prime numbers), and whether one can lead them to find proofs of facts that have not been discovered yet. We will read current literature on this topic and find out what experts think about the potential for doing mathematical research interactively, assisted by AI. Moreover, we will try to find out how Chatbots understand various mathematical problems, from elementary to more advanced. The second topic is that of proof assistants (e.g., the Lean theorem prover). The purpose of these machines is not to let an AI find a proof by itself, but to have a program which checks that every step of a proof (written by a human) is correct in the sense that it follows from a given set of axioms. By looking at various examples, we will try out what these programs can do. Of course, there is a certain connection between these two topics, and one of the goals of the project is to understand the relation between AI generated proofs and theorems verified by proof assistants.

Technology or Computational Component

None or this is required as a prerequisite, but getting familiar with the languages in which proofs assistants are written is one computational aspect. We will also use Python and the computing platform SAGE for writing code that verifies computationally certain mathematical statements (so as to check whether the Chatbot is correct!). The student will also learn to write documents with the software LaTeX (using the platform Overleaf) which is the standard editor to produce texts involving mathematics.