As far as an entry point, I would highly recommend first trying the natural number game. It is fun (it is a game-based tutorial to Lean), it is short, it has a low barrier to entry (it is just in browser), and it would teach you things that are universal to most proof assistants (such as the inductive definition of the natural numbers and rewriting). Unfortunately, the sequel "real number game" hasn't been developed yet, since I think that is what you are looking for.
After that, I would find a proof assistant with:
- Good documentation. You want to be able to learn the language well, so you want good documentation, especially a good tutorial.
- Nice tooling. You want your experience working in that language to be positive with a good IDE, good interactivity, and good error messages.
- A vibrant and welcoming community. When you get stuck (on something which is completely trivial mathematically), you want to be able to just ask for help in a low barrier environment. Many proof assistants have chat-based communities on Zulip and Discord.
- Priorities similar to yours. Every proof assistant community comes with an implicit set of priorities. For example, do users tend to work on classical mathematics or constructive mathematics? Is the focus on building a library of mathematics, or on verifying algorithms in computer science, or on verifying computer code? Is it a single monolithic project with a central code repository, or is it a bunch of individual projects focusing on separate topics (which may or may not be compatible).
I think from what you said, Lean 3 might fit your interests. It has a decent tutorial (Theorem Proving in Lean), it uses a modern and popular IDE (VS Code), it has a very vibrant and supportive community on Zulip, and it is focused on building a library of classical mathematics covering all topics from undergraduate mathematics up to the cutting edge of research.
Its downsides are that Lean isn't very stable (especially with the current 2022 transition from Lean 3 to Lean 4). So unless your code goes into mathlib (the main mathematical repo), it will possibly bit rot. Also, mathlib already has a lot of analysis, but it is done in a very general way to make it widely applicable to other application. So for example, a theorem might be about Banach spaces instead of $\mathbb{R}^n$ for example.
A second option is Isabelle which is also focused on building a library of classical mathematics, and has a lot of analysis already. Also, maybe (???) its Isar style of proofs is more similar to what you are looking for with keeping proofs closer to the original mathematics, but honestly, I don't know if any proof assistant does this well since formal and informal mathematics are just so different.
But I don't want to say that these are the only options. See Proof assistants for beginners - a comparison for (opinionated) views on what proof assistants to start with. (Also, if you plan on doing very advanced mathematics, I would look at Are some proof assistants better suited for given areas of math than others? .) But don't let decision paralysis prevent you from learning one. Once you learn one, it is easier to transition to any other.
