Zulip Chat Archive

Stream: new members

Topic: re entry into math

kapil verma (Mar 10 2022 at 17:53):

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 (Mar 10 2022 at 17:54):

What sort of maths are you interested in?

kapil verma (Mar 10 2022 at 17:55):

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

kapil verma (Mar 10 2022 at 18:13):

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

Notification Bot (Mar 10 2022 at 19:08):

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

Moritz Doll (Mar 10 2022 at 19:11):

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 (Mar 10 2022 at 19:11):

What is GTR?

Moritz Doll (Mar 10 2022 at 19:16):

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 (Mar 10 2022 at 19:23):

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 (Mar 10 2022 at 19:41):

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.

Last updated: Dec 20 2023 at 11:08 UTC