I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my work. I am currently going through the natural number game and it's brilliant.
Are there any limitations or problems I may run into with my plan? I am new to proof assistants and am not sure what the limitations of such software is (I am a software engineer by trade).
I have a degree in software engineering and share the same goal as yours.
Truth be told, you can learn more about proof by reading introductory maths book at university level and start writing informal proofs. A good book recommendation will be Velleman's "How to Prove It: A Structured Approach". The maths discord server is a great place to ask about your maths problem, url: https://discord.gg/math.
If you're determine on continuing this path, I can share some of my experience after learning Coq for nearly two months, especially on how writing proofs in Coq is different from writing proofs on paper.
I can't comment on the differences between Coq and other proof assistants because I'm not familiar with them. But Coq and Lean might be similar because they are based on the same underlying type theory: CoC. Isabelle/HOL is based on a simpler theory instead, but they excel in producing very readable proof documents using Isar.
In programming parlance, informal proofs are pseudocodes. They're high level and written only to communicate with other mathematicians. Informal proofs are good enough as long as the other party understands what you're trying to communicate. However, you're required to fill in a lot of details by yourself.
On the other hand, formal proofs in Coq are like writing algorithms in an actual programming language. It's similar to how you'll write programs in Standard ML, OCaml or Haskell. You have to be correct down to the finest details because, now, instead of convincing an intelligent person, you have to convince Coq that your proofs are indeed correct.
It means that you need to be familiar with both constructive type theory and classical set theory if you're going to learn maths with Coq. Why? You need to understand classical set theory to understand mainstream maths; then constructive type theory to translate those knowledge into Coq.
There are two main differences between them: (i) constructive vs classical maths, (ii) type theory vs set theory.
Classical maths is what you learn from most maths textbook (e.g. including the Velleman book I recommend above). On the other hand, constructive maths is maths done without principle of excluded middle. No proof by contradiction as well. I don't know of other subtle differences.
In set theory, new mathematical objects are always defined as sets or elements of some sets. Type theory is a bit familiar to you if you've programmed in static typed functional programming language. New mathematical objects are introduced very much like how you define new data structures in programming languages.
Don't underestimate the time and efforts needed to master your tool! You can start right away with pen and paper with informal proofs. But since you're going to write maths in Coq, you need to learn how Coq works!
This might be surprising. Your proofs written with pen and paper won't get outdated, but your proofs written in a proof assistant will! Why? Your proofs written in proof assistants are essentially programs, so it's tied to specific versions of your proof assistant.
It means that if your proof assistant introduces breaking changes, your proofs will no longer work with the newer version of the proof assistant. A notable example is the port of mathlib from Lean 3 to Lean 4.
So, maintainability and portability across versions is a factor of consideration during your proof development. It might be no different from software development at this stage.
Ask for help in Coq zulip or here. People are busy, but they are friendly and welcoming. Feel free to chat with me on Coq zulip, my username there is Jiahong Lee.
Hope that my experience will be useful to you. Thanks!
I am in a little bit the same boat, in that I am (partly) self-taught and I will say that using a proof system has been a significant help to me (although I will say in conjunction with informal proofs, not instead of).
In my case the most approachable one has been Metamath (and offshoots of metamath, but none of those are as active or well developed as metamath itself). This is because metamath lets you see every step (in a more human-readable form than in a proof system where there is no particular focus on making reducing the number of steps or otherwise making them something you'd normally see at all).
Probably the biggest pitfall I have found is the learning curve (starting with just installing some of these systems, to the fact that the documentation for some of them assumes you already know type theory - which as far as I can tell is a problem of how they are explained as much as a genuine catch 22 in terms of whether you can really get started before you know what you are trying to learn). Oh, and choosing which system is most likely to be helpful in a crowded field - I installed quite a few before I got up the curve of learning how they work and figuring out what sorts of problems/exercises I might take on.
I could write more, including about my own journey from not having written a proof (formal or otherwise) in years, to being one of the significant contributors to the metamath proof collection, but perhaps the best place to point you is the mini-FAQ on https://us.metamath.org/index.html especially the question "Will Metamath help me learn abstract mathematics?"
