Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Foundation_of_geometry


view this post on Zulip Email Gateway (Dec 13 2021 at 03:47):

From: Gerwin Klein <kleing@unsw.edu.au>
Foundation of geometry in planes, and some complements: Excluding the parallel axioms
by Fumiya Iwama

"Foundations of Geometry" is a mathematical book written by Hilbert in 1899.
This entry is a complete formalization of ``Incidence" (excluding cubic axioms),
"Order" and "Congruence" (excluding point sequences) of the axioms constructed in this book.
In addition, the theorem of the problem about the part that is treated implicitly
and is not clearly stated in it is being carried out in parallel.

https://www.isa-afp.org/entries/Foundation_of_geometry.html

Enjoy!
Gerwin


Last updated: Jul 15 2022 at 23:21 UTC