A terminal AI coding agent that formalizes math problems into Lean 4 theorems and proves them.
Read in full here:
1 Like
Ok, this looks dope. The catch is that it’s tied to Lean 4.
Bookmarking it for when I do actually get started with Lean 4.