This is absolutely not a helpful list for someone who wants to prove things in lean, and just seems like weird gate-keeping. In particular, Proof Trees are completely irrelevant, incompleteness and compactness are only relevant if you are proving things in those specific fields and the only thing you need to know about constructive vs intuitionistic vs classical logic in lean is if you want to use the law of the excluded middle or some non-constructive proofs and tactics, lean won’t force that on you, so you sometimes need to “open classical”. (And this is covered in “Mathematics in Lean” and “Theorem Proving in Lean” at the appropriate place).

Knowing that the Curry-Howard correspondence exists is important if you care about the CS magic that makes lean work and to understand how term mode and tactic mode relate to each other but again it’s really not necessary to understand the correspondence itself to use lean as a proof assistant. (And this is covered extensively in “Theorem proving in Lean” if that’s your jam).

Whatever mathematical background you have is obviously helpful and will widen the scope of what you can do, but you don’t need to learn a huge amount of foundational mathematics to get your hands dirty in lean. For example, “The Mechanics of Proof” by Heather Macbeth was written as a course for 1st year undergrads so only assumes high school maths knowledge. Here’s a list of learning resources that the lean prover community recommends https://leanprover-community.github.io/learn.html

One thing I would add is if you want to learn about proof writing in general there are a lot of good resources out there including “The Book of Proof” which is free online. https://rcsnyder.github.io/open-frontier-curriculum/07-resou...

I personally really enjoyed Jay Cummings’ “Proof: A long-form mathematics textbook” which is on that list as it provides lovely little intros to various areas of mathematics along the way. I have done every exercise in that book and had a lot of fun in the process.

But these aren’t things you necessarily need to do before getting started in lean.