I’m yes on this, almost completely.

But. I’m also thoughtful about proving things — my own math experience was decades ago, but I spent a lot of ‘slow thought’ time mulling over whatever my assignments were, trying things on paper, soaking up second hand smoke and coffee, your basic math paradise stuff.

I wonder if using Lean here could lead to some flailing / random checking / spewing. I haven’t worked with Lean much, although I did do a few rounds with coq five or ten years ago; my memory is that I mostly futzed with it and tried things.

Upshot - a solver might be great for a lot of things. But I wonder if it will cut out some of this slow thoughtful back-and-forth that leads to internalization, conceptualization, and sometimes new ideas. Any thoughts on this?