Re: [mizar] Euclid's Elements

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Piotr,

>Has anybody done beginnings of Euclid's Elements in Mizar,
>Mizar-MSE, or any other proof assistant?

I always want to do this, but I didn't really start yet.

An interesting question is how to model "equality" (which in
Euclid means "equal length/area/angle").  You want "sums of
figures" to be equal when the figures are equal, so the
question arises whether the "size" of a figure should be
oriented or not.  I.e., if you "add" the triangle ABC to the
triangle ACB, does it become zero?  That probably is
mathematically nicest, but it doesn't sound much like
Euclid.  Or should this addition be illegal? (because the
triangles overlap?)

Freek