[FOM] Formalization Thesis
Freek Wiedijk
freek at cs.ru.nl
Mon Jan 14 07:52:56 EST 2008
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
More information about the FOM
mailing list