NHacker Next
- new
- past
- show
- ask
- show
- jobs
- submit
login
Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
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.
Could you provide a practical example?
There is one in the 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).
Rendered at 19:40:57 GMT+0000 (Coordinated Universal Time) with Vercel.