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 p

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