Timeline for Formalizations of unsolved problems
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 31, 2022 at 19:04 | comment | added | Timothy Chow | By contrast, if there is no generally accepted formalization of the conjecture, and someone produces a formal proof from scratch, then we know they've proved something, but it's not clear whether what they've proved is actually the famous conjecture. | |
| Mar 31, 2022 at 19:03 | comment | added | Timothy Chow | The danger of incorrectly formalized statements is a real one. On the other hand, if the statement is formalized correctly, then there is a plus side in the case of well-known open problems for which false proofs are regularly proposed. Namely, someone who claims to have solved the problem can be challenged to provide a formal proof of the already-formalized statement. If the already-formalized statement can be formally proved, then that should remove any doubts about the correctness of the proposed proof. | |
| Mar 23, 2022 at 14:05 | comment | added | Andrej Bauer | It would, except that I would say that statements presuppose some rather than "imply" them. For example, the statement "the largest perfect number is not divisible by 13" presupposes there is a largest perfect number. | |
| Mar 23, 2022 at 10:43 | comment | added | Joachim Breitner | Would it be worth adding the point that often statements already implies that some things hold (e.g. if a statement uses “the”, or implies the existence of something, or uses definitions that have some precondition as arguments). It's an extension of your point 1, but maybe worth pointing out. | |
| Mar 22, 2022 at 16:59 | comment | added | Jason Rute | This is basically the answer I also had in mind. I think if the FA project ever gets off the ground, that open problems could possibly be fair game (of course labeled as such), but it unfortunately hasn't got going. | |
| Mar 22, 2022 at 16:52 | history | answered | Andrej Bauer | CC BY-SA 4.0 |