Quantum computing

Stream: PhysLean

[Shlok Vaibhav]

Had a query about everyone's views on the coverage of formalization of basics of quantum computing?? That is very amenable to theorem proving already and is also very popular amongst young undergrads these days?? I don't think we have any active project ideas on this??

[Joseph Tooby-Smith]

@Alex Meiburg has a library for quantum information here.

I would certainly advocate for parts of quantum computing to be in PhysLean - especially the parts (e.g. the API) which have applications to other areas of physics, how far one goes in this direction within PhysLean is another question, the answer to which may be found organically.

But to answer your question directly: There are no active project ideas for this as part of PhysLean.

[ZhiKai Pong]

was just going to say this, and to add to that I recall seeing this thread #mathlib4 > > Quantum Computing in Lean4

which recently ported some quantum computing theory to lean4 which you might be interested

[Alex Meiburg]

I know @Mattias Ehatamm is also exploring doing some quantum computing related stuff in Lean.

In my repo I have some basic gates / facts (e.g. how to commute a controlled gate around), but nothing about "circuits" more broadly. (As in, over some variable number of qubits with a PROP structure.)

There's some /theoretical/ work trying to figure out a nice theory to talk about circuits. I mean, we all know quantum physics, but in the same way that there's a difference between Boolean algebra and the notion of "Boolean circuit", there's a theory needed.

You could look at https://arxiv.org/abs/2105.10914 for a good treatment of how we figure out what a "variable" is, or https://arxiv.org/abs/2206.10577 for a nice idea of how the PROP looks

[Joseph Tooby-Smith]

By API above, I mean we probably want things like:

1. Tensor product of Hilbert spaces and hamiltonians,
2. Mixed states,
3. Pure states,
4. Density matrices.

[Notification Bot]

5 messages were moved here from #PhysLean > PhsyLean suitable for a mathematics undergrad student by Joseph Tooby-Smith.

[Alex Meiburg]

Regardless of what you want to do, you should also chat about what you're doing in https://leanprover.zulipchat.com/#narrow/channel/508986-Quantum-information ! As well as here if you're building on PhysLean. :)

[Joseph Tooby-Smith]

(A bit of an aside: PhysLean does have the project ideas page, and it might be worth adding something along these lines to that. This is something anyone can do here)