I personally prefer Agda to Lean or Coq [1] to prove my theorems but this frontier is imho among the most exciting research in theoretical CS in many many decades. I really wish more programmers and mathematicians knew about automated theorem proving and automated reasoning. It's nothing short of revolutionary and I think next generation of pure mathematicians will use these as a crucial tool in their research.

[1] It's a personal preference but Agda is simply a much better language with almost limitless metaprogramming which allows me to write proofs close to as they'd appear in prose math papers. It has a smaller ecosystem though. I've never seen a proof in any other language I personally didn't think would be much more readable/simpler in Agda.