1. 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!).

  2. 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.

  3. 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.

  4. 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)