Interesting work. Is this a wrapper around the AUTOLEAN project (<a href="https:&#x2F;&#x2F;github.com&#x2F;T3S1AMAX&#x2F;autolean" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;T3S1AMAX&#x2F;autolean</a>)?

the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.

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

And doesn’t use as many tokens, at least for now.

Instructions:<p>&quot;git clone <a href="https:&#x2F;&#x2F;github.com&#x2F;math-ai-org&#x2F;mathcode.git" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;math-ai-org&#x2F;mathcode.git</a>&quot;<p>What a luddite! It should be &quot;Claude, write me a math coding agent. Make no mistakes!&quot;

There is one in the quickstart:<p><pre><code>    mathcode -p &quot;prove that the square of an even number is even&quot;
</code></pre>
<a href="https:&#x2F;&#x2F;math-ai-org.github.io&#x2F;mathcode&#x2F;#quickstart" rel="nofollow">https:&#x2F;&#x2F;math-ai-org.github.io&#x2F;mathcode&#x2F;#quickstart</a> - if you look very closely, the screenshot at the top actually shows the output (and the solution).

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.