4 ms·

I found this, unfortunately it is about category theory: "manuscripts [...] that are cited but never became widely available" https://ncatlab.org/nlab/show/lis

• constantcrying 3y ago
  Any particular theorem? This links to hard/impossible to access materials, but does any of them actually contain a theorem which proof is not accessible in some form? Further is it any relevant theorem, which has been cited many times?
  • rdlw 3y ago
    From the link I posted: John Beck's Monadicity Theorem is cited in "many sources" but a manuscript has been found and "The proof is reproduced for instance in (MacLane, p. 147-150, Riehl 2017, 5/5/)". Fred Linton cites Michael Barr for a "Universal property of the Kleisli construction" and no copy has been found. I don't know enough about the subject to say how difficult these proofs would be to recreate or whether they exist elsewhere, but these definitely seem to be specific theorems. I'd like to see a specific theorem in any field that was once proven and accepted but all existing proofs have been lost. That would be extremely tantalizing
    • constantcrying 3y ago
      I don't think this is convicing at all. None of this shows that there are generally accepted theorems without proofs. The first one isn't lost at all, the second is just a single lost citation. All of this is very far away from mathematicians building upon thr shaky grounds of mythical theorems. Also, in all my mathematical experience (going up to recent research in analysis) I never encountered something like this. In all textbooks I ever read either everything was proven or was cited to other works, which every time I checked included the proof.
      • cubefox 3y ago
        "Everything was proven" ... everything to satisfy a mathematician, not a logician. Formal proofs are generally very unwieldy, because informal proofs treat all the most obvious parts as obvious. In some cases these parts are not even trivial to prove formally. Last time I checked there was still no formal version of Cantor's diagonalization argument.
        • zozbot234 3y ago
          I don't think this is correct. Cantor's diagonal argument follows easily from Lawvere's fixed-point theorem https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theore... and both are quite easy to formalize.
          • cubefox 3y ago
            That seems to be a different proof which implies Cantor's theorem, but not a formalization of Cantor's diagonal argument itself.
            • zozbot234 3y ago
              It is a formalization of Cantor's diagonal argument - in fact, of "diagonal arguments" more generally. See http://arxiv.org/abs/math/0305282 http://arxiv.org/abs/math/0305282 for an expository treatment.
              • cubefox 3y ago
                Thanks, looks interesting.
        • scapp 3y ago
          > Last time I checked there was still no formal version of Cantor's diagonalization argument. Formalization? Like a computer checked proof? Lean: https://leanprover-community.github.io/mathlib_docs/logic/function/basic.html#function.cantor_surjective https://leanprover-community.github.io/mathlib_docs/logic/fu... Coq: https://github.com/bmsherman/finite/blob/63706fa4898aa05296c4290be1dba646b2c512d1/Iso.v#L277 https://github.com/bmsherman/finite/blob/63706fa4898aa05296c... Isabelle: https://isabelle.in.tum.de/website-Isabelle2009-2/dist/library/HOL/Isar_Examples/Cantor.html https://isabelle.in.tum.de/website-Isabelle2009-2/dist/libra...