Something that’s been on my mind as one of the key benefits of theorem provers like #leanlang #Lean4 for someone like me is they enable storing reasoning long term much more effectively than written proofs as well as forcing local reasoning.
I left academic #math about 8 years ago to have a more stable and less demanding career in tech. But I always intended to continue my research in an informal capacity, just for love of the subject. I managed to do a halfway decent job as well, but the big problem is that I would work on my math maybe once or twice a week. And here I found that I would always lose an inordinate amount of time with context switching. My work style until that point had been to develop a complete sketch proof and fill in the details. Importantly this required me to always maintain a sort of complete picture of the proof in my head. But now being unable to focus full time on cleaning up the sketch I would lose so much time trying to remember the notation that I created as well as reloading the whole strategy.
My time in tech has exposed me to a bunch of programming languages. At first Python which sort of fit with this sloppy idea of just keeping the whole program in my had with a lot of global variables. But bit by bit I was exposed to other more rigorous languages: first #scala and then #rust #rustlang . It was really in rust that I started to get the idea of local reasoning.
Especially rustlang folks seemed interested in formal methods and bit by bit I got exposed to those languages through them.
Now especially with “sorry” I can incrementally work on goals with consistent notation and without having to load the full context as the intermediate goal is right there.
=> More informations about this toot | View the thread | More toots from gigapixel@mathstodon.xyz
=> View rustlang tag | View rust tag | View scala tag | View math tag | View Lean4 tag | View LeanLang tag This content has been proxied by September (3851b).Proxy Information
text/gemini