Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle/HOL in the era of Quantum Computer Sc...

view this post on Zulip Email Gateway (Aug 22 2022 at 18:53):

From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
In my last email in this mailing list I mentioned that

I guess that Homotopy Type Theory will be a natural framework for formal

verification of programs written for a topological quantum computer. Of
course, some skeptic people may disagree.

I would like to justify these two claims by giving some references, which
may be useful for some students, because both subjects are trend (there
were many PhD thesis about these subject related to several proof
assistants in the last 10 years). Also, there is a lot of funding in this
area:
https://www.geekwire.com/2018/trump-signs-legislation-back-quantum-computing-research-1-2-billion/

Affirmation 1: *I guess that Homotopy Type Theory will be a natural
framework for formal verification of programs written for a topological
quantum computer.*

My reference is page 8 of the (literally beautiful!) paper

Paredes, Belén. "Boson-Lattice Construction for Anyon Models." *arXiv
preprint arXiv:1804.01605* (2018).
https://arxiv.org/pdf/1804.01605.pdf

where we find the statement:

From a purely mathematical perspective, it is known that the language
underlying anyon models is modular tensor category

Definition of modular tensor category:
https://ncatlab.org/nlab/show/modular+tensor+category

Homotopy Type Theory has being successfully used in order to formalize
category theory:
https://homotopytypetheory.org/book/

On the other hand, quantum mechanics can be formalized avoiding category
theory, as most physicists do. So, Isabelle/HOL is also a possible approach
to formalize this subject.

Affirmation 2: Of course, some skeptic people may disagree.

One example of skeptic person concerning quantum computing, in particular,
topological quantum computing, is Prof. Gil Kalai (Hebrew University of
Jerusalem and Yale University). Here are some of his arguments:

On the other hand, there are optimistic people too. For example, Prof.
Scott Aaronson (MIT, UT Austin) considers that it is more conservative to
think that a quantum computer is possible than to think that it is
fundamentally impossible:
https://www.youtube.com/watch?v=s1bxNomtaTE

I hope that these references will be useful for the students working in
these areas from the point of view of proof assistants.

My advise to people who want to enter to this subject, using Isabelle/HOL,
is to practice a lot of linear algebra, e.g., here:
https://www.isa-afp.org/entries/VectorSpace.html
<https://www.isa-afp.org/entries/VectorSpace.html>

Some people prefer to use dependent type theory (Coq) and their main
argument is given in the following paper (see Definition dep_matrix):
http://www.cs.umd.edu/~rrand/coqpl_2018.pdf

Kind Regards,
José M.

Last updated: Apr 25 2024 at 04:18 UTC