This is great. Many people online who "verify their software" seem to just tell an LLM "verify dis" and have no idea what comes out. The model could be proving 1+1=2 for all they know.
These guys actually show some Lean theorems they proved. Also interesting approach to compile the existing interpreter into the de-facto spec.
These guys actually show some Lean theorems they proved. Also interesting approach to compile the existing interpreter into the de-facto spec.