skip to content

This is a list of academic projects offered through the Cambridge Mathematics Placements programme for summer 2019 and will be updated on an ongoing basis. Projects should be aimed at students working in the Faculty of Mathematics. To remove a listing, please contact Jacob Rasmussen.

Certified Quantum Algorithms

Contact Name Prof. Lawrence Paulson and Dr. Anthony Bordg
Contact Email
Company Name Computer Laboratory
Address University of Cambridge 15 JJ Thomson Avenue Cambridge CB3 0FD
Period of the Project Summer 2019 (flexible)
Project Open to Undergraduates, Part III students, PhD students
Deadline to Register Interest February 22 2019
Brief Description of the Project Interactive proof assistants such as Isabelle and Coq have attracted prominence recently because of their use in formalising significant results in mathematics such as the Kepler conjecture and the odd order theorem. In the former case, the original mathematical proof was distrusted because of its reliance on a lengthy computation, as in the more familiar four colour theorem. The latter result was formalised to demonstrate the power of the technology. With more and more intricate proofs in mathematics and computer science, proof assistants become appealing. In this project we propose to formalise some quantum algorithms of the candidate's choice, extending an existing basic library. Other topics suitable for formalisation during this project include the mathematical background needed for general relativity (tensor analysis, differential geometry ...) and financial mathematics, depending on the candidate's taste and skills. The candidate will receive training in the use of the Isabelle proof assistant.
Skills Required Knowledge of the requisite mathematics (for instance linear algebra in the case of quantum computing) and basic computer literacy. No knowledge of Isabelle or quantum computing required.
Skills Desired Prior familiarity with any proof assistant would be valuable.