Re: [mizar] Euclid's Elements

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Few years ago Witold Marciszewski proposed me to formalize Elementa, and even
borrowed  me his copy in Polish. I ran quite fast into troubles. I had expected
usual problems with the continuity, but something else arisen.:
There is no concept of (straight) line in Elementa, only arbitrary long segment.
So, while doing a construction we take the segment e.g. going through 2 points,
it must be long enough, and how long one learns only later when a point of the
intersection with something else is needed.
I was quite surprised.

Andrzej

Piotr Rudnicki wrote:

> Hi:
>
> Has anybody done beginnings of Euclid's Elements in Mizar, Mizar-MSE, or
> any other proof assistant?
>
> --
> Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
> email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr