I would really like to dip my toe into the theorem proving waters from a scientific/mathematical perspective.
I'm not sure whether to start with Coq, Agda, Isabelle or Lean. Does anyone on HN have a feeling as to a sensible one to start with?
If you search the web for "Software Foundations in X", you will find partial ports of some of the initial chapters to pretty much any other proof assistant. Maybe nowadays they are full, complete ones that would allow you to use Isabelle or Lean instead.
This isn't really a problem per se, but instead an invitation to look into, say, Agda to see that side of things, too.
(One other approach is to generate a "declarative", human-readable version of the proof directly from the proof term. Very old versions of Coq (6.x series) and IIRC even Agda (1.x) could essentially do this. Declarative proof mode integrates better with complex tactics however - proof terms can sometimes get a bit weird.)
The advantage of Agda is that everyone else does, too. This provides two things: one, there's a huge set of examples of how people have constructed their proof terms which encode best practices and are themselves designed to be as readable as possible, and two, people also build tooling which helps you to make them.
In Coq, since tactics are primary, you end up with things like Sledgehammer. This is super practical and useful for tactics management, but it's a whole culture that will take you further and further away from understanding how proof terms work.
Agda is pretty finicky, proving stuff in it is harder and the entire project feels more researchy (as a playground to try out ideas for programming languages).
Lean seems promising, but it's still kind of new, so compared to Coq will not find as much documentation, and there are fewer people on Stack Overflow to answer questions.