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

Ahh, that is a valid point; so it's not quite as clear as using something like quick check, but it does feel like there is increasing interest and activity in people trying out doing exploratory maths in Lean itself.

I mention it in the blog post, but one project in that direction is Terence Tao's equational_theories project (https://teorth.github.io/equational_theories/), where it seems like a bunch of hobbyists and mathematicians are working together using Lean to prove new mathematics enabled by Lean.

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.

I'm currently creating an interactive tutorial on Agda, with lots of embedded exercises (running purely in the browser/on a server, no installation required), perhaps it is useful to some:

https://lets-play-agda.quasicoherent.io/

Oh, really? I'm curious what exactly you mean by limitless metaprogramming. I've really been drawn into Lean specifically because of how easy to extend and malleable the language itself is, so if Agda is even more so then I'd be really eager to try that out.

e.g.:

- embedding a prolog/asp DSL: https://github.com/kiranandcode/cleango

- embedding a tex/latex DSL: https://github.com/kiranandcode/LeanTeX

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.

Fwiw there's also an Emacs plugin which is what I use and it works really well.

For using Lean as a theorem prover, this book is pretty good: https://github.com/lean-forward/logical_verification_2024

Also, Lean is also remarkably usable as a programming language itself, which might give an easier onboarding ramp: https://lean-lang.org/functional_programming_in_lean/

Lean is more complex to develop in than most programming languages since it relies heavily on interactive programming, i.e. the context pane. The "easy way" is with a plugin.

If you're interested in learning more about Lean for writing proofs, I would recommend The Mechanics of Proof [0]. It strips out a lot of the convenience tactics in Mathlib to focus on the more primitive mechanisms Mathlib builds on.

[0]: https://hrmacbeth.github.io/math2001/index.html

Ironically, the website broke, and became stuck on the "rw[one_is_succ_zero]" rewrite rule, continually telling me that "rfl" isn't valid. Sigh.