MathCode, Mathematical Coding Agent

5 comments

• muds 1 hour ago
  Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
• eisbaw 30 minutes ago
  the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
• owlbite 49 minutes ago
  Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
• 129387 1 hour 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 32 minutes ago
    git clone is slightly faster
    [-]
    • gumby 29 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 hour ago
    Could you provide a practical example?
    [-]
    • rawland 1 hour 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).