Comment by ndriscoll

It doesn't require an expert though. That was kind of my point. If you've taken an intro proof class (so the intro class for math majors/the topic), and if you've fiddled with Lean a bit (e.g. played some of the Natural Numbers Game another commenter linked), you'll know it's easy (source: I did math in my undergrad, and have fiddled with Lean a bit). Honestly I expect intro proof classes will start to be centered around something like Lean soonish if some aren't already incorporating it, and we'll see math majors more explicitly making the connection between program and proof.

Like if someone were incredulous that we could reasonably analyze running time and memory usage of something like merge sort and I said that's a standard example in an intro algorithms course, presumably people would be like "yeah it is".