a true proof assistant wow moment

Stream: Analysis I

[Rado Kirov]

After wrestling with the type checker for weeks now, I got a nice "proof assistant" wow moment, I wanted to share. Part a) of the exercise asked me to prove something given some hypotheses, and when I got to part b) which asked which of the hypotheses are needed - I could immediately see the Lean linter showing me two hypotheses were not used in the proof. Kinda magical, won't be nearly as easy to look through a pen and paper the proof and see what was used and what not, especially with A B C D looking a bit similar.

Screenshot 2025-07-16 at 11.35.54 PM.png

[Ruben Van de Velde]

Ah, but is the questions which hypotheses were not needed or not used? :)

[Rado Kirov]

My thinking is - not used for my specific proof means they are not needed in general, but for the two used, it is not clear that there isn't a better proof that doesn't use them. But I showed a counter example where the goal is not true, when A is empty. The only thing I don't know how to do yet in Lean is reason use symmetry and commutativity of the product that same applies to B.

[Edward van de Meent]

there is the wlog tactic, but it's been alledged to be a bit buggy, and is in general a bit rough around the edges.

[Kyle Miller]

Rado Kirov said:

I got a nice "proof assistant" wow moment

I think my first big one was when I ported a proof I'd written from Lean 3 to Lean 4, the unused variable linter pointed out that in my lengthy proof by cases, I'd never actually used the fact I was in any particular case, and I could delete half the proof! (This was with a by_cases tactic.)

[Terence Tao]

My "wow" moment was when we had just completed a three-week project to formalize a newly proven conjecture (the polynomial Freiman-Ruzsa conjecture, PFR) with a certain constant C=12. But then someone managed to modify the (informal) proof to improve the constant C=11. We could implement this new proof in roughly a day, basically by replacing C with 12 at one line of the proof, seeing where the elaborator now complained, and filling in the steps with fixes that were either coming from the new informal proof, or were obvious modifications. We could refactor thousands of lines of code with remarkable speed because we could safely zero in on the few lines of code that actually needed modification.