The GitHub account hosting the artifact is not cryptographically bound to the ORCID; see NP2 for that gap.
The specific model version is not recorded in the conversation export; see NP2.
Tarski's Euclidean geometry in Lean 4 - Stages 0-4
A standalone synthetic development of Tarski's axiomatic Euclidean geometry following Schwabhaeuser-Szmielew-Tarski (SST) chapters 2, 3, 4 and 7, culminating in SST 7.13/7.15: point reflection is an isometry. Two primitives, eight axiom groups, no coordinates, no numbers. Contains 40 theorems and 5 definitions in namespace Synthetic.
Lean 4 core; zero import statements; no Mathlib dependency
The ISCC (ISO 24138) above was generated with iscc-core over the exact 28435 bytes retrieved from the raw content URL on 2026-07-29; it binds this declaration to that byte sequence and to no other.
W. Schwabhaeuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Hochschultext, Springer, 1983. Part I, 'Ein axiomatischer Aufbau der euklidischen Geometrie', pp. 1-171.
Metamathematische Methoden in der Geometrie
The source of the 'SST n.m' theorem numbering used throughout the artifact. Part I rests in part on unpublished results of Tarski and Szmielew and on results of H. N. Gupta, per the authors' preface.
The axiomatic ideal the artifact rebuilds, and the straightedge-and-compass constraint that governs it.
The modern axiomatic programme and the segment arithmetic that is the eventual route from this development to Pythagoras.
Contributions to the axiomatic foundations of geometry
Doctoral dissertation, University of California, Berkeley, supervised by Tarski. Source of axiom simplifications adopted in SST and of the continuity-free perpendicular construction that the artifact stops short of.
Origin of the order axiom formalised in the artifact as inner_pasch.
A. Tarski, S. Givant, Tarski's system of geometry, Bulletin of Symbolic Logic 5(2), 1999, pp. 175-214.
Myles Axton thanks his father, Richard Axton (1941-2021), for his introduction to Euclidean geometry and the lifelong inspiration to do more with less - straightedge and compass only.
Each proved statement in the artifact, mapped to its printed SST theorem number and, where one exists, the corresponding GeoCoq lemma label. GeoCoq's lXX_YY labels denote SST Satz XX.YY, so the chapter digit of the label and of the SST reference agree by construction. Chapter titles are given as printed in the 1983 Springer edition.
Theorem-to-source concordance for Tarski.lean
Git blob object identifier (SHA-1 over the 'blob <len>\0' header plus content), for matching against the GitHub object store.
Framed the governing constraint (prove Pythagoras from inside Euclidean space with straightedge and compass only), selected each descent of the trajectory, directed the development to zero sorry, commissioned the provenance record, and published the artifact.
Reconstructed the SST development from the published architecture into dependency-free core Lean 4, re-deriving proof details where recall failed - notably the l4_5 scaffold bookkeeping, the SST 3.7(2) mirror argument, and the three-stroke five-segment cascade that breaks the circularity in SST 7.13. Under prevailing scholarly norms a software agent is not an author; this attribution is an acknowledgement of contribution, and responsibility for correctness rests with the named human agent.
Origin of the lemma labels (l4_2, l4_5, l4_6, l7_13, l7_15) cited in the artifact's comments, and the first machine-checked ascent of the SST development at scale. GeoCoq's file names track SST chapters one-for-one; the artifact reconstructs that architecture and does not port GeoCoq proof scripts. No specific commit was consulted; see NP2.
SST (1983), Satz 3.6(2), chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
SST (1983), Satz 3.6, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
SST (1983), Satz 3.5, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
GeoCoq label: between_inner_transitivity
SST (1983), Satz 3.3, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
SST (1983), Satz 3.7, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
GeoCoq label: outer_transitivity_between
SST (1983), Satz 3.7(2), chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
GeoCoq label: outer_transitivity_between2
SST (1983), Satz 3.2, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
SST (1983), Satz 4.6, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)
SST (1983), Satz 3.1, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
SST (1983), Satz 4.5, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)
SST (1983), Satz 2.11, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
SST (1983), Satz 2.4, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
SST (1983), Satz 2.1, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
SST (1983), Satz 2.5, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
SST (1983), Satz 4.3, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)
SST (1983), Satz 2.2, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
SST (1983), Satz 2.3, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
SST (1983), Satz 2.8, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
SST (1983), Satz 2.12, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
SST (1983), Satz 4.2, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)
SST (1983), Satz 7.15, chapter 7: Punktspiegelungen (pp. 49-56)
SST (1983), Satz 7.13, chapter 7: Punktspiegelungen (pp. 49-56)
SST (1983), Satz 7.4, chapter 7: Punktspiegelungen (pp. 49-56)
GeoCoq label: symmetric_point_construction
SST (1983), Satz 7.5, chapter 7: Punktspiegelungen (pp. 49-56)
GeoCoq label: symmetric_point_uniqueness
Wrote and completed Part I of SST for publication in 1983.
Part I of SST, the development the artifact follows lemma for lemma, grew from her Berkeley lectures; she died in 1976, before publication.
Designed the axiom system (Warsaw, 1926-27) and proved its completeness and decidability.
A port of a large portion of GeoCoq into a branch of mathlib3, described by its author as covering roughly 70 percent of the Tarski work in GeoCoq. Cited here as prior art establishing that Tarski.lean is not the first formalisation of Tarski's axioms in Lean. It is NOT an ancestor of this artifact: see NP2, which records that no derivation relation holds.
Drafting of the credit ledger, its expression as nanopublications, an external review pass on 2026-07-21, and the correction of that review. The correction history is recorded in NP2.
Provenance declaration drafting and revision
Conversation export: Pythagorean theorem in Lean4 inner product spaces
Not publicly resolvable at the time of this declaration; the checksum permits verification if and when it is deposited.
Thirty-six turns beginning from the Pythagorean theorem in Mathlib's inner product spaces, specialising to EuclideanSpace R (Fin n), then inverting the question to ask whether Pythagoras can be earned synthetically from within. The development proceeded in stages: congruence calculus, betweenness calculus, vocabulary, point reflection, the chapter-4 bridge, and finally SST 7.13. Two sorry placeholders were introduced and both were subsequently discharged.
Version 2. Supersedes the 2026-07-21 draft and its external review pass, both of which contained attribution and citation errors now corrected and itemised in NP2.
Tarski.lean: attribution, ancestry and source concordance (v2)