just saying hi

Stream: new members

[Maciej Pacut]

Hi! Cools stuff going on here, looking forward to learn from you.

[Christian Schöner]

Hi! I'm new here, too! Keep it up, good work!

[Adam Bornemann]

Hi, I'm Adam. I've been working on formalizing quantum mechanics in Lean 4, specifically handling unbounded operators properly (Robertson uncertainty, Stone's theorem, spectral theory). I think this makes Lean the first theorem prover where you can actually do real QM, not just finite-dimensional toy models.

Repo: https://github.com/adambornemann-glitch/LogosLibrary

I'm currently working on Cayley transform before I move on to functional calculus for spectral theory.

Thanks for any scrutiny you can offer.

[Joseph Tooby-Smith]

Hi @Adam Bornemann , you may be interested in the projects/channels #PhysLean and #Quantum information

[Yoh Tanimoto]

there is an ongoing work on the spectral theorem, see the discussion around
#mathlib4 > L^infty as C*-algebra @ 💬
I'm hoping to come back to work after the exams are done in february