Lean verification record
Checked Artifact: Ptolemy’s Theorem (mathlib)
Proof Atlas collected build, no-sorry, axiom, and clean-source evidence directly from the pinned upstream declaration.
Verification result
The recorded Lean checks passed
- Build replaypassed with retained transcript
- Unfinished stepsNone found
- Source identityPinned commit and file recorded
- Dependency profileAxiom closure recorded
Reproducibility details
What the checker recorded
- Declaration checked
EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical- Module
Mathlib.Geometry.Euclidean.Sphere.Ptolemy- Source file checked
Mathlib/Geometry/Euclidean/Sphere/Ptolemy.lean- Package commit
5e932f97dd25535344f80f9dd8da3aab83df0fe6- Build transcript
- passed · retained with this record
- Unfinished proof steps
- None found by the recorded no-sorry scan
- Axiom closure
- Classical.choice, Quot.sound, propext
- Collection provenance
- Clean source state recorded
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Evidence boundary
Exact formal statement only
This page indexes Mathlib's cospherical four-point distance identity in a real inner-product affine metric space. It assumes an auxiliary point p with ∠ a p c = π and ∠ b p d = π, which encodes the crossing order through p, and concludes dist a b * dist c d + dist b c * dist d a = dist a c * dist b d. It does not separately assume an ordered planar polygon, convexity, pairwise-distinct vertices, or nondegeneracy, and it does not assert the equality for an arbitrary ordering of four cospherical points.
This checker record does not establish novelty, transfer a historical acceptance decision, or authorize publication.