Are there any formal proofs of maths theorems?

Are there any formal proofs of maths theorems? Aren't mathematicians systematically checking all theorems by doing the formal proofs? I never came across any so far!
EB

 

Log in or Sign up to hide all adverts.

Of course there are.
What are you Googling that you haven't found any?

 

Log in or Sign up to hide all adverts.

Things like that: "⊢ ¬Countable(UNIV:Real → Bool)"...
Do you have better than that?
I'm talking of self-sufficient proofs you can understand on reading them, like in my old maths textbook. Here, apparently, you'd need to refer to some unspecified technical manual I'm not going to have anyway.
EB

 

Log in or Sign up to hide all adverts.

Euclid (born circa 325 BC) produced some excellent proofs relating to geometry & I am not sure what else.

His proofs are easily understood.

While known prior to Pythagoras (circa 500 BC), he was probably the first to prove the theorem relating to right triangles.

 

What's wrong with the proof for Pythagorus' Theorem of Right Triangles?

 

Never mind.
EB

 

What a peculiar fellow...

 

You are talking about the language, not the proof, which might be very simple.
How about: ". . . - - - . . . ", where's the proof in that?

But are all equations not self-referential proofs?

 

No, I'm talking about proofs. A proof is a particular sequence of the symbols used in one language. All proofs are couched in a particular language so language is a necessary fixture which makes reference manuals necessary too. The difficulty in the formal proofs I found on the Internet is that they are couched in a language I don't the reference manual for. And I would also expect mathematicians to produce formal proofs outside the use of theorem solvers. That's what I'm looking for.
So, again, most of your post is just irrelevant to the OP.
EB

 

What seems particular to me is that you should reply without addressing the OP: Are there any formal proofs of maths theorems? Aren't mathematicians systematically checking all theorems by doing the formal proofs? I never came across any so far!
EB

 

I certainly did.
You asked if there are formal proofs. I told you there are.
You asked if mathemetians write proofs. They do. I gave an example.

Your questions are answered.

You are not communicating very well. Instead of requiring us to pull teeth to get clarification out of you, why don't you just proactively offer the clarification?

 

So we are talking about language. I'm happy with that little bit which is relevant....

Please Register or Log in to view the hidden image!

 

A mathematical theorem is a formal proof. Or it has one or more proofs.
Duh.

If you don't understand the notation, that's ok, someone else does, somewhere.

 

No, I'm talking about proofs.
EB

 

I responded to your first reply, provided one example of proofs I had found on the Internet and explained why I can't use them.
In your second reply, you talk not of a "formal proof" but of a "proof", which was a derail, perhaps because you didn't get the OP to begin with.
Specialists apparently make the distinction between formal and informal proofs. Most of the proofs produced by mathematicians are informal proofs.
There are formal proofs produced more or less automatically by machines. To be able to read them, you'd need to have the technical manual for the language and train for weeks, and even then the presentation of the proofs would still be cumbersome. It also appears that people who are specialist of automatic theorem solvers aren't capable or willing to explain what they do very well. So, I'm looking for formal proofs produced by mathematicians, which should be more readable.
EB

 

See my response above to Dave.
EB

 

A pity it took 15 posts for the OP to explain what he was asking for...

 

???
Here's my second post:

And again, it was you who ignored what the OP was talking about, namely "formal proofs". And as to explaining, all you needed to do was go to the Wiki article on "formal proof":

If you ignore the OP (and my second post) or are to lazy to read or pay attention, why should I feel like you're going to read and pay attention to my other posts?
EB

 

Most folks in the USA take a course in 10th grade which presents many of Euclid's Geometric proofs as well as proofs of the Pythagorean theorem relating to right triangles.

As far as I know, those are considered valid proofs.

BTW: For a long time (perhaps centuries) folks tried to prove Euclid's postulate relating to parallel lines, which many thought should be a theorem instead of a postulate.

Riemann or perhaps Gauss finally established that it was an unprovable axiom of plane geometry. Alternatives to it led to spherical & hyperbolic geometry rather than plane geometry.

 

They are all over the internet. I'm not sure what you could be looking for that you can't find.
Pick a theorem or consequence you are interested in, copy paste its name and the word "proof" into the search bar of a browser, select your preferred exposition.

Example: "Hölder's Inequality" + proof, in search bar of Google Advanced Search, yields pages of links Inequality&as_oq=&as_eq=&as_nlo=&as_nhi=&lr=&cr=&as_qdr=all&as_sitesearch=&as_occt=any&safe=images&as_filetype=&as_rights=
leading off with the Wikipedia entry (a couple of proofs and links) https://en.wikipedia.org/wiki/Hölder's_inequality: https://www.google.com/search?as_q=proof &as_epq=Hölder's
and including things like this: https://www.math.upenn.edu/~brweber/Courses/2011/Math361/Notes/YMandH.pdf

Not my favorite proof, btw, (and there's at least one careless error, probably a typo, easily caught in intro Cauchy layout, so I don't recommend it), but I didn't go looking around.