[thaumasiotes]

> For everyone else in this thread, exhaustion means trying out all values and proving it works.

My instinct was that you can still call it proof by exhaustion if you divide the values into classes and do the proof for each class.

> Similar way you'd prove four color theorem.

And this seems to support that idea? It's the same thing as proof by cases.

So the proof that n^2 + n is even for all integers is exhaustive: you do one proof for even integers, and another one for odd ones. But we wouldn't generally use the term "exhaustion" there because the vibes are wrong.

[vjerancrnjak]

Thing with "classes" is that you need to identify them before proving and you need to prove the implication to general case.

Lean is not powerful enough to do this, to somehow conclude that there's a finite set of cases on which you can run brute-force checks and prove a general case.