This is an unofficial reimagining of the Archive of Formal Proofs
The independence of Tarski's Euclidean axiomby T. J. M. Makarios