Automated Formalisation of Quantum Mathematical Proofs Using Machine Learning

This project aims to build an AI system that can turn regular, human-written math problems and solutions into fully checked, error-free formal proofs, with a special focus on quantum mathematics. The project will collect open-source quantum math problems, train a machine-learning model to translate them into formal proofs using the Lean proof assistant, and create an open dataset and simple converter tool that others can use.

The greatest benefit for the institutions participating in the research partnership will be the sharing of access to new toolkits, data, and approaches to trustworthy AI reasoning. Both University of Calgary and Technical University of Munich will benefit from the up-to-date knowledge and sharing of resources in the field of AI, formal verification, and quantum math. Valuable resources such as the dataset and the coverter system will contribute to their work in the fields of ML and mathematical reasoning. The work will result in a publication in an academic journal, which will improve both universities’ academic reputation.

Faculty Supervisor:

Samira Ebrahimi Kahou

Student:

Partner:

Technical University of Munich

Discipline:

Computer science

Sector:

Quantum Science; Artificial Intelligence; Information and Communications Technology (ICT)

University:

University of Calgary

Program: