re entry into math

Stream: new members

[kapil verma]

Last I studied theoretical math was 11 years ago while studying Physics (GTR, QM, chaos theory etc) ... Been into programming since then .. want to explore lean and probably try implementing some basic theorems in it .... What'd be a good math book to kind of re-enter mathematics and go beyond https://leanprover.github.io/theorem_proving_in_lean/

[Logan Murphy]

What sort of maths are you interested in?

[kapil verma]

The type that gets used in physics tbh ... Not sure what it's called

[kapil verma]

Or anything that can lead up to that in time in lean

[Notification Bot]

This topic was moved here from #general > good re-entry into theoretical math by Eric Wieser.

[Moritz Doll]

Lots of stuff in quantum mechanics is just :tm: functional analysis. I think we have quite some progress on C*-algebras and on Hilbert space theory. I don't think we have anything on unbounded operators (-Δ + V is an unbounded operator and there is lots of stuff in mathematical physics about abstract results for unbounded self-adjoint operators (and we don't even have the definitions for that)). As for books, there is the Conway's functional analysis book, there is monograph series by Reed-Simon and probably lots of other good books I am forgetting.

[Moritz Doll]

What is GTR?

[Moritz Doll]

I don't know anything about chaos theory, but I think it is essentially dynamical systems and ergodic theory, for which I only know the book by Einsiedler-Ward and I have no clue what the state of that is in mathlib.

[Andrew Yang]

I guess he is referring to the General (Theory of?) Relativity.
Now that we have Picard-Lindelöf in mathlib, I think we are probably able to do some more basic calculations on manifolds now, which I think the people working on the sphere eversion project might be pushing forward a bit?

[Moritz Doll]

without serious support for vector bundles on smooth manifolds there is no point in trying to prove anything related to general relativity. Special relativity is possible, but I doubt that there are lots of interesting theorems to prove.