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 33 days ago [-]
Could you provide a practical example?
rawland 33 days ago [-]
There is one in the quickstart:
mathcode -p "prove that the square of an even number is even"
so ' a problem' here is just preexisting math theorems ?
eisbaw 33 days ago [-]
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
bayesnet 33 days ago [-]
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.
wanderlust123 33 days ago [-]
What kind of economic modelling uses Lean?
barrenko 33 days ago [-]
+1
dominotw 33 days ago [-]
do you have examples . i am fascinated by this
owlbite 33 days ago [-]
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
jrflo 33 days ago [-]
What commercial setting do you want to use a Lean theorem-proving agent in?
It's AI generated, so licensing terms are unenforceable.
a2ff6eeb0 33 days ago [-]
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.
whattheheckheck 33 days ago [-]
Is this effectivly mit or no license?
a2ff6eeb0 32 days ago [-]
Effectively public domain.
dominotw 33 days ago [-]
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.
philipfweiss 33 days ago [-]
Maybe consider an integration with theoremdb.org?
fractorial 33 days 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.
andxor 33 days ago [-]
> hooking up slop to slop is just unlikely to produce anything valuable
Do you have a formal proof of that?
skew-aberration 33 days ago [-]
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.
cgio 33 days ago [-]
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.
skew-aberration 33 days ago [-]
Nevertheless, the proof is valid and easy to certify
c0rruptbytes 33 days ago [-]
looks nice...time to turn it into a pi extension
tizerluo 33 days ago [-]
[flagged]
shidesheng 32 days ago [-]
[flagged]
CodeWithLeo 33 days ago [-]
[dead]
129387 33 days ago [-]
[dead]
eisbaw 33 days ago [-]
git clone is slightly faster
gumby 33 days ago [-]
And doesn’t use as many tokens, at least for now.
black_knight 33 days 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.
agentwyz 32 days ago [-]
[dead]
pullshark91 33 days ago [-]
My, what a creative name
Rendered at 20:14:51 GMT+0000 (Coordinated Universal Time) with Vercel.
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.
[1] http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF
wish these project always start with an example. i dont care about quickstart or featurelist if i dont know what this is.
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.
Do you have a formal proof of that?
By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.
Lets me ignore the LICENSE.md file, and use how I want.