• Hacker News
  • new|
  • comments|
  • show|
  • ask|
  • jobs|
  • muds 9 minutes

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

  • 129387 6 minutes

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

  • homarp 1 hours

    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 29 minutes

    Could you provide a practical example?

    rawland 23 minutes

    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).