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.
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.
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