16
$\begingroup$

Is there a library (for any proof assistant) which provides formalized definitions of unsolved problems? To clarify, I mean some collection that correctly defines unsolved problems in the language of a proof assistant, without attempting to provide any solutions.

By unsolved problems, I mean one which haven't been solved by any human mathematician (like the Riemann hypothesis) rather than just ones which have been proven but not formalized in a proof assistant.

Improve this question
$\endgroup$
5
  • $\begingroup$ @GuyCoder I don’t think it is that open ended as the answer is likely there isn’t one. $\endgroup$
    – Jason Rute
    Commented Mar 22, 2022 at 12:16
  • $\begingroup$ This question is related: Libraries of formally stated theorems with proofs verified by humans. But if I understand correctly you want problems which haven’t been solved by any mathematician (like the Reimann hypothesis), whereas that question just wants problems which haven’t been proved formally in that system (like Fermat’s Last Theorem). $\endgroup$
    – Jason Rute
    Commented Mar 22, 2022 at 12:22
  • $\begingroup$ @GuyCoder I wouldn’t vote to close. It is a legitimate question. Maybe a bit more clarification could be added, but it isn’t unreasonable to think that someone started a formal library of open problems in mathematics. $\endgroup$
    – Jason Rute
    Commented Mar 22, 2022 at 12:45
  • $\begingroup$ I made a discussion on meta: What is wrong with the question "Formalizations of unsolved problems"? $\endgroup$
    – Jason Rute
    Commented Mar 22, 2022 at 13:02
  • $\begingroup$ Thanks Jason, your description (giving examples like the Riemann hypothesis) is exactly what I meant, so I'll edit my question to add that for clarity. $\endgroup$
    – Reubend
    Commented Mar 24, 2022 at 5:21

1 Answer 1

Reset to default
10
$\begingroup$

The closest to what you are asking for might be the Formal abstracts project whose aim is to formalize the statements (but no proofs) of results from papers.

Formalizing statements without proofs is not as trivial as one might think at first. Some challenges are:

  1. The statement of the proof might require formalization of a complicated constructions. For instance, consider a theorem about cohomology – presumably we need to define cohomology before we can state it.

  2. Without proofs and without any applications of the theorem there is no sanity check as to whether the statement is formalized correctly. There is real danger of mistakes going undetected.

  3. Not only should one formalize the statements itself, but also keep track of provenance, i.e., information of where in the non-formalized world the theorem originated.

Similar challenges will present themselves with a library of open problems.

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Commented Mar 22, 2022 at 16:59
  • $\begingroup$ 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. $\endgroup$
    – Joachim Breitner
    Commented Mar 23, 2022 at 10:43
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Mar 23, 2022 at 14:05
  • $\begingroup$ 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. $\endgroup$
    – Timothy Chow
    Commented Mar 31, 2022 at 19:03
  • $\begingroup$ 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. $\endgroup$
    – Timothy Chow
    Commented Mar 31, 2022 at 19:04

Not the answer you're looking for? Browse other questions tagged or ask your own question.