Alternate characterization of Hilbert spaces

Stream: general

[Alex Meiburg]

I see people doing work like https://twitter.com/chrisheunen/status/1747286108860248330 , which is a fully category-theory-first description of what "complex numbers" are, what a "finite dimensional Hilbert space" is, and so on. It seems interesting. As definitely-not-a-category-theorist, is that something that could make sense to write in Lean? Like, that the structures obeying these axioms are in one-to-one correspondence with finite-dimensional Hilbert spaces?

[Alex Meiburg]

(this is not, mm, a serious question about anything. Just sort of wondering what this would even look like)

[Kim Morrison]

Yes, this stuff would definitely be formalizable in Lean, and while it's a bit niche it's not obviously out of scope for Mathlib. You'd certainly find interesting gaps in the library that deserve filling.