A tangential topic, but anyone have recommendations for proof-checking languages? Lean, Isabelle, Coq, Idris are the few I know about. I've only ever used Isabelle, but can't really tell the difference between them. Anyone here used more than one, and can tell why people pick one over the other?
Isabelle is my favorite, and it's the one I've used the most, if only because sledgehammer is super cool, but Coq is neat as well. It has coqhammer (a word I will not say at work), and that works ok but it didn't seem to work as well as sledgehammer did for me.
Coq is much more type-theory focused, which I do think lends it a bit better to a regular programming language. Isabelle feels a lot more predicate-logic and set-theory-ish to me, which is useful in its own right but I don't feel maps quite as cleanly to code (though the Isabelle code exporter has generally worked fine).
They are pretty similar as languages. In general I would recommend Lean because the open source community is very active and helpful and you can easily get help with whatever you're doing on Zulip. (Zulip is a Slack/Discord alternative.) The other ones are technically open source but the developers are far less engaged with the public.
Proof-checking languages are still just quite hard to use, compared to a regular programming language. So you're going to need assistance in order to get things done, and the Lean community is currently the best at that.
I have personally tried Coq and Lean and stuck to Lean as it has much better tooling, documentation and usability while being functionally similar to Coq.
Caveat that I have only used Coq and Lean side by side for about a month before deciding to stick with Lean.
One consideration in choosing a proof assistant is the type of proofs you are doing. For example, mathematicians often lean towards Lean (pun intended), while those in programming languages favour Coq or Isabelle, among others.
It depends on the kind of proofs you deal with. If you need to write math in general terms, you can't avoid dealing with at some level the equivalent of category theory and you will want natural access to dependent types. So Coq and Lean. Otoh HOL is easy to comprehend and sufficient for almost everything else. And HOL based provers are designed to work with ATPs. HOL Light in particular is just another OCaml program and all terms and data structures can be easily manipulated in OCaml.
If you mean dependence on VS Code, there are emacs and neovim packages for Lean; some of the core devs use those exclusively. Also note that de Moura is no longer at Microsoft and Lean is not an MS product.
