MathCode, Mathematical Coding Agent

Posted by homarp |2 hours ago |6 comments

owlbite 8 minutes ago

Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.

muds 28 minutes ago

Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?

homarp 2 hours ago[1 more]

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.

129387 25 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!"