Wojciech Nawrocki (Sep 27 2018 at 13:02):
Hey, I'm curious - are there any physicists here looking at formalising some of the vector algebra for quantum theory? I couldn't find anything related to e.g. Hilbert spaces.
Kevin Buzzard (Sep 27 2018 at 13:11):
A first year undergraduate student of mine formalised the definition of Hilbert spaces as part of their summer project, but I don't think there's anything in the official maths library.
Sean Leather (Sep 27 2018 at 13:13):
I don't recall any physicists coming forward openly. But if you are one, you'd better beware.
Kevin Buzzard (Sep 27 2018 at 13:15):
https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Banach%20spaces.lean and and there are inner product spaces too, but actually I don't see Hilbert space yet.
Andreas Swerdlow (Sep 27 2018 at 13:58):
I’m pretty sure I fixed the issue with Hilbert space so hope to PR soon
Andreas Swerdlow (Sep 27 2018 at 14:00):
Although I only have one trivial lemma about Hilbert Spaces specifically
Wojciech Nawrocki (Sep 27 2018 at 22:29):
Ok, thanks! I was looking at (maybe) formalising some results that require notions of a Hilbert space.
@Andreas Swerdlow do you mean it might be included in mathlib at some point?
Andreas Swerdlow (Sep 27 2018 at 23:08):
Hopefully, but it probably needs some cleaning up
Last updated: May 16 2021 at 21:11 UTC