Quantum algorithms in CSLib

Stream: Quantum information

[Maris Ozols]

I'm interested in formalizing quantum algorithms in Lean - I made a post with more details about this in the #CSLib channel under #CSLib > Quantum algorithms in CSLib?. Feel free to comment there if this is something you find interesting. I'm currently waiting for funding to be approved and I hope that my PhD student will be able to start working on this in January.

[Shreyas Srinivas]

I will also be working on this in a few months.

[Maris Ozols]

I'm curious to know more. Can you elaborate a bit?

[Shreyas Srinivas]

May I DM?

[Mattias Ehatamm]

FYI, i am also working on formalizing some "quantum algorithms" (quantum error-correcting codes) at the moment.

[Maris Ozols]

Cool! @Mattias Ehatamm, are you co-supervised also by Xiaodi Wu? I know that he was involved in formalizing Shor's algorithm in Coq.

[Mattias Ehatamm]

Yes, I am co-supervised by Xiaodi Wu and Runzhou Tao at UMD. I know this is a Lean chat, but if you haven't looked much into formalization of quantum in Coq I would recommend you check it out as some great progress has been made! Robert Rand's group especially has proved a number of useful things.