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
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.
You looking for something like this (proof by contradiction): Please Register or Log in to view the hidden image!
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?
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
Rational people want to be read by other rational people, understood, and valued for their hard work. EB
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.
Mathematics is a language. Every expression can be transformed to most native languages. Comprehension is the key to understanding. Any language requires decoding symbols.
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.
Of course. But mistakes will be made - especially in something like a formal proof from very basic axioms. Typos. Sweet. Props.
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
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