Learn · Geometry
Axeyum for geometers
Axeyum has a substantial coordinate-geometry library over its constructed real numbers, with both kernel proofs and computer algebra certificates.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation After reading this guide, you should be able to
Learning objectives
- Identify the parts of Axeyum that are relevant to geometry.
- Distinguish implemented results from the current research frontier.
- Open a lesson or artifact that provides the underlying definitions and evidence.
Current state
What geometry has been checked over the constructed real plane?
The checked corpus includes Stewart's theorem, Ptolemy's identity and inequality, Ceva's theorem, Menelaus' theorem, the Euler line, the nine-point center, power of a point, and the radical axis. Points and lines use explicit coordinates over constructed reals.
This representation turns many geometric claims into exact algebra while retaining named geometric definitions and theorem dependencies. Some computer algebra certificates are reconstructed in the kernel; others remain operation-specific CAS evidence and are labeled that way.
Why it matters
What the current work makes possible
- A broad collection of classical Euclidean results shares one constructed coordinate plane.
- Degenerate cases and side conditions are explicit in formal statements.
- The geometry corpus tests cooperation between symbolic computation and proof checking.
Results to inspect
Open the evidence
What comes next
Extend the present base
The next geometric layer includes an abstract incidence development, transformations, and reusable affine and projective structures.
Differential and algebraic geometry will require the topology and algebra frontiers: general spaces, manifolds, polynomial rings, ideals, and quotient constructions.
Where to begin