MathCode, Mathematical Coding Agent

▲ MathCode, Mathematical Coding Agent(math-ai-org.github.io)

12 points by homarp an hour ago | 3 comments

▲ homarp an hour ago | parent [-]

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 16 minutes ago | parent [-]

Could you provide a practical example?

	▲	rawland 10 minutes ago \| parent [-]
		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).