TechPulseTechPulse
Back to News
Advertisement
Advertisement

⚡ Community Insights

Discussion Sentiment

50% Positive

Analyzed from 153 words in the discussion.

Trending Topics

#lean#interesting#autolean#https#github#licensing#terms#commercial#setting#theorem

Discussion (13 Comments)Read Original on HackerNews

muds•about 3 hours ago
Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
owlbite•about 3 hours ago
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
jrflo•about 1 hour ago
What commercial setting do you want to use a Lean theorem-proving agent in?
a2ff6eeb0•about 2 hours ago
It's AI generated, so licensing terms are unenforceable.
philipfweiss•about 2 hours ago
Maybe consider an integration with theoremdb.org?
fractorial•about 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.

eisbaw•about 3 hours ago
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
homarp•about 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•about 4 hours ago
Could you provide a practical example?
rawland•about 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).