Zulip Chat Archive

Stream: general

Topic: Physics?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Andreas Swerdlow (Sep 27 2018 at 13:58):

I’m pretty sure I fixed the issue with Hilbert space so hope to PR soon

view this post on Zulip Andreas Swerdlow (Sep 27 2018 at 14:00):

Although I only have one trivial lemma about Hilbert Spaces specifically

view this post on Zulip 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?

view this post on Zulip 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