NHacker Next
  • new
  • past
  • show
  • ask
  • show
  • jobs
  • submit
▲MathCode, Mathematical Coding Agent (math-ai-org.github.io)
27 points by homarp 2 hours ago | 9 comments
muds 55 minutes ago [-]
Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
eisbaw 15 minutes ago [-]
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
owlbite 35 minutes ago [-]
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
129387 51 minutes ago [-]
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!"

eisbaw 18 minutes ago [-]
git clone is slightly faster
gumby 15 minutes ago [-]
And doesn’t use as many tokens, at least for now.
homarp 2 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 1 hours ago [-]
Could you provide a practical example?
rawland 1 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).
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact
Rendered at 20:35:15 GMT+0000 (Coordinated Universal Time) with Vercel.