muds4 hours ago
Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
eisbaw3 hours ago
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
owlbite3 hours ago
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
jrfloan hour ago
What commercial setting do you want to use a Lean theorem-proving agent in?
a2ff6eeb02 hours ago
It's AI generated, so licensing terms are unenforceable.
philipfweiss2 hours ago
Maybe consider an integration with theoremdb.org?
fractorialan hour ago
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.
homarpop5 hours ago
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.
seunosewa4 hours ago
Could you provide a practical example?
rawland4 hours ago
There is one in the quickstart:
mathcode -p "prove that the square of an even number is even"
1293874 hours ago
[dead]
eisbaw3 hours ago
git clone is slightly faster
gumby3 hours ago
And doesn’t use as many tokens, at least for now.
black_knightan hour ago
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.