#I want to be clear that a lot of advanced math is in mathlib already. like we’re not behind on how advanced it can be really

[as-if-and-only-if]

anyway, on a more serious note, we’re really in the early stages of formal verification. the notes are right in feeling that formalization is currently annoying and time consuming. but it’s become easier to just reach for a definition or a structure without much consternation, and from what I’ve seen Lean is pretty focused specifically on making that process easier.

in just the past year or so I’ve seen tactics and interface infrastructure emerge for lean specifically to make the formalization process easier, like search tools (loogle and moogle—sorry, I didn’t name these), ways to add in all the assumptions you want (just as usual in natural language, but a pain during formalization), proof automation aids like `hint` which just tries a bunch of different high-powered tactics for you (some of which do their own library searching, in different ways), linters to help you see when you’ve gone astray in an obvious way, dynamic widgets for visualizing things, etc.

anyway this isn’t to say that formalizing is easy yet, but it has been wild to see the interface get better so quickly. (A lot of this is due to the new metaprogramming capabilities in Lean 4.) With all the funding they’ve got I imagine it’ll continue to improve.

I wonder when it (or something inspired by it/which learns from it) will be close enough to mathematical practice that it’s more or less no more effort to verify your proof than to write it (and the annoying in between steps that the original post is talking about will be automated and still not need to be written!). Past that point, proof assistants will actually be able to assist you in proofs! (imagine that!)

anyway my point is that in my experience we’re very tangibly heading in that direction, and it seems inevitable that one day we’ll get there.

i dont like how "trust-based" a lot of advanced math is. like, a lot of papers will at various points say "we did this calculation, and got this", (like, two steps in equation manipulation will be related in a very unclear way) and not show you the calculation. and i get it, typing up the calculation is annoying. but often, i will try to replicate the calculation, and will not be able to! and generally i assume this is because i am much worse at math than the author. but like. i guess i just have to take your word for it that the calculation works! this sucks! math isnt supposed to be like this! thats the whole point!