Zulip Chat Archive

Stream: general

Topic: Physics?

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

I'm a Physicist but am just starting to learn Lean (as in a few days ago). I have almost no experience with proofs. I'm interested in figuring out how Lean can be applied to mathematical derivations in Physics.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib