# Zulip Chat Archive

## Stream: Lean for teaching

### Topic: Quantum computing

#### Dan Stanescu (May 17 2020 at 21:11):

@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 (May 17 2020 at 22:07):

i'm not sure exactly what you mean by ideas

#### Jalex Stark (May 17 2020 at 22:08):

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 (May 17 2020 at 22:08):

i am happy to contribute to such an effort

#### Jalex Stark (May 17 2020 at 22:08):

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 (May 17 2020 at 22:09):

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

#### Jalex Stark (May 17 2020 at 22:09):

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

#### Dan Stanescu (May 17 2020 at 22:09):

Teaching quantum computing is different from math.

#### Kevin Buzzard (May 17 2020 at 22:09):

What do the problem sheets look like?

#### Jalex Stark (May 17 2020 at 22:10):

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

#### Dan Stanescu (May 17 2020 at 22:10):

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

#### Jalex Stark (May 17 2020 at 22:10):

what are the goals of this course?

#### Jalex Stark (May 17 2020 at 22:10):

i think it's mathematically pretty nontrivial

#### Dan Stanescu (May 17 2020 at 22:10):

It is a course in the math department.

#### Jalex Stark (May 17 2020 at 22:10):

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 (May 17 2020 at 22:11):

Dan Stanescu said:

Teaching quantum computing is different from math.

I'm not sure what this comment means, then

#### Jalex Stark (May 17 2020 at 22:11):

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 (May 17 2020 at 22:12):

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

#### Jalex Stark (May 17 2020 at 22:12):

on the other hand...

#### Jalex Stark (May 17 2020 at 22:12):

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 (May 17 2020 at 22:13):

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 (May 17 2020 at 22:13):

say more?

#### Dan Stanescu (May 17 2020 at 22:13):

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

#### Jalex Stark (May 17 2020 at 22:13):

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 (May 17 2020 at 22:14):

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

#### Jalex Stark (May 17 2020 at 22:16):

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 (May 17 2020 at 22:16):

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

#### Jalex Stark (May 17 2020 at 22:16):

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

#### Jalex Stark (May 17 2020 at 22:17):

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 (May 17 2020 at 22:18):

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

#### Jalex Stark (May 17 2020 at 22:18):

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 (May 17 2020 at 22:19):

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

#### Jalex Stark (May 17 2020 at 22:22):

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 (May 17 2020 at 22:23):

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 (May 17 2020 at 22:23):

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

#### Jalex Stark (May 17 2020 at 22:24):

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

#### Jalex Stark (May 17 2020 at 22:25):

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 (May 17 2020 at 22:25):

why is that relevant?

#### Jalex Stark (May 17 2020 at 22:26):

I guess these notes are the long answer

#### Jalex Stark (May 17 2020 at 22:26):

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

#### Jalex Stark (May 17 2020 at 22:26):

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

#### Jalex Stark (May 17 2020 at 22:27):

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 (May 17 2020 at 22:27):

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

#### Dan Stanescu (May 17 2020 at 22:27):

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 (May 17 2020 at 22:28):

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 (May 17 2020 at 22:28):

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

#### Jalex Stark (May 17 2020 at 22:29):

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 (May 17 2020 at 22:29):

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

#### Mario Carneiro (May 17 2020 at 22:29):

and that's to say nothing of symmetric monoidal categories

#### Jalex Stark (May 17 2020 at 22:30):

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 (May 17 2020 at 22:31):

that sounds right

#### Jalex Stark (May 17 2020 at 22:32):

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 (May 17 2020 at 22:32):

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

#### Jalex Stark (May 17 2020 at 22:33):

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 (May 17 2020 at 22:33):

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

#### Dan Stanescu (May 17 2020 at 22:34):

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 (May 17 2020 at 22:34):

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

#### Mario Carneiro (May 17 2020 at 22:34):

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

#### Dan Stanescu (May 17 2020 at 22:34):

Get to explain the material.

#### Jalex Stark (May 17 2020 at 22:35):

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

#### Jalex Stark (May 17 2020 at 22:36):

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 (May 17 2020 at 22:37):

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

#### Dan Stanescu (May 17 2020 at 22:37):

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 (May 17 2020 at 22:38):

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

#### Mario Carneiro (May 17 2020 at 22:38):

If all you need is vectors in a 2D vector space spanned by `|0>`

and `|1>`

then `ring`

can probably do it

#### Jalex Stark (May 17 2020 at 22:38):

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 (May 17 2020 at 22:39):

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 (May 17 2020 at 22:39):

do you have some students laying around? :)

#### Dan Stanescu (May 17 2020 at 22:39):

Thank you both for the ideas!

#### Mario Carneiro (May 17 2020 at 22:39):

It should be possible to do in ~50 lines though

#### Dan Stanescu (May 17 2020 at 22:39):

Jalex Stark said:

do you have some students laying around? :)

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

#### Jalex Stark (May 17 2020 at 22:39):

what's "it" here?

#### Mario Carneiro (May 17 2020 at 22:40):

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

#### Mario Carneiro (May 17 2020 at 22:40):

one of these exercises on 2D vectors

#### Jalex Stark (May 17 2020 at 22:40):

gotcha

#### Jalex Stark (May 17 2020 at 22:41):

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 (May 17 2020 at 22:41):

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

#### Mario Carneiro (May 17 2020 at 22:41):

(not necessarily formal in lean)

#### Jalex Stark (May 17 2020 at 22:41):

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

#### Jalex Stark (May 17 2020 at 22:42):

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

#### Mario Carneiro (May 17 2020 at 22:43):

heh, the second question implies the answer to the first

#### Jalex Stark (May 17 2020 at 22:43):

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

#### Jalex Stark (May 17 2020 at 22:44):

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

#### Jalex Stark (May 17 2020 at 22:44):

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

#### Jalex Stark (May 17 2020 at 22:45):

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

#### Mario Carneiro (May 17 2020 at 22:45):

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 (May 17 2020 at 22:46):

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 (May 17 2020 at 22:47):

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 (May 17 2020 at 22:47):

it's less efficient than brute force, I guess

#### Mario Carneiro (May 17 2020 at 22:48):

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

#### Mario Carneiro (May 17 2020 at 22:48):

or is that a well known group

#### Jalex Stark (May 17 2020 at 22:50):

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 (May 17 2020 at 22:51):

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

#### Jalex Stark (May 17 2020 at 22:51):

"and so is swapping x with Jxz"

#### Mario Carneiro (May 17 2020 at 22:52):

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 (May 17 2020 at 22:52):

right, so I would write down the normal form

#### Jalex Stark (May 17 2020 at 22:53):

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

#### Mario Carneiro (May 17 2020 at 22:53):

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 (May 17 2020 at 22:53):

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

#### Jalex Stark (May 17 2020 at 22:54):

that seems fine

#### Mario Carneiro (May 17 2020 at 22:54):

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

#### Mario Carneiro (May 17 2020 at 22:55):

in fact I think `norm_num [matrix_mul_2x2]`

would do it

#### Mario Carneiro (May 17 2020 at 22:56):

where `matrix_mul_2x2`

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

#### Jalex Stark (May 17 2020 at 22:56):

that would be cool

#### Jalex Stark (May 17 2020 at 22:56):

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

#### Jalex Stark (May 17 2020 at 22:57):

(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 (May 17 2020 at 22:58):

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 (May 17 2020 at 23:00):

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 (May 17 2020 at 23:17):

(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 (May 18 2020 at 00:20):

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 (May 18 2020 at 03:42):

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

#### Patrick Massot (May 18 2020 at 07:48):

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 (May 18 2020 at 07:56):

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

#### Scott Morrison (May 18 2020 at 08:14):

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 (May 18 2020 at 08:15):

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 (May 18 2020 at 08:17):

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 (May 18 2020 at 13:19):

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 (May 18 2020 at 13:41):

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 (May 18 2020 at 14:02):

I wanted to know why category theory is useful there.

#### Jalex Stark (May 18 2020 at 14:07):

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

#### Jalex Stark (May 18 2020 at 14:08):

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 (May 18 2020 at 14:08):

and take partial traces

#### Jalex Stark (May 18 2020 at 14:09):

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 (May 18 2020 at 14:09):

moving a two-dimensional calculus simplifies that stuff greatly

#### Jalex Stark (May 18 2020 at 14:11):

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 (May 18 2020 at 14:11):

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

#### Jalex Stark (May 18 2020 at 14:11):

yes

#### Patrick Massot (May 18 2020 at 14:11):

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

#### Jalex Stark (May 18 2020 at 14:11):

very much

#### Jalex Stark (May 18 2020 at 14:12):

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 (May 18 2020 at 14:13):

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

#### Jalex Stark (May 18 2020 at 14:14):

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 (May 18 2020 at 14:16):

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

#### Jalex Stark (May 18 2020 at 14:16):

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

#### Jalex Stark (May 18 2020 at 14:20):

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 (May 18 2020 at 14:20):

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 (May 18 2020 at 14:21):

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

#### Jalex Stark (May 18 2020 at 14:22):

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

#### Jalex Stark (May 18 2020 at 14:24):

(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)

Last updated: Dec 20 2023 at 11:08 UTC