Every proposition is a small program. It draws its own figure with a straightedge and compass, checks its own conclusion, and says what it depended on. Nothing is measured or approximated.
465propositions
7605steps checked
549dependency edges
2573unproved assumptions
The idea
A straightedge and compass can only produce certain numbers: the ones you reach from whole numbers by adding, subtracting, multiplying, dividing, and taking square roots. This project stores those numbers exactly, as square roots piled on square roots, never as decimals.
That sounds like a small choice, but it changes what the machine can say. Two lengths are either equal or they are not; there is no rounding, no tolerance to set, and no near-miss that might be mistaken for a theorem. Everything else on this site follows from that.
What it found
The book measured by algebraic depth. Every magnitude a construction produces has an exact degree over the rationals, so each book has a ceiling. I.1 already needs a square root; Books VII to IX never leave the rationals; X.115 reaches degree 32.
Hypotheses broken on purpose. Move a given until one of Euclid's stated conditions fails, then run without enforcing it, and see whether the conclusion held anyway. II.9 and II.10 turn out to be the same identity written twice.
The gaps Euclid never mentions. His rules let you draw circles, but never say that two circles meet. He uses that fact anyway, starting on page one.
The shortest possible constructions. Where the table says fewest possible, every shorter figure was ruled out in exact arithmetic. With no straightedge at all a midpoint costs six circles.
What depends on what. Two kinds of edge, and the page says which is which: I.1 carries 168 of the others, but most of that is Euclid's own cross-references.
Each proposition is run on many different figures that fit its assumptions, and every step is tested exactly against the figure that was built. That is a strong test, but it is a test of the pictures, not a proof in Euclid's own logic. It confirms the conclusions are true of the constructions; it does not confirm they follow by his rules of reasoning.
The references each step cites are recorded, but the test does not rely on them. So a step with the wrong reference attached still cannot slip a false statement past.