For anyone that's interested in formalizing mathematics but wished there was an easier way to do it, I've been working on a different sort of theorem prover recently.
The idea is that there's a small AI built into the VS Code extension that will fill in the details of proofs for you. Check it out if you're interested in this sort of thing!