MathCode, Mathematical Coding Agent

homarp

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.

muds

Interesting work. Is this a wrapper around the AUTOLEAN project ( https://github.com/T3S1AMAX/autolean )?

owlbite

Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.

eisbaw

the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.

philipfweiss

Maybe consider an integration with theoremdb.org?

dominotw

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.

pullshark91

My, what a creative name