MathCode, Mathematical Coding Agent

6 comments

• muds 4 hours ago
  Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
• eisbaw 3 hours ago
  the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
• owlbite 3 hours ago
  Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
  [-]
  • jrflo 1 hour ago
    What commercial setting do you want to use a Lean theorem-proving agent in?
    [-]
    • ljwoods2 4 minutes ago
      Mathematics, Inc [1], I assume

      [1] http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF
  • a2ff6eeb0 2 hours ago
    It's AI generated, so licensing terms are unenforceable.
• philipfweiss 2 hours ago
  Maybe consider an integration with theoremdb.org?
  [-]
  • fractorial 1 hour 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.
• homarp 5 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 4 hours ago
    Could you provide a practical example?
    [-]
    • rawland 4 hours 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 3 hours ago
  [dead]
  [-]
  • eisbaw 3 hours ago
    git clone is slightly faster
    [-]
    • gumby 3 hours ago
      And doesn’t use as many tokens, at least for now.
      [-]
      • black_knight 1 hour 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.