Quantum computing

Stream: Lean for teaching

[Dan Stanescu]

@Jalex Stark I'm wondering if you'd have any ideas, from a teaching-with-Lean perspective, in quantum computing/information. I'll give an introductory class on quantum computing this Fall. It is a graduate class, so there's some room open for experiments. One of my colleagues in CS used ACL2 to prove that a quantum algorithm is correct, but aside from that line of work I'm not aware of any other use of formalization in the field.

[Jalex Stark]

i'm not sure exactly what you mean by ideas

[Jalex Stark]

I haven't gone and formalized a bunch of the basic theorems in a private repo, if that's what you're asking

[Jalex Stark]

i am happy to contribute to such an effort

[Jalex Stark]

if you want to learn about how one might use Lean in the setting of a graduate course that proves theorems, then you should study @Kevin Buzzard's algebraic geometry course

[Dan Stanescu]

I meant to possibly start some brainstorming about how Lean could be used in that regard.

[Jalex Stark]

the last time I thought about this, I got stuck on whether teaching lean bra-ket notation is worth the effort

[Dan Stanescu]

Teaching quantum computing is different from math.

[Kevin Buzzard]

What do the problem sheets look like?

[Jalex Stark]

mm, i mostly have experience teaching it to a mathy audience

[Dan Stanescu]

Right, I'm also wondering if it's worth the effort. Maybe it is, and I don't quite see it.

[Jalex Stark]

what are the goals of this course?

[Jalex Stark]

i think it's mathematically pretty nontrivial

[Dan Stanescu]

It is a course in the math department.

[Jalex Stark]

when we use brakets we're using quite a decent chunk of the power of "finite dimensional hilbert spaces with tensor product form a symmetric monoidal category"

[Jalex Stark]

Dan Stanescu said:

Teaching quantum computing is different from math.

I'm not sure what this comment means, then

[Jalex Stark]

when i went down this path, I started thinking about whether you can make diagrams in globular.science compile into proofs in Lean or similar

[Jalex Stark]

but that still doesn't help you with writing these notations "in-line"

[Jalex Stark]

on the other hand...

[Jalex Stark]

when teaching physicists and undergrads to compute with braket notation they don't come very close to knowing why the manipulations are correct

[Dan Stanescu]

Jalex Stark said:

Dan Stanescu said:

Teaching quantum computing is different from math.

I'm not sure what this comment means, then

This means that we won't be focusing so much on proving theorems as a math class would. We'll focus on discussing the algorithms.

[Jalex Stark]

say more?

[Dan Stanescu]

It is an applied math class, but of course open to students in physics and CS

[Jalex Stark]

a 1-term class that formally proves the correctness of say shor's algorithm has its work cut out for it, interms of proving theorems

[Jalex Stark]

i mean maybe a lot of the theorems are "just matrix multiplication"

[Jalex Stark]

I think that many students are massively confused throughout the entire first year of quantum computing courses about how to do computations in the symmetric monoidal category of finite-dimensional hilbert spaces

[Dan Stanescu]

OK, I see your point. Yes, that's one place where Lean could be brought in.

[Jalex Stark]

My attempts to explain this to them generally end up relying on math they don't know

[Jalex Stark]

one time I wrote a definition of C^* algebra in my recitation notes and Kitaev warned me that this would not go over well with students, so I asked him how he would formalize it and he didn't have a simpler answer

[Jalex Stark]

physicists are happy to throw examples at their students until the students are good at generating correct examples on their own

[Jalex Stark]

all of this is to say, maybe by writing down this stuff in a theorem prover, we can learn more efficient ways to explain these things to students

[Jalex Stark]

just like Kevin learned something about how to explain equivalence relations to 18 year olds

[Jalex Stark]

I think students generally leave the quantum computing courses at caltech without knowing what the statement "for a f.d. hilbert space $$H, H \otimes H^\dagger \congr L(H)$$" means, even though they have usefully exploited such an isomorphism many times

[Mario Carneiro]

Jalex Stark said:

when teaching physicists and undergrads to compute with braket notation they don't come very close to knowing why the manipulations are correct

You could always axiomatize the rules of bra-ket manipulation in lean

[Jalex Stark]

yes, I agree that this is a good thing to do

[Jalex Stark]

in my head, this starts with showing that fdHilb is a symmetric monoidal category

[Jalex Stark]

but maybe there's a more direct path that I would think of if I were forcing myself to prepare notes for a course deadline

[Mario Carneiro]

why is that relevant?

[Jalex Stark]

I guess these notes are the long answer

[Jalex Stark]

(and I am trying to think of a shorter one)

[Jalex Stark]

maybe the simplest "rule of braket manipulation" is associativity of tensor contraction

[Jalex Stark]

so that when you write $$ \bra \psi A \ket \psi $$ you don't have to think about which things are operators acting on what spaces

[Mario Carneiro]

Under a time pressure, one might even use false axioms that imply that all these things associate nicely in any vector space

[Dan Stanescu]

Mario Carneiro said:

Jalex Stark said:

when teaching physicists and undergrads to compute with braket notation they don't come very close to knowing why the manipulations are correct

You could always axiomatize the rules of bra-ket manipulation in lean

That would be nice, too! Thanks for the suggestion, Mario!

[Jalex Stark]

Mario Carneiro said:

Under a time pressure, one might even use false axioms that imply that all these things associate nicely in any vector space

that sounds like it could be pedagogically valuable

[Mario Carneiro]

But I took a class in QM and C* algebras definitely never came up

[Jalex Stark]

the place where I wanted to say the word C* algebra was when discussing the following "computational trick":
if you have a 4x4 matrix, then the operation "think of it as a 2x2 matrix with coefficients who are also 2x2 matrices" commutes with matrix multiplication

[Mario Carneiro]

I would say that any approach that necessitates them is pedagogically suboptimal

[Mario Carneiro]

and that's to say nothing of symmetric monoidal categories

[Jalex Stark]

I don't think that saying the words "c* algebra" or "symmetric monoidal category" to the students is necessary, but they're the words I would use to prove the soundness of the "computational rules" we teach them

[Mario Carneiro]

that sounds right

[Jalex Stark]

i see, so the idea is to do exactly the same things the physicists do, which is to isolate the computational rules and just teach them

[Jalex Stark]

and the advantage of doing that in lean is that you have to actually make the rules explicit

[Jalex Stark]

whereas people who are comfortable with these rules don't think in terms of having a finite ruleset they can apply, they instead think in terms of the underlying spaces

[Jalex Stark]

and can elaborate a proof of why a computation they did is valid on demand

[Dan Stanescu]

Jalex Stark said:

I don't think that saying the words "c* algebra" or "symmetric monoidal category" to the students is necessary, but they're the words I would use to prove the soundness of the "computational rules" we teach them

Do you feel you could get to this in one semester with newcomers?

[Jalex Stark]

get to using those words explicitly? not without sacrificing "canonical" first semester material

[Mario Carneiro]

I would do that in the last chapter, if at all

[Dan Stanescu]

Get to explain the material.

[Jalex Stark]

but explaining the computational rules, of course, that's what the first few weeks are all about

[Jalex Stark]

i don't want to teach my students any quantum algorithms until they can prove that "quantum teleportation" works (without multiplying any matrices bigger than 2x2)

[Mario Carneiro]

I would be curious to see a worked example of one of these statements in lean

[Dan Stanescu]

Jalex Stark said:

but explaining the computational rules, of course, that's what the first few weeks are all about

Thanks Jalex! I have to start thinking about this class carefully. I was going to use Rieffel, btw. I see your next message about teleportation. I think I start having a better idea of what you're trying to say.

[Jalex Stark]

i'm not volunteering to do that until after I think multiplying matrices in Lean is easy

[Mario Carneiro]

If all you need is vectors in a 2D vector space spanned by |0> and |1> then ring can probably do it

[Jalex Stark]

for what it's worth, my favorite book when i was a math student first learning quantum computing was the monograph of kitaev shen and vyalyi

[Dan Stanescu]

Mario Carneiro said:

I would be curious to see a worked example of one of these statements in lean

Might be a nice project for a graduate student.

[Jalex Stark]

do you have some students laying around? :)

[Dan Stanescu]

Thank you both for the ideas!

[Mario Carneiro]

It should be possible to do in ~50 lines though

[Dan Stanescu]

Jalex Stark said:

do you have some students laying around? :)

Only undergrad as of now. They caught on formalization much faster.

[Jalex Stark]

what's "it" here?

[Mario Carneiro]

if it's more than that then something is lacking in the infrastructure

[Mario Carneiro]

one of these exercises on 2D vectors

[Jalex Stark]

gotcha

[Jalex Stark]

to be honest, I have not thought about this in a long time, because "prove stuff about quantum computing" was my initial goal when i came to this zulip server, and I got stuck at "work concretely with any nonabelian finite group"

[Mario Carneiro]

do you have a precise statement of the sort of problem you want to pose?

[Mario Carneiro]

(not necessarily formal in lean)

[Jalex Stark]

"compute the size of the group generated by (1 0 0 -1) and (0 1 1 0)"

[Jalex Stark]

"show that the aforementioned group forms a basis of the 2x2 matrices as a vector space"

[Mario Carneiro]

heh, the second question implies the answer to the first

[Jalex Stark]

indeed, and I think I would be happy stating those problems in that order on a prblem sheet

[Jalex Stark]

where of course "compute" means "give me an explicit enumeration"

[Jalex Stark]

(also it's not literally true, you need to quotient by the center if you want only 4 elements)

[Jalex Stark]

i can go dig up some old recitation notes if you want more exercises

[Mario Carneiro]

I think we can probably get the answer to the first one by brute force; not sure if there is a better method

[Jalex Stark]

the way I wanted to do it was to build the abstract group {x, z, J | x^2, z^2, J^2, xzxzJ, xJxJ, zJzJ}

[Jalex Stark]

then show a group isomorphism associating x with (0 1 1 0), z with (1 0 0 -1) and J with (-1 0 0 -1)

[Jalex Stark]

it's less efficient than brute force, I guess

[Mario Carneiro]

but you still need to prove the order of the group?

[Mario Carneiro]

or is that a well known group

[Jalex Stark]

eh, you still need to prove the order of the group, I guess my point is that I would do the brute force in group land instead of matrix land, there's really no difference

[Jalex Stark]

though once you've phrased it that way it makes it easier to say "swapping x and z is a group automorphism"

[Jalex Stark]

"and so is swapping x with Jxz"

[Mario Carneiro]

well, in matrix land there is an algorithm for reduction (compute the answer as a matrix) while for groups it's some undecidable reduction problem

[Jalex Stark]

right, so I would write down the normal form

[Jalex Stark]

prove the theorem that every element of the group is equal to $J^ax^bz^c$ for a b c : zmod 2

[Mario Carneiro]

I'm imagining that the answer is something like: "observe that {(1,0,0,1),(0,1,1,0),...} is closed under multiplication and each element is reachable from the generators thusly"

[Jalex Stark]

where the proof of the theorem is a reduction algorithm for the word problem in this group

[Jalex Stark]

that seems fine

[Mario Carneiro]

this requires a bunch of subgoals that are matrix multiplies but that seems doable with a tactic

[Mario Carneiro]

in fact I think norm_num [matrix_mul_2x2] would do it

[Mario Carneiro]

where matrix_mul_2x2 is the theorem [a,b,c,d] * [e,f,g,h] = [a*e+b*g, ...]

[Jalex Stark]

that would be cool

[Jalex Stark]

i'll make a serious attempt at this in the next two days with ~50% probability

[Jalex Stark]

(or if you do it, I promise to be excited about it and read your code and try to apply it to something)

[Kevin Buzzard]

Jalex Stark said:

"show that the aforementioned group forms a basis of the 2x2 matrices as a vector space"

That's not true in characteristic 2

[Jalex Stark]

yes, I think open_locale quantum_computing includes an axiom "all matrix coefficients are in the complex numbers or an algebra over it"

[Jalex Stark]

(I don't actually know if the thing I said make sense, it was supposed to be a cheeky way of saying "in a quantum computing class, whenever you write a matrix with explicit coefficients, they are complex numbers")

[Dan Stanescu]

Kevin Buzzard said:

What do the problem sheets look like?

@Kevin Buzzard This is a sample set of problems from the book I'll be using.

http://twoqubits.wikidot.com/ch2

[Donald Sebastian Leung]

Not sure if this is related, but you may wish to take a look at Verified Quantum Computing in Coq

[Patrick Massot]

Now I'm really curious about quantum computing. I've attended quite a lot of quantum mechanics with a strong mathematical bias, and I'm really sure that category theory was completely irrelevant. Linear algebra and functional analysis was everywhere, but monoidal categories sound like a piece of added obfuscation layer.

[Patrick Massot]

The two links above suggest "c* algebra" and "symmetric monoidal category" means "linear algebra in dimension 2", as I expected.

[Scott Morrison]

Some branches of quantum computing, in particular "topological quantum computing", definitely require some category theory: there a working hypothesis is that modular tensor categories (and their associated Reshetikhin-Turaev topological field theories) describe the physics of certain devices. The topological invariance of the ground state is the essential explanation for the hoped-for resistance to decoherence, and topological operations such as braiding are, for some systems, sufficient to build the required unitary operators requested by the quantum computer scientists.

[Scott Morrison]

For plain old quantum computing (rather than studying the materials out of which you might build one), I agree that the category theory is inessential.

[Scott Morrison]

There's a plausible argument that it is nevertheless useful. David Reutter and co have some nice discoveries of (perhaps esoteric) quantum protocols which are easy to describe and prove work once you learn what the notion of a "biunitary connection" is (which first arose in kindred subfactors/planar algebras/fusion categories worlds).

[Dan Stanescu]

Donald Sebastian Leung said:

Not sure if this is related, but you may wish to take a look at Verified Quantum Computing in Coq

Thank you! @Donald Sebastian Leung

[Jalex Stark]

Patrick Massot said:

Now I'm really curious about quantum computing.[...]

What do you want to know? I might be a good API into the computer science-y parts of the literature.

[Patrick Massot]

I wanted to know why category theory is useful there.

[Jalex Stark]

For me it's just as a way to justify string diagram calculations

[Jalex Stark]

often you have multiple "registers" (tensor factors of the ambient hilbert space) and you multiply together a bunch of operators which act on only some of the registers

[Jalex Stark]

and take partial traces

[Jalex Stark]

when you do this all "inline" you have to play a weird parenthesis matching game, because you have both the tensor product (= parallel composition) and tensor contraction (= sequential composition) happening left-to-right

[Jalex Stark]

moving a two-dimensional calculus simplifies that stuff greatly

[Jalex Stark]

I don't think there are other categorical ideas that "mainstream" quantum computing people care about, and indeed they're happy to calculate with these diagrams without trying very hard to prove that the calculus is sound

[Patrick Massot]

Ok, so this is still multilinear algebra, nothing more fancy than tensor products of Hilbert spaces.

[Jalex Stark]

yes

[Patrick Massot]

But probably it helps with the bookkeeping of "associativity" and "commutativity" of tensor product of Hilbert spaces.

[Jalex Stark]

very much

[Jalex Stark]

I guess I'm lying a bit, as scott suggested, some "mainstream" people (people with jobs in physics departments who interact regularly with experimentalists) want to compute with nonabelian anyons

[Jalex Stark]

which have braiding and fusion rules of the sort that category theorists understand

[Jalex Stark]

i took a class from a physicist once where they defined "particles" on the plane as having "charges" whose values were representations of some specific finite group (and assigned homework exercises involving $S_3$-valued anyons which required knowing its character table)

[Jalex Stark]

and the charges would go in tensor product or direct sum with each other when you move particles around

[Jalex Stark]

they argued that using any non-solvable group gives you a model that lets you efficiently implement arbitrary quantum circuits

[Jalex Stark]

there are also topological quantum field theories with a very categorical flavor (I think this is Scott's area of expertise), but these are more "foundations of quantum mechanics"; as far as I know the people in physics departments thinking about topologically-ordered phases of matter can get by without it

[Patrick Massot]

Nice. Even the basic bookkeeping use would be very nice to see in Lean if you can make them usable (I mean more usable than a naive implementation). But maybe normalizing tactics would be better than a category theory coating

[Jalex Stark]

yes, normalizing tactics should be enough do "inline" bra-ket notation

[Jalex Stark]

If I thought I knew a path to a usable implementation of bookkeeping via string diagrams, I would work on it

[Jalex Stark]

(by the way the term "any-on" comes from generalizing "bos-on" and "fermi-on", which are just anyons over the trivial group and the group of order 2. bosons and fermions are the only anyons in a 3-dimensional configuration space)