-
F. Wiedijk, "Irrationality of e." Formalized Mathematics 9(1), 35-39, 2001: abs miz ps
Abstract.
We prove the irrationality of square roots of prime numbers and of the number e. In order to be able to prove the last, a proof is given that number_e = exp(1) as defined in the Mizar library, that is that lim(n->infinity,(1+1/n)^n) = sum(k=0..infinity,1/k!).
-
F. Wiedijk, "Pythagorean triples." Formalized Mathematics 9(4), 809-812, 2001: abs miz ps
Abstract.
A Pythagorean triple is a set of positive integers {a,b,c} with a^2 + b^2 = c^2. We prove that every Pythagorean triple is of the form
a = n^2 - m^2, b = 2mn, c = n^2 + m^2,
or is a multiple of such a triple. Using this characterization we show that for every n > 2 there exists a Pythagorean triple X with n in X. Also we show that even the set of simplified Pythagorean triples is infinite.
-
F. Wiedijk, "Chains on a Grating in Euclidean Space." Formalized Mathematics 11(2), 159-167, 2003: abs miz
Abstract.
Translation of pages 101, the second half of 102, and 103 of Newman's Elements of the Topology of Plane Sets of Points.
-
F. Wiedijk, "Arrow's Impossibility Theorem." Formalized Mathematics 15(4), 171-174, 2007.
Abstract.
A formalization of the first proof from Geanakoplos's Three Brief Proofs of Arrow's Impossibility Theorem.
publications
notes
mizar
talks
(last modification 2008-08-30)
|