The part of your answer I like best is a "Python of proof assistants". :)
When I see "Python" I read "a programming language which is deceptively simple on the surface level but has totally crazy semantics". On the funnier side of this craziness we have "Negatypes" and there are long lists of "gotchas" including confusing syntax.
I don't think proof assistants even remotely approach that level of sophistication and "industrial strength". :'D
For one thing proof assistants are built on some variant of Type Theory thus they have mostly straightforward core semantics. Due to the fact you can't practically prove soundness for too hairy theory and soundness is a pretty much a requirement for an acceptable Type Theory. Though we're doing much better on the surface syntax level especially with user-extensible parsers of Coq and Lean! :D
Anyway jokes aside I would advertise Isabelle/HOL as a good proof assistant for beginners. Let's examine how it fares on criteria you mentioned.
How is it is to pick as a language?
Funny thing it comprises several languages, two most important of which are a language for writing programs and a language for writing proofs.
I consider it a good thing for beginners: instead of learning one complicated language for everything (
Type? Wait there's also
SProp?!) you can learn two simpler ones, or even only proof language (Isar in this case) if you don't care about programming per se. Even if you do care about programming Isabelle/HOL provides a variant of ML for that, which is in my opinion the closest to "Python of statically typed functional languages" in the sense of the most straightforward syntax and semantics. It doesn't have Dependent Types for a change! :D
And for writing proofs Isabelle offers aforementioned Isar language which is pretty much a benchmark for clear structured proofs. On top of that Isabelle/Isar seamlessly integrates very powerful proof automation keeping structure and readability intact which IMO helps beginners a great deal.
How easy is it to install and connect with popular IDEs (such as Visual Studio Code)?
Installation consists of downloading and unpacking the official distribution. And there's no third step — it's immediately ready to run with "batteries included", including third-party tools like Z3, E prover, etc.
As for connecting to popular IDEs, I suspect not very well at all... :D But on the bright side Isabelle/HOL distribution includes its own jEdit-based IDE quite tailored for easy access to system's facilities.
And when built-in search facilities are not enough you can reach for https://behemoth.cl.cam.ac.uk/search/ which also looks in the great Archive of Formal Proofs :)
Availability of learning material
Again the standard distribution includes quite a number of PDFs ranging from tutorials to comprehensive manuals. The most important of them is Programming and Proving in Isabelle/HOL which not only introduces Isabelle/HOL/Isar from scratch but also teaches basics of programming and formal logic.
Additionally there's a free book on algorithms and data structures verification and another one on formally verified semantics of programming languages. Both are very approachable and beginner-friendly in my view.
Availability of online forums willing to cater to beginners
Answer to this question I don't know but maybe this StackExchange corner will be of some help? :D
PS. I hope I don't sound mean or dismissive towards Python or other proof assistants... That's nothing more than my personal opinion based on very limited experience 'coz I am but a beginner myself and never formalized anything complicated.