[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Paradox

On Thu, Jan 09, 2003 at 11:15:36AM +0100, Freek Wiedijk wrote:

> Has any one formalized the Banach-Tarski decomposition (the
> "paradox" that you can make multiple spheres from one sphere)
> already?  Would it be difficult?  (I think in Mizar it would
> be much easier to formalize than in the other systems, and it
> would make a nice showcase.)

Speaking of showcases.  Matthias Baaz, TU Vienna, is visiting here in
Edmonton and as an exercise we have formalized Fuerstenberg's proof on
infinity of primes (this involves a topology on INT).  Now, Matthias
suggested that we formalize Witt's proof of Weddernburn's theorem that
every finite division ring is commutative.  Just by the looks at the
proof it seems a bit hairy but I am ready to try.  Has anyone done
something like this?

Best,

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr