Could you provide a practical example?

    mathcode -p "prove that the square of an even number is even"

I’ve written a lot of Lean for economic modeling (so take this with the caveat that it’s not frontier-level mathematics research) but I think this problem is overstated. If you follow good engineering standards—keep primitives composable and design abstraction well—it’s not so hard to understand enough Lean to ensure the formalized statement is correct.

In part this is possible because mathlib is very well-designed and has a very good API (in no small part because they’re willing to make breaking changes all the time), so building on top of it makes life much easier.

What commercial setting do you want to use a Lean theorem-proving agent in?

It's AI generated, so licensing terms are unenforceable.

To be clear, I am deep into auto-research, but hooking up slop to slop is just unlikely to produce anything valuable.

Value is in how maths is communicated: The process, frustrations, triumphs, etc.

We have to able to take generated formalizations from “it compiles” to “it is correct” before crystallizing them.