In the future I hope there is an option for more instructive feedback from Lean's compiler in the spirit of how the Rust compiler offers suggestions to correct code.
This is how Acorn works, so that when proving fails but you are "close", you get suggestions in VS Code like:
Try this:
reduce(r.num, r.denom) = reduce(a, b)
cross_equals(a, b, r.num, r.denom)
r.denom * a = r.num * b
It doesn't use LLMs, though, there's a small local model running inside the VS Code extension. One day hopefully that small local model can be superhumanly strong. For more info: https://acornprover.org/docs/tutorial/proving-a-theorem/
This looks nice. I wasn't aware of Acorn--how much adoption does it have in the mathematics community (or formal methods / robotics / other communities)? I feel like most are rallying around Lean.
It's a much newer project than Lean, and Lean has more adoption. But the vast majority of mathematicians aren't using formal methods at all, so perhaps the space is still oepn.
This is how Acorn works, so that when proving fails but you are "close", you get suggestions in VS Code like:
It doesn't use LLMs, though, there's a small local model running inside the VS Code extension. One day hopefully that small local model can be superhumanly strong. For more info: https://acornprover.org/docs/tutorial/proving-a-theorem/