6 ms·
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 att
by homarp 1mo 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 1mo agoCould you provide a practical example?
- rawland 1mo 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 1mo agoso ' a problem' here is just preexisting math theorems ?