Geometry
The Lean Pool projects whose card's first MSC2020 code is in class 51, Geometry: 5 articles, one per card.
ClassAxiomatic projective geometry (Faure–Frölicher)#
Develops, following Faure and Frölicher's Modern Projective Geometry, the axiomatic theory of projective geometries given by a ternary collinearity relation, with subspaces and subgeometries, proves that the central projection between two lines is a bijection, and exhibits every Mathlib projectivization as a projective geometry. Groundwork from the upstream desargues repository — Desargues' theorem itself is not formalized.
Quoted from the card LeanPool/projects/desargues.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Basic.ProjectiveGeometry(class; a main declaration), declared in LeanPool/Desargues/Basic.lean, line 117: “Axiomatizes a projective geometry as a typeclass (axioms L₁–L₃, Faure–Frölicher p. 26) on a ternary collinearity relation.”Basic.centralProjection(def; a main declaration), declared in LeanPool/Desargues/Basic.lean, line 394: “Defines the central projection of a line onto another from a center point.”Basic.cen_proj_bij(theorem; a main declaration), declared in LeanPool/Desargues/Basic.lean, line 657: “The headline theorem — the central projection between two lines is a bijection.”
Project
- Authors: Abdullah Uyu.
- Source: Modern Projective Geometry by Claude-Alain Faure, Alfred Frölicher, doi:10.1007/978-94-015-9590-2.
- Project repository: oneofvalts/desargues.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 51A05, 51A30.
- In Lean Pool: LeanPool/Desargues, from the card LeanPool/projects/desargues.yaml.
Sources
TheoremThe Convex-Octagon Case of Erdős Problem 97#
Proves that among eight labelled points in the Euclidean plane in convex position, at least one point has no four other points at a common distance. The development reduces a geometric counterexample to a finite incidence model, classifies normalized row patterns up to symmetry, proves geometric and algebraic obstructions, and excludes seven canonical first-row masks with a kernel-audited exhaustive search over the remaining legal row masks and checked geometric obstruction witnesses. This is the modern four-equidistant formulation; Erdős's 1946 paper posed the stronger three-equidistant version. This is the convex-octagon case only; the general Erdős Problem 97 remains open.
Quoted from the card LeanPool/projects/erdos-97-convex-octagon.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Erdos97Octagon.erdos97_convex_octagon(theorem; a main declaration), declared in LeanPool/Erdos97ConvexOctagon/Classification.lean, line 39: “Among eight labelled points in the Euclidean plane in convex position, some point has no four other points at a common distance.”
Project
- Authors: Egor Lyfar.
- Source: On Sets of Distances of n Points by Paul Erdős, doi:10.1080/00029890.1946.11991674, https://www.erdosproblems.com/97.
- Project repository: lyfar/erdos-97-octagon-lean.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 51K05, 52A10.
- In Lean Pool: LeanPool/Erdos97ConvexOctagon, from the card LeanPool/projects/erdos-97-convex-octagon.yaml.
Sources
TheoremEuclidean Distance Geometry#
Develops the basepoint-centered Gram approach to finite Euclidean distance geometry. Proves both directions of Schoenberg's characterization, including a rank-controlled factorization of positive-semidefinite matrices; proves that three affinely independent centers in Euclidean three-space determine at most two points with prescribed distances; and verifies the Cayley--Menger determinant for segments and triangles, including the triangle-area identity underlying Heron's formula.
Quoted from the card LeanPool/projects/distance-geometry.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
DistanceGeometry.schoenberg(theorem; a main declaration), declared in LeanPool/DistanceGeometry/SchoenbergHard.lean, line 235: “For n at least one, a symmetric hollow n-by-n matrix is a squared-distance matrix of points in k-dimensional Euclidean space exactly when its basepoint-centered Gram matrix is positive semidefinite and has rank at most k.”DistanceGeometry.encard_setOf_forall_dist_eq_le_two(theorem), declared in LeanPool/DistanceGeometry/Trilateration.lean, line 160: “In a finite-dimensional real inner-product affine space, prescribed distances to centers whose affine span has codimension one admit at most two solutions.”DistanceGeometry.trilateration_le_two(theorem; a main declaration), declared in LeanPool/DistanceGeometry/Trilateration.lean, line 188: “Three affinely independent centers in three-dimensional Euclidean space admit at most two points with any prescribed triple of distances.”DistanceGeometry.cayleyMenger_det_heron(theorem), declared in LeanPool/DistanceGeometry/CayleyMengerVolume.lean, line 233: “The Cayley--Menger determinant of three planar points equals minus sixteen times the squared area of their triangle.”
Project
- Authors: Egor Lyfar.
- Source: 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 by Isaac Jacob Schoenberg, doi:10.2307/1968654.
- Project repository: lyfar/distance-geometry-lean.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 51K05, 52C99, 15A18.
- In Lean Pool: LeanPool/DistanceGeometry, from the card LeanPool/projects/distance-geometry.yaml.
Sources
TheoremIndependence of Playfair's axiom via Euclidean and Klein models#
Constructs Euclidean and Klein models of a synthetic Hilbert plane, proving that Playfair's axiom is independent of incidence, Pasch order, and congruence axioms, even with Archimedes and Dedekind continuity. Develops reusable coordinate geometry over ordered fields, projective motions, Klein angles and metric, smooth-path length and distance, congruence constructions, and a coordinate curvature calculation. Dedekind continuity replaces Hilbert's maximal completeness axiom; their equivalence is not formalized. Curvature uses Brioschi's formula, and distance uses C1 paths; no identification with Mathlib's Riemannian distance or connection curvature is asserted.
Quoted from the card LeanPool/projects/parallel-postulate.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
ParallelPostulate.Hilbert.playfair_independent_continuous(theorem; a main declaration), declared in LeanPool/ParallelPostulate.lean, line 4530: “There exists a Hilbert plane satisfying Archimedes and Dedekind continuity and Playfair's axiom, and there exists another satisfying the same continuity axioms and the negation of Playfair's axiom. The models use real coordinate planes with bounds zero and minus one.” Its source, as the card gives it: “Upstream Hilbert/Independence.lean. First publicly announced 2026-09-30 01:08:53 UTC at https://leanprover.zulipchat.com/#narrow/channel/583339-AI-authored-projects/topic/Independence.20Parallel.20Postulate/near/627942879. The author's follow-up discloses mostly AI-written proofs. Pasch order and Dedekind continuity are the stated variants; equivalence to plane separation and maximal completeness is not proved.”ParallelPostulate.HyperbolicPlane.hyperbolic_parallels(theorem), declared in LeanPool/ParallelPostulate/Geometry.lean, line 1179: “Over any linearly ordered field, for every negative bound and every line in the bounded coordinate plane, infinitely many distinct lines pass through any point of the plane outside that line without meeting it.”ParallelPostulate.HyperbolicPlane.kleinDist_eq_arsinh(theorem), declared in LeanPool/ParallelPostulate.lean, line 2667: “For every negative real bound and every pair of points in its plane, the infimum of C1-path lengths in Klein's coordinate metric equals arsinh of the square root of minus the bound times apart, divided by the square root of minus the bound.”ParallelPostulate.HyperbolicPlane.kleinMetric_curvature(theorem), declared in LeanPool/ParallelPostulate.lean, line 2158: “For every real bound, Brioschi's coordinate curvature formula applied to the three coefficients of Klein's metric equals that bound at every point of its coordinate plane.”
Project
- Authors: Richard Sutton.
- Source: ParallelPostulate formalization by Richard Sutton.
- Project repository: Richiesutie/ParallelPostulate, at commit 8ee50280.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 51F15, 51M10, 53A35.
- In Lean Pool: LeanPool/ParallelPostulate, from the card LeanPool/projects/parallel-postulate.yaml.
Sources
TheoremSynthetic Euclidean geometry: Euclid's Elements Book I#
Formalizes Book I of Euclid's Elements via an axiomatic synthetic-geometry system (incidence, betweenness, congruence, and area), culminating in the Pythagorean theorem and its converse.
Quoted from the card LeanPool/projects/synthetic-euclid.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
SyntheticEuclid4.IncidenceGeometry(class), declared in LeanPool/SyntheticEuclid4/Axioms.lean, line 26: “The axiomatic class of synthetic Euclidean geometry, bundling points, lines, circles, and the incidence, betweenness, congruence, and area primitives with Euclid's axioms.”SyntheticEuclid4.square_of_len(theorem), declared in LeanPool/SyntheticEuclid4/SyntheticEuclid4.lean, line 1922: “Constructs a square on a given segment off a given line.”SyntheticEuclid4.pythagoras_construct(theorem), declared in LeanPool/SyntheticEuclid4/SyntheticEuclid4.lean, line 1988: “Constructs the three squares and parallelograms on the sides of a triangle used in the proof of the Pythagorean theorem.”SyntheticEuclid4.pythagoras(theorem; a main declaration), declared in LeanPool/SyntheticEuclid4/SyntheticEuclid4.lean, line 2007: “Euclid I.47, the Pythagorean theorem, that the square on the hypotenuse of a right triangle equals the sum of the squares on the other two sides.”SyntheticEuclid4.pythagoras_converse(theorem; a main declaration), declared in LeanPool/SyntheticEuclid4/SyntheticEuclid4.lean, line 2104: “Euclid I.48, the converse of the Pythagorean theorem, that a triangle whose square areas satisfy the Pythagorean relation has a right angle.”
Project
- Authors: André Hernandez-Espiet, Vladimir Sedlacek.
- Source: A formal system for Euclid's Elements by Jeremy Avigad, Edward Dean, John Mumma, doi:10.1017/S1755020309990098.
- Project repository: ah1112/synthetic_euclid_4.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 51M04.
- In Lean Pool: LeanPool/SyntheticEuclid4, from the card LeanPool/projects/synthetic-euclid.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.