Are there any formal proofs of maths theorems?

Discussion in 'Physics & Math' started by Speakpigeon, Nov 12, 2018.

  1. Speakpigeon Valued Senior Member

    Messages:
    1,123
    Irrelevant.
    EB
     
  2. Google AdSense Guest Advertisement



    to hide all adverts.
  3. Speakpigeon Valued Senior Member

    Messages:
    1,123
    All these are what's called "informal proofs". There's just one example of a formal proof but it's done using a machine (theorem solver ACL2(r)).
    There you are, formal proofs don't contain "careless errors", that's the point of them.
    They are also I guess probably extremely tedious to produce without using a machine and probably mathematicians don't think it's worth their time considering that writing their usual informal proofs that are more legible to fellow mathematicians will be a better use of their time.
    Anyway, thanks for the links.
    EB
     
  4. Google AdSense Guest Advertisement



    to hide all adverts.
  5. iceaura Valued Senior Member

    Messages:
    30,994
    Ok. They do start in the middle.
    But why you would expect a mathematician's typing of a complete derivation from axiom to be any more "legible" than a machine's typing of the same, I don't know.
    They do when they are typed unto internet pages, or published in manuscript etc.
    There's a coder's insight involved - at some point, debugging introduces more errors than it fixes.
     
  6. Google AdSense Guest Advertisement



    to hide all adverts.
  7. Beer w/Straw Transcendental Ignorance! Valued Senior Member

    Messages:
    6,549
    You looking for something like this (proof by contradiction):

    Please Register or Log in to view the hidden image!

     
  8. Dinosaur Rational Skeptic Valued Senior Member

    Messages:
    4,885
    From SpeakPigeon Post 15
    Do you have a citation for the above?

    You surely are not referring to any of Euclid’s geometric proofs, which are accepted as formal proofs & easy to understand by 10th graders with average intelligence & a willingness to pay attention.​

    BTW: Where did you find the following?
     
  9. Speakpigeon Valued Senior Member

    Messages:
    1,123
    No. That's an "informal" proof and those are obviously very easy to find.
    I'm talking about formal proofs. Typically, you wouldn't have all these plain English explanations. The bit of explanation you could have, if any, would be minimal, predefined and repetitive.
    It would be more something like this, but more readable (this bit would be machine-generated):
    Prove (1 \in f @* (G :&: H))
    Lemma natCauchy m p : 2 * (m * p)<= m ^ 2 + p ^ 2 ?= iff (m == p)
    Definition (X : Prop) : Prop :=
    forall u : bool, (X -> u) -> u.​
    EB
     
  10. Speakpigeon Valued Senior Member

    Messages:
    1,123
    Rational people want to be read by other rational people, understood, and valued for their hard work.
    EB
     
  11. Beer w/Straw Transcendental Ignorance! Valued Senior Member

    Messages:
    6,549
    No, you're just wrong, I could have easily of proved that the square root of two was irrational.

    :EDIT:

    A "Mathematical Proof" and "Formal Proof" might not be the same thing.

    :EDIT:

    Well, I guess when you get down to it, unless I can prove/disprove infinity, I'm kinda' stuck.
     
    Last edited: Nov 16, 2018
  12. phyti Registered Senior Member

    Messages:
    732
    Mathematics is a language. Every expression can be transformed to most native languages.
    Comprehension is the key to understanding. Any language requires decoding symbols.
     
  13. Dinosaur Rational Skeptic Valued Senior Member

    Messages:
    4,885
    SpeakPigeon: If you do not consider Beer/Straw's proof to be valid & formal enough, provide your formal version of a proof that SquareRoot(2) is irrational instead of posting the following
    Which has nothing to do with Beer/wStraw's proof which looks very valid & succinct to me. I am sure that it could be found in a standard text for high school students & would be accepted as valid by pedantic mathematicians..

    What does the above prove? The conclusion seems to be unrelated to Beer's proof.

    Where did you find that proof?

    BTW: As far as I know machines (Id Est: computers, I suppose) do not compare with humans for generating proofs. They are pretty much number crunchers.
     
  14. uhClem Registered Member

    Messages:
    25
    iceaura likes this.
  15. iceaura Valued Senior Member

    Messages:
    30,994
    Of course. But mistakes will be made - especially in something like a formal proof from very basic axioms. Typos.
    Sweet. Props.
     
  16. Speakpigeon Valued Senior Member

    Messages:
    1,123
    Thanks, that's exactly it!
    Proofs come with a pdf version in a style which is human-reader-friendly, at least the one for "The Transcendence of π" that I looked at.
    Thanks again. Christmas was early this year.
    EB
     
  17. Speakpigeon Valued Senior Member

    Messages:
    1,123
    That's not the point. Machine-made formal proofs usually need a human input.

    The point is that the probability of typos is almost zero in proofs made by machines. Logical errors are also less probable. I guess, the only possibility would be a systematic error, something like an error in the basic principles of the logic used by the machine, and I assume that would be easily detectable by the specialists.

    Also, it seems mathematicians are not too motivated to write them themselves.
    EB
     
  18. Speakpigeon Valued Senior Member

    Messages:
    1,123
    Irrelevant.
    EB
     
  19. Speakpigeon Valued Senior Member

    Messages:
    1,123
    ???
    Wrong about what?
    EB
     

Share This Page