alt.hn

8/16/2026 at 6:17:10 PM

MathCode, Mathematical Coding Agent

 https://math-ai-org.github.io/mathcode/

by homarp

8/16/2026 at 6:17:10 PM

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.

by homarp

8/16/2026 at 7:20:10 PM

Could you provide a practical example?

by seunosewa

8/16/2026 at 7:26:20 PM

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

by rawland

8/17/2026 at 2:30:39 AM

so ' a problem' here is just preexisting math theorems ?

by dominotw

8/16/2026 at 8:19:49 PM

the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.

by eisbaw

8/16/2026 at 11:55:01 PM

I’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.

by bayesnet

8/17/2026 at 1:14:35 AM

What kind of economic modelling uses Lean?

by wanderlust123

8/17/2026 at 7:03:44 AM

+1

by barrenko

8/17/2026 at 2:31:43 AM

do you have examples . i am fascinated by this

by dominotw

8/16/2026 at 8:00:09 PM

Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.

by owlbite

8/16/2026 at 9:31:39 PM

It's AI generated, so licensing terms are unenforceable.

by a2ff6eeb0

8/16/2026 at 11:43:42 PM

Or, 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.

by a2ff6eeb0

8/17/2026 at 5:17:09 AM

Is this effectivly mit or no license?

by whattheheckheck

8/17/2026 at 11:47:12 AM

Effectively public domain.

by a2ff6eeb0

8/17/2026 at 2:29:42 AM

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

by dominotw

8/16/2026 at 9:32:39 PM

Maybe consider an integration with theoremdb.org?

by philipfweiss

8/16/2026 at 9:58:40 PM

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.

by fractorial

8/17/2026 at 12:02:45 AM

> hooking up slop to slop is just unlikely to produce anything valuable

Do you have a formal proof of that?

by andxor

8/17/2026 at 1:41:13 AM

Premises: 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.

by skew-aberration

8/17/2026 at 2:39:47 AM

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

by cgio

8/17/2026 at 3:35:19 AM

Nevertheless, the proof is valid and easy to certify

by skew-aberration

8/17/2026 at 7:19:50 AM

looks nice...time to turn it into a pi extension

by c0rruptbytes

8/17/2026 at 9:30:49 AM

[flagged]

by shidesheng

8/17/2026 at 1:33:31 AM

[flagged]

by tizerluo

8/17/2026 at 5:26:15 AM

[dead]

by CodeWithLeo

8/17/2026 at 10:54:50 AM

[dead]

by agentwyz

8/16/2026 at 7:43:46 PM

[dead]

by 129387

8/16/2026 at 8:17:14 PM

git clone is slightly faster

by eisbaw

8/16/2026 at 8:20:10 PM

And doesn’t use as many tokens, at least for now.

by gumby

8/16/2026 at 10:17:27 PM

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.

by black_knight

8/17/2026 at 4:44:55 AM

My, what a creative name

by pullshark91