https://leanprover-community.github.io/
I think it is the future of mathematics. Yes I know that 99% of mathematicians will disagree. That's not unusual for a fundamental change to how people think. And yes I know it will take a very long time for this change to manifest itself. That is also not unusual for a fundamental change to how people think. But don't underestimate the exponential power of real formal mathematics. What mathematicians are currently calling "formal" proofs aren't. They are just informal proofs with lots of details. Again, 99% of mathematicians will strongly disagree. However eventually we will see math journals dedicated to formally proven correct mathematics. And those proof will start to be regarded above and beyond the current informal proofs. It will take a long time. But IMHO it is inevitable.