Tarski.lean: attribution, ancestry and source concordance (v2)
type: Nanopublication
has assertion: assertion
has provenance: provenance
has publication info: pubinfo
created: 2026-07-29T15:00:47Z
creator: Myles Axton
description: 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.
license: http://creativecommons.org/publicdomain/zero/1.0/
has nanopub type: Attribution
introduces: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
was attributed to: Myles Axton

Anthropic PBC
type: Organization

Myles Axton
type: Person
comment: The GitHub account hosting the artifact is not cryptographically bound to the ORCID; see NP2 for that gap.
account: johnmaxton

Claude (Anthropic PBC)
type: SoftwareApplication
type: SoftwareAgent
publisher: Anthropic PBC
comment: The specific model version is not recorded in the conversation export; see NP2.

Tarski's Euclidean geometry in Lean 4 - Stages 0-4
type: SoftwareSourceCode
type: Entity
conforms to: Metamathematische Methoden in der Geometrie
references: Euclid
references: David Hilbert
references: Contributions to the axiomatic foundations of geometry
references: Vorlesungen ueber neuere Geometrie
references: Tarski's system of geometry
relation: Dedication
table of contents: Theorem-to-source concordance for Tarski.lean
filename: Tarski.lean
code repository: lean4-starter
description: 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.
encoding format: text/x-lean
file size: 28435
name: Tarski.lean
programming language: Lean 4
runtime platform: Lean 4 core; zero import statements; no Mathlib dependency
checksum: checksum-gitblob
checksum: checksum-sha256
comment: 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.
qualified attribution: attr-axton
qualified attribution: attr-claude
was generated by: Interactive formalization dialogue

Metamathematische Methoden in der Geometrie
type: Book
type: Entity
bibliographic citation: 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.
author: Wolfram Schwabhaeuser
author: Wanda Szmielew
author: Alfred Tarski
date published: 1983
isbn: 978-3-540-12958-5
publisher: Springer-Verlag, Berlin Heidelberg
comment: 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.

Euclid
type: Person
comment: The axiomatic ideal the artifact rebuilds, and the straightedge-and-compass constraint that governs it.

David Hilbert
type: Person
comment: 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
type: Thesis
type: Entity
author: Haragauri Narayan Gupta
date published: 1965
comment: 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.

Vorlesungen ueber neuere Geometrie
type: Book
type: Entity
author: Moritz Pasch
date published: 1882
comment: Origin of the order axiom formalised in the artifact as inner_pasch.

Tarski's system of geometry
type: ScholarlyArticle
type: Entity
bibliographic citation: A. Tarski, S. Givant, Tarski's system of geometry, Bulletin of Symbolic Logic 5(2), 1999, pp. 175-214.
author: Alfred Tarski
contributor: Steven Givant
date published: 1999

Dedication
type: Comment
about: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
mentions: Richard Axton
text: 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.

Theorem-to-source concordance for Tarski.lean
type: Dataset
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
description: 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.

checksum-gitblob
type: Checksum
algorithm: checksumAlgorithm sha1
comment: Git blob object identifier (SHA-1 over the 'blob <len>\0' header plus content), for matching against the GitHub object store.

attr-axton
type: Attribution
description: 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.
agent: Myles Axton
had role: conceptualization
had role: investigation
had role: project-administration
had role: supervision

attr-claude
type: Attribution
description: 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.
agent: Claude (Anthropic PBC)
had role: formal-analysis
had role: software
had role: writing-original-draft

GeoCoq
type: SoftwareSourceCode
type: Entity
license: LGPL-3.0-only
author: Julien Narboux
contributor: C. Gries
contributor: G. Braun
contributor: M. Beeson
contributor: P. Boutry
contributor: P. Schreck
programming language: Coq
comment: 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.

Richard Axton
type: Person
birth date: 1941
death date: 2021

Synthetic.betw_exchange2
type: Entity
bibliographic citation: SST (1983), Satz 3.6(2), chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: between_exchange2

Synthetic.betw_exchange_left
type: Entity
bibliographic citation: SST (1983), Satz 3.6, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: between_exchange3

Synthetic.betw_inner_trans
type: Entity
bibliographic citation: SST (1983), Satz 3.5, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: between_inner_transitivity

Synthetic.betw_left_trivial
type: Entity
bibliographic citation: SST (1983), Satz 3.3, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean

Synthetic.betw_outer_trans
type: Entity
bibliographic citation: SST (1983), Satz 3.7, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: outer_transitivity_between

Synthetic.betw_outer_trans'
type: Entity
bibliographic citation: SST (1983), Satz 3.7(2), chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: outer_transitivity_between2

Synthetic.betw_symm
type: Entity
bibliographic citation: SST (1983), Satz 3.2, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: between_symmetry

Synthetic.betw_transfer
type: Entity
bibliographic citation: SST (1983), Satz 4.6, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: l4_6

Synthetic.betw_trivial
type: Entity
bibliographic citation: SST (1983), Satz 3.1, chapter 3: Einfache Saetze ueber die Zwischenbeziehung (pp. 30-33)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean

Synthetic.cong3_construction
type: Entity
bibliographic citation: SST (1983), Satz 4.5, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: l4_5

Synthetic.cong_add
type: Entity
bibliographic citation: SST (1983), Satz 2.11, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: l2_11

Synthetic.cong_left_comm
type: Entity
bibliographic citation: SST (1983), Satz 2.4, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean

Synthetic.cong_refl
type: Entity
bibliographic citation: SST (1983), Satz 2.1, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean

Synthetic.cong_right_comm
type: Entity
bibliographic citation: SST (1983), Satz 2.5, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean

Synthetic.cong_sub
type: Entity
bibliographic citation: SST (1983), Satz 4.3, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: l4_3

Synthetic.cong_symm
type: Entity
bibliographic citation: SST (1983), Satz 2.2, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean

Synthetic.cong_trans
type: Entity
bibliographic citation: SST (1983), Satz 2.3, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean

Synthetic.cong_trivial
type: Entity
bibliographic citation: SST (1983), Satz 2.8, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean

Synthetic.construction_uniqueness
type: Entity
bibliographic citation: SST (1983), Satz 2.12, chapter 2: Folgerungen aus A1 bis A5 (pp. 27-29)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: construction_uniqueness

Synthetic.inner_five_segment
type: Entity
bibliographic citation: SST (1983), Satz 4.2, chapter 4: Einfache Saetze ueber Kongruenz und Zwischenbeziehung (pp. 34-38)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: l4_2

Synthetic.reflect_betw
type: Entity
bibliographic citation: SST (1983), Satz 7.15, chapter 7: Punktspiegelungen (pp. 49-56)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: l7_15

Synthetic.reflect_cong
type: Entity
bibliographic citation: SST (1983), Satz 7.13, chapter 7: Punktspiegelungen (pp. 49-56)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: l7_13

Synthetic.symmetric_point_exists
type: Entity
bibliographic citation: SST (1983), Satz 7.4, chapter 7: Punktspiegelungen (pp. 49-56)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: symmetric_point_construction

Synthetic.symmetric_point_uniqueness
type: Entity
bibliographic citation: SST (1983), Satz 7.5, chapter 7: Punktspiegelungen (pp. 49-56)
is part of: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
is referenced by: Theorem-to-source concordance for Tarski.lean
see also: GeoCoq label: symmetric_point_uniqueness

Haragauri Narayan Gupta
type: Person

Bhavik Mehta
type: Person

Julien Narboux
type: Person

Moritz Pasch
type: Person

Wolfram Schwabhaeuser
type: Person
comment: Wrote and completed Part I of SST for publication in 1983.

Wanda Szmielew
type: Person
comment: Part I of SST, the development the artifact follows lemma for lemma, grew from her Berkeley lectures; she died in 1976, before publication.

Alfred Tarski
type: Person
comment: Designed the axiom system (Warsaw, 1926-27) and proved its completeness and decidability.

GeoLean (mathlib3 branch)
type: SoftwareSourceCode
type: Entity
author: Bhavik Mehta
programming language: Lean 3
comment: 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.

Provenance declaration drafting and revision
type: Activity
description: 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.
ended at time: 2026-07-29T00:00:00Z
started at time: 2026-07-18T10:37:00Z
used: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
used: Conversation export: Pythagorean theorem in Lean4 inner product spaces
was associated with: Myles Axton
was associated with: Claude (Anthropic PBC)

Conversation export: Pythagorean theorem in Lean4 inner product spaces
type: Dataset
type: Entity
date created: 2026-07-21T08:51:48Z
encoding format: application/json
file size: 69228
checksum: checksum-transcript
comment: Not publicly resolvable at the time of this declaration; the checksum permits verification if and when it is deposited.

Interactive formalization dialogue
type: Activity
description: 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.
ended at time: 2026-07-19T07:51:20Z
generated: Tarski's Euclidean geometry in Lean 4 - Stages 0-4
generated: Conversation export: Pythagorean theorem in Lean4 inner product spaces
started at time: 2026-07-18T08:47:58Z
used: GeoCoq
used: Metamathematische Methoden in der Geometrie
was associated with: Myles Axton
was associated with: Claude (Anthropic PBC)

sig
has algorithm: RSA
signed by: https://orcid.org/0000-0002-8042-4131