3 ms·

I 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 start

I 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 ago
Also, VS Code for Lean is beyond awesome. And the Emacs package is not bad either.
- eggy 5y ago
  I 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.