A terminal AI coding assistant with a built-in math formalization engine — describe a problem in plain language and it converts it into a Lean 4 theorem and attempts a formal proof.
seunosewa•Aug 16, 2026
Could you provide a practical example?
rawland•Aug 16, 2026
There is one in the quickstart:
mathcode -p "prove that the square of an even number is even"
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
a2ff6eeb0•Aug 16, 2026
It's AI generated, so licensing terms are unenforceable.
a2ff6eeb0•Aug 16, 2026
Or, more accurately: it's not possible to apply copyright to generated code; if you don't release it, it's a trade secret, but if you do, people can use it how they please.
jrflo•Aug 16, 2026
What commercial setting do you want to use a Lean theorem-proving agent in?
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
bayesnet•Aug 16, 2026
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.
wanderlust123•Aug 17, 2026
What kind of economic modelling uses Lean?
philipfweiss•Aug 16, 2026
Maybe consider an integration with theoremdb.org?
fractorial•Aug 16, 2026
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.
andxor•Aug 17, 2026
> hooking up slop to slop is just unlikely to produce anything valuable
Do you have a formal proof of that?
skew-aberration•Aug 17, 2026
Premises:
Garbage in implies garbage out (first principle of computer science)
The input is possibly, but not necessarily garbage (definition of slop)
By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.
5 Comments
[1] http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF
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.
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.
Do you have a formal proof of that?
By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.