[ubj]

To me, the most exciting aspect of teaching mathematics using Lean is the immediate feedback. If a student's proof is wrong, it simply won't compile.

Previously, the only feedback students could receive would be from another human such as a TA, instructor, or other knowledgeable expert. Now they can receive rapid feedback from the Lean compiler.

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 would probably require the use of dedicated LLMs though.)

[vessenes]

I’m yes on this, almost completely.

But. I’m also thoughtful about proving things — my own math experience was decades ago, but I spent a lot of ‘slow thought’ time mulling over whatever my assignments were, trying things on paper, soaking up second hand smoke and coffee, your basic math paradise stuff.

I wonder if using Lean here could lead to some flailing / random checking / spewing. I haven’t worked with Lean much, although I did do a few rounds with coq five or ten years ago; my memory is that I mostly futzed with it and tried things.

Upshot - a solver might be great for a lot of things. But I wonder if it will cut out some of this slow thoughtful back-and-forth that leads to internalization, conceptualization, and sometimes new ideas. Any thoughts on this?

[mseri]

Jim Portegies (TU/e, Netherlands) and Jelle Wemmenhobe have done a lot of research on this, using their “waterproof” (controlled natural language compiled to coa) to test this directly in class. The results are very interesting, and indeed actively messing around is still a very important part of the learning experience, but you can see at least some benefits in also having a theorem prover to check if your proofs are correct.

What I was surprised is that the students learn some patterns of proof properly, but only if you make sure that they are explicitly exposed by the proof assistant (so the more automation the less learning also in this case).

You can find a lot of the work summarized in Jelle’s PhD thesis at https://research.tue.nl/nl/publications/waterproof-transform...

[lacker]

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/

[ubj]

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.

[lacker]

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.