4 ms·
MathCode, Mathematical Coding Agent
- homarp 2mo agoA 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 2mo agoCould you provide a practical example?
- rawland 2mo agoThere 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 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).
- dominotw 2mo agoso ' a problem' here is just preexisting math theorems ?
- muds 2mo agoInteresting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean https://github.com/T3S1AMAX/autolean)?
- 129387 2mo ago[dead]
- eisbaw 2mo agogit clone is slightly faster
- gumby 2mo agoAnd doesn’t use as many tokens, at least for now.
- black_knight 2mo agoI 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.
- owlbite 2mo agoInteresting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
- a2ff6eeb0 2mo agoIt's AI generated, so licensing terms are unenforceable.
- a2ff6eeb0 2mo agoOr, more accurately: it's not possible to apply copyright to generated code; if you don't release it, it's a trade secret, but if you do, people can use it how they please.
- whattheheckheck 2mo agoIs this effectivly mit or no license?
- a2ff6eeb0 2mo agoEffectively public domain.
- jrflo 2mo agoWhat commercial setting do you want to use a Lean theorem-proving agent in?
- ljwoods2 2mo agoMathematics, Inc [1], I assume [1] http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF
- eisbaw 2mo agothe tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
- bayesnet 2mo agoI’ve written a lot of Lean for economic modeling (so take this with the caveat that it’s not frontier-level mathematics research) but I think this problem is overstated. If you follow good engineering standards—keep primitives composable and design abstraction well—it’s not so hard to understand enough Lean to ensure the formalized statement is correct. In part this is possible because mathlib is very well-designed and has a very good API (in no small part because they’re willing to make breaking changes all the time), so building on top of it makes life much easier.
- wanderlust123 2mo agoWhat kind of economic modelling uses Lean?
- barrenko 2mo ago+1
- dominotw 2mo agodo you have examples . i am fascinated by this
- philipfweiss 2mo agoMaybe consider an integration with theoremdb.org?
- fractorial 2mo agoTo 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.
- andxor 2mo ago> hooking up slop to slop is just unlikely to produce anything valuable Do you have a formal proof of that?
- skew-aberration 2mo agoPremises: Garbage in implies garbage out (first principle of computer science) The input is possibly, but not necessarily garbage (definition of slop) By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.
- cgio 2mo agoI am not sure of the premise. You can have a filter which takes garbage in and outputs the clean data from the garbage, a denoiser. Also your definition of slop is not specific to slop. Any input can be garbage, including this human sourced and thought comment.
- skew-aberration 2mo agoNevertheless, the proof is valid and easy to certify
- tizerluo 2mo ago[flagged]
- dominotw 2mo agosounds like an awesome project. wish these project always start with an example. i dont care about quickstart or featurelist if i dont know what this is.
- pullshark91 2mo agoMy, what a creative name
- CodeWithLeo 2mo ago[dead]
- c0rruptbytes 2mo agolooks nice...time to turn it into a pi extension
- shidesheng 2mo ago[flagged]
- agentwyz 2mo ago[dead]