This repository is part of an AI-assisted research workflow that formalizes mathematics in Lean so results are independently checkable. For this project, the possible biomedical path is indirect. Distance geometry is used in protein-structure determination, and structural analysis informs gene-therapy vector design. This repository does not claim a gene-therapy result. It tests whether our AI-assisted workflow can turn mathematics into correct, reviewable, reusable proofs.
This repository contains a Lean 4 formalization of several results in finite Euclidean distance geometry. It connects squared-distance matrices with Gram matrices anchored at a basepoint, proves a two-candidate trilateration bound, and treats the segment and triangle cases of the Cayley--Menger determinant.
DistanceGeometry.schoenberg: forn ≥ 1, a symmetric hollown × nmatrix embeds as squared distances ink-dimensional Euclidean space if and only if its basepoint-centered Gram matrix is positive semidefinite and has rank at mostk.DistanceGeometry.encard_setOf_forall_dist_eq_le_two: if a family of centers spans a hyperplane, the points with prescribed distances to those centers form a set of cardinality at most two.DistanceGeometry.trilateration_le_two: three affinely independent centers in three-dimensional Euclidean space determine at most two points with any prescribed triple of distances.DistanceGeometry.cayleyMenger_det_heron: for three points in the Euclidean plane, the Cayley--Menger determinant equals-16times the squared area of the triangle.
The last declaration states the triangle-area identity underlying Heron's formula. After expansion and factorization in the three side lengths, the identity is equivalent to Heron's formula. The repository does not state the factorized formula as a separate theorem.
The supporting API includes a rank-controlled factorization of positive-semidefinite matrices and algebraic Cayley--Menger formulas for segments and triangles.
The development concerns finite configurations over the real numbers. The Cayley--Menger part covers dimensions one and two. The DMDGP connection consists of the two-candidate sphere-intersection theorem; algorithmic reconstruction and the general dimension formula are outside the current scope.
IsPreDistMatrix is the project's symmetric-and-hollow structural predicate. It
omits entrywise nonnegativity; some distance-geometry references include that
condition in the term "pre-distance matrix".
The mathematics is classical. This repository contributes a Lean formalization and reusable definitions and lemmas around it.
Install Lean through elan, then run:
lake exe cache get
lake buildThe repository pins its Lean and Mathlib versions.
I. J. Schoenberg, “Remarks to Maurice Fréchet's Article Sur la définition axiomatique d'une classe d'espace distanciés vectoriellement applicable sur l'espace de Hilbert” (1935). DOI 10.2307/1968654.
Project direction: Egor Lyfar. AI systems produced most of the Lean code. Lean checks the proofs with the pinned toolchain.
Apache-2.0