▲ 40 points
back
14 comments
Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
What commercial setting do you want to use a Lean theorem-proving agent in?
It's AI generated, so licensing terms are unenforceable.
Maybe consider an integration with theoremdb.org?
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.
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
Instructions:
"git clone https://github.com/math-ai-org/mathcode.git"
What a luddite! It should be "Claude, write me a math coding agent. Make no mistakes!"
git clone is slightly faster
And doesn’t use as many tokens, at least for now.
I just replaced git clone with a script which fetches the README.md and sets of a fleet of agents to do a cleanroom reimplementation.
Lets me ignore the LICENSE.md file, and use how I want.
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.
Could you provide a practical example?
There is one in the quickstart:
mathcode -p "prove that the square of an even number is even"