MathCode, Mathematical Coding Agent

(math-ai-org.github.io)

16 points | by homarp 1 hour ago

3 comments

muds 14 minutes ago
Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
homarp 1 hour 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 34 minutes ago
  Could you provide a practical example?
  [-]
  - rawland 28 minutes 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 11 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!"