3 ms·
I have copies of Newton's PM, W&R's Pricipia and The Elements for post-apocalyptic reading ;) For someone with little computational theorem proving, but not ne
by eggy 5y ago
I have copies of Newton's PM, W&R's Pricipia and The Elements for post-apocalyptic reading ;)
For someone with little computational theorem proving, but not new to real analysis, would it be best to start with Lean vs. Coq? I have heard that HoTT has put Coq up front for this, but that Lean is much easier to get started with as someone with a mathematical background vs. a computational mathematics background, and that Lean tops out after you really dig in. Any tips would be much appreciated!
Thanks!
- ocschwar 5y agoI had no experience with proof assistants until this year, and no real interest in formal proofs except as a QA method for statistical analysis code, so I started from a blank slate with almost no prior art to walk through. Lean is way the hell easier to deal with than Coq, and the video walkthroughs from the Xena project are amazingly good for understanding this stuff.
- ocschwar 5y agoAlso, VS Code for Lean is beyond awesome. And the Emacs package is not bad either.
- eggy 5y agoI am going to have to try Lean. I find I sometimes fall into the trap of wanting the ideal tool or solution when good enough will get me further. The little I've looked at Lean so far, has been encouraging from when I tried to play with Coq several years ago.