MathCode, Mathematical Coding Agent

(math-ai-org.github.io)

45 points by homarp4 hours ago

6 comments

muds3 hours ago
Interesting work. Is this a wrapper around the AUTOLEAN project (<a href="https://github.com/T3S1AMAX/autolean" rel="nofollow">https://github.com/T3S1AMAX/autolean</a>)?
owlbite2 hours ago
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
- jrflo1 hour ago
  What commercial setting do you want to use a Lean theorem-proving agent in?
- a2ff6eeb01 hour ago
  It's AI generated, so licensing terms are unenforceable.
philipfweiss1 hour ago
Maybe consider an integration with theoremdb.org?
- fractorial58 minutes ago
  To be clear, I am deep into auto-research, but hooking up slop to slop is just unlikely to produce anything valuable.<p>Value is in how maths is communicated: The process, frustrations, triumphs, etc.<p>We have to able to take generated formalizations from “it compiles” to “it is correct” before crystallizing them.
eisbaw2 hours ago
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
homarp4 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.
- seunosewa3 hours ago
  Could you provide a practical example?
  - rawland3 hours ago
    There is one in the quickstart:<p><pre><code> mathcode -p "prove that the square of an even number is even" </code></pre> <a href="https://math-ai-org.github.io/mathcode/#quickstart" rel="nofollow">https://math-ai-org.github.io/mathcode/#quickstart</a> - if you look very closely, the screenshot at the top actually shows the output (and the solution).
1293873 hours ago
[dead]
- eisbaw2 hours ago
  git clone is slightly faster
  - gumby2 hours ago
    And doesn’t use as many tokens, at least for now.
    - black_knight39 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.<p>Lets me ignore the LICENSE.md file, and use how I want.