5 ms·
To be clear, this is not the kind of thing where a Lean formalization provides any value at all. It's like formalizing the answer to a high school algebra probl
by bugufu8f83 2mo ago
To be clear, this is not the kind of thing where a Lean formalization provides any value at all. It's like formalizing the answer to a high school algebra problem. The counterexample is obviously correct.
- sciyoshi 2mo agoIndeed. I was mainly responding to the comment about waiting for "independent seasoned mathematicians to verify", whereas in this case it is easy enough to convince oneself of the counterexample's correctness.