Systems

Deep architectural and forensic dossiers on all 11 formal, visual, and symbolic geometry systems surveyed in GEOMETOR Codes—each audited directly from source code on disk down to exact file paths, line numbers, verification kernels, opus coverage, and live bugs.

Dossier	Paradigm	Verification Substrate	Headline Forensic Catch
LeanEuclid & System E	Diagrammatic System E + SMT	Lean 4 + Z3/CVC5	SMT_VERIF trust axiom + 6 missed Euclid lemmas in Prop47
GeoCoq	Point-Only Synthetic Axiomatics	Coq Kernel + ColR/CongR	34 parallel postulates & neutral midpoint; omits X(5), inversion, \(\phi\)
Lean 4 Mathlib	Dependent Affine Torsors	Lean 4 Kernel (noncomputable)	\(n\)-dim Monge/Feuerbach/La Hire; omits Euclid I.1, crossRatio, Pappus
AlphaGeometry & Newclid	Neuro-Symbolic Clause DD + AR	Python/C++ Gaussian AR + LM	rconst log-ratio bug (ar.py:425), ; drops, and Pappus DD+AR wall
JGEX & Area Method	Coordinate-Free Invariant Elimination	Java (GDD, Full, Area, Wu, GB)	0-step Pythagoras/Orthocenter; Area.java tab disabled in GUI!
PGA & CGA (kingdon / galgebra)	Covariant Clifford Multivector Calculi	kingdon SymPy CSE compiler	C >> P inversion in kingdon vs. .dual() crash & >> trap in galgebra
CindyJS (CP^2 & PSLQ)	Complex Projective & Riemann Tracing	Schwartz–Zippel + PSLQ.js	Semicircle homotopy continuation (Tracing.js) + ConicBy5 Plücker pencils
SymPy Geometry (1.14.0)	Affine Cartesian Symbolic CAS	simplify() + generic solve()	Live double bug in Triangle.excenters + Point.affine_rank float bug
Oliver Byrne (1847 / Rougeux)	Pointer-Free Visual Pseudocode	Chromatic value-tokens + SVG hover	Eliminates vertex pointers across Books I–VI (including \(\phi\) in II.11/VI.30)
GEOMETOR (geometor.model)	Exact Constructive Symbolic DAG	SymPy ANP + Rational Trig	100% float-free radical towers + ETC X(1)–X(53144) + 11 roadmap upgrades