MathCode, Mathematical Coding Agent

 (math-ai-org.github.io)

41 points | by homarp 4 hours ago

6 comments

  • muds 2 hours ago
    Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
  • owlbite 2 hours ago
    Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
    [-]
    • jrflo 42 minutes ago
      What commercial setting do you want to use a Lean theorem-proving agent in?
    • a2ff6eeb0 1 hour ago
      It's AI generated, so licensing terms are unenforceable.
  • philipfweiss 1 hour ago
    Maybe consider an integration with theoremdb.org?
    [-]
    • fractorial 34 minutes ago
      To be clear, I am deep into auto-research, but hooking up slop to slop is just unlikely to produce anything valuable.

      Value is in how maths is communicated: The process, frustrations, triumphs, etc.

      We have to able to take generated formalizations from “it compiles” to “it is correct” before crystallizing them.

  • eisbaw 2 hours ago
    the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
  • 129387 2 hours 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 2 hours ago
      git clone is slightly faster
      [-]
      • gumby 2 hours ago
        And doesn’t use as many tokens, at least for now.
        [-]
        • black_knight 15 minutes ago
          I just replaced git clone with a script which fetches the README.md and sets of a fleet of agents to do a cleanroom reimplementation.

          Lets me ignore the LICENSE.md file, and use how I want.

  • homarp 4 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.
    [-]