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.

Interesting. I always wanted to try Lean, and personally never found an easy way to do it, as it requires installing a plugin in vscode, create a project or reading the lean book. But following the links I've found this nice interactive tutorial for proving 2+2=4 in Peano arithmetic:

https://adam.math.hhu.de/#/g/leanprover-community/nng4/

It's quite instructive.

A thing that still stands out to me is that even in this work we're looking at Lean as a way of verifying a proof, but I do not know how much exploratory work is possible in Lean.

In Rocq/Coq, I've found myself often lost in the weeds when exploring a problem just through tactics mode (half expecting it to handle the more boring machinery), and really do have to think pretty hard about how I get from A to B.

Some of this is, quite simply, me just walking in the wrong direction (if you have multiple things you can induct on, the choice can greatly affect how easy it is to move forward!). I just wish that the computer would be a bit better at helping me realize I'm in the wrong direction.

Stuff like Quickchick[0] helps, but just generally I would love the computer to more actively give me counterexamples to some extent.

[0]: https://github.com/QuickChick/QuickChick

I have a pet (undergraduate complex analysis) formalisation project in Lean, purely for didactic and recreational purposes. I find it rewarding in the same way others may find it rewarding to train for a triathlon - it's often extremely grueling work and it can take forever to make even modest progress. When I actually do get to a "big" result such as defining pi (from scratch) or Cauchy's integral theorem it feels rewarding, but there's a ton of torn out hairs along the way, when linarith is stupider than it should be, I need to spend forever to prove very obvious things, I can't find the tactic I need in mathlib or I realise there's barely anything about triangles in there. For somebody like me without a PhD it also doesn't help that mathlib almost always goes for full generality which makes it hard to use it effectively (although I do understand the reason for it).

I think this is all very exciting but I also think ergonomics will probably need to improve quite a bit before Lean will become mainstream in mathematics.