[FOM] Formalization Thesis

[Freek Wiedijk]

Dear Andrew,

>Since posting it has occurred to me that an even better example would  
>be the Pythagorean Theorem, "better" in the sense that I would expect  
>a better than even chance that working mathematicians would agree  
>that it is a counterexample.

For what it's worth: this theorem has been formalized in
HOL Light, Mizar, Isabelle, Coq, ProofPower and PVS; see
item 4 in the list on <http://www.cs.ru.nl/~freek/100/>.

Click on the links for the systems in the table at the top
of the page to see some statements.  For instance in HOL
Light it has been formalized as

  !A B C:real^2.
       orthogonal (A - B) (C - B)
       ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2

in Mizar as

  for p1,p2,p3 st p1<>p2 & p3<>p2 &
      (angle(p1,p2,p3)=PI/2 or angle(p1,p2,p3)=3/2*PI) holds
      (|.p1-p2.|^2+|.p3-p2.|^2=|.p1-p3.|^2);

etc.

Freek