MathCode, Mathematical Coding Agent 5 hours ago (math-ai-org.github.io) 14 comments homarp Reply Add to library muds 4 hours ago Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)? eisbaw 3 hours ago the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean. owlbite 3 hours ago Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting. jrflo 1 hour ago What commercial setting do you want to use a Lean theorem-proving agent in? a2ff6eeb0 2 hours ago It's AI generated, so licensing terms are unenforceable. philipfweiss 2 hours ago Maybe consider an integration with theoremdb.org? fractorial 1 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. homarp 5 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. seunosewa 4 hours ago Could you provide a practical example? rawland 4 hours ago There is one in the quickstart: mathcode -p "prove that the square of an even number is even" https://math-ai-org.github.io/mathcode/#quickstart - if you look very closely, the screenshot at the top actually shows the output (and the solution). 129387 4 hours ago [dead] eisbaw 3 hours ago git clone is slightly faster gumby 3 hours ago And doesn’t use as many tokens, at least for now. 1 reply →
muds 4 hours ago Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
eisbaw 3 hours ago the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
owlbite 3 hours ago Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting. jrflo 1 hour ago What commercial setting do you want to use a Lean theorem-proving agent in? a2ff6eeb0 2 hours ago It's AI generated, so licensing terms are unenforceable.
philipfweiss 2 hours ago Maybe consider an integration with theoremdb.org? fractorial 1 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.
fractorial 1 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.
homarp 5 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. seunosewa 4 hours ago Could you provide a practical example? rawland 4 hours ago There is one in the quickstart: mathcode -p "prove that the square of an even number is even" https://math-ai-org.github.io/mathcode/#quickstart - if you look very closely, the screenshot at the top actually shows the output (and the solution).
seunosewa 4 hours ago Could you provide a practical example? rawland 4 hours ago There is one in the quickstart: mathcode -p "prove that the square of an even number is even" https://math-ai-org.github.io/mathcode/#quickstart - if you look very closely, the screenshot at the top actually shows the output (and the solution).
rawland 4 hours ago There is one in the quickstart: mathcode -p "prove that the square of an even number is even" https://math-ai-org.github.io/mathcode/#quickstart - if you look very closely, the screenshot at the top actually shows the output (and the solution).
129387 4 hours ago [dead] eisbaw 3 hours ago git clone is slightly faster gumby 3 hours ago And doesn’t use as many tokens, at least for now. 1 reply →
eisbaw 3 hours ago git clone is slightly faster gumby 3 hours ago And doesn’t use as many tokens, at least for now. 1 reply →
Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
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.
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:
https://math-ai-org.github.io/mathcode/#quickstart - if you look very closely, the screenshot at the top actually shows the output (and the solution).
[dead]
git clone is slightly faster
And doesn’t use as many tokens, at least for now.
1 reply →