|
|
|
|
|
|
by jojomodding
5 hours ago
|
|
|
No, Lean allows non-constructive proofs so a proof could be like "if the Riemann hypothesis is true the counterexample is 42 otherwise it is the first nontrivial zero" or something like this, and then you don't get a fully closed counterexample. |
|
|