Tarski.lean provenance and credit declaration
type: Nanopublication
has assertion: assertion
has provenance: provenance
has publication info: pubinfo
created: 2026-07-18T14:45:07Z
creator: https://orcid.org/0000-0002-8042-4131
creator: Claude (Anthropic)
creator: Myles Axton
description: Provenance and credit declaration for Tarski.lean, a dependency-free Lean 4 formalization of Tarski's synthetic Euclidean geometry (SST chapters 2–7, Stages 0–4). Records intellectual lineage (Euclid through Gupta and GeoCoq), the AI-human authorship split, and a dedication.
license: https://creativecommons.org/licenses/by/4.0/
generated at time: 2026-07-18T14:45:07Z

Claude (Anthropic)
type: SoftwareAgent
description: Drafted all Lean code and documentation; reconstructed and in places re-derived the proofs (see sub:faia). In a follow-up session, diagnosed and fixed the sole compile error and verified compilation under two toolchains (see sub:activity-verify). Not an author under prevailing scholarly norms; correctly credited by acknowledgment. All errors in the draft are attributable here, not to the mathematical tradition.
had role: software
had role: validation
had role: writing-original-draft

Euclid of Alexandria (fl. c. 300 BCE)
type: Person
description: The axiomatic ideal the artifact rebuilds; the original tower (Elements, Book I), including target propositions I.47–I.48 (Pythagoras and converse) and Definition I.10, echoed in the planned `Per` (SST ch. 8).
had role: Intellectual ancestor

GeoCoq project (J. Narboux, M. Beeson, P. Boutry, G. Braun, C. Gries, P. Schreck, et al.)
type: Organization
description: First machine-checked ascent of the SST development (Coq, from Narboux 2006 onward). The artifact reconstructs the GeoCoq architecture and navigated by its lemma map (l4_2 → inner_five_segment, l4_3 → cong_sub, l4_5 → cong3_construction, l4_6 → betw_transfer, l7_13 → reflect_cong, l7_15 → reflect_betw) but ports no GeoCoq code.
had role: Formal ancestor

Haragauri Narayan Gupta (1925–2016)
type: Person
description: PhD dissertation, UC Berkeley 1965, under Tarski: axiom independence and simplification (several axioms are as lean as A1–A8 because of him), and the perpendicular and midpoint constructions without any continuity axiom — SST 8.18 and 8.22, the declared next stage of this artifact, not yet contained in it.
had role: Axiom simplifier; author of the continuity-free constructions ahead

David Hilbert (1862–1943)
type: Person
description: Grundlagen der Geometrie (1899): the modern axiomatic program, and the segment arithmetic (Streckenrechnung, cf. SST ch. 14–15) that is the declared future route from this artifact to Pythagoras.
had role: Program architect

Moritz Pasch (1843–1930)
type: Person
description: Discovered that order is an assumption, not a triviality (Vorlesungen über neuere Geometrie, 1882). Namesake of axiom A7 (`inner_pasch`), on which the whole of Stage 2 rests: SST 3.1 (betw_trivial, indirectly), 3.2 (betw_symm), 3.5 (betw_inner_trans).
had role: Axiom source

Wolfram Schwabhäuser (1931–1985)
type: Person
description: Completed and published the treatise: Schwabhäuser, Szmielew, Tarski, 'Metamathematische Methoden in der Geometrie', Springer 1983. Every 'SST n.m' tag in the artifact cites all three authors through his numbering.
had role: Systematizer and publisher

Wanda Szmielew (1918–1976)
type: Person
description: Part I of SST grew from her lectures; the artifact follows her development lemma-for-lemma: SST 2.1–2.5, 2.8, 2.11, 2.12 (congruence calculus, segment addition, construction uniqueness); 3.1–3.3, 3.5, 3.6(1), 3.6(2), 3.7(1), 3.7(2) (betweenness calculus); 4.2, 4.3, 4.5, 4.6 (congruence–betweenness bridge); 7.4, 7.5, 7.13, 7.15 (point reflection and its isometry). She died before publication; her share of the credit is frequently understated.
had role: Development author (followed lemma-for-lemma)

Alfred Tarski (1901–1983)
type: Person
description: The axiom system formalized as the `Tarski` typeclass, axioms A1–A8 (cong_pseudo_refl, cong_inner_trans, cong_identity, segment_construction, five_segment, betw_identity, inner_pasch, lower_dim), developed 1926–27; completeness and decidability of elementary geometry, guaranteeing the synthetic development agrees with EuclideanSpace ℝ (Fin n) on all first-order sentences. Survey citation: Tarski & Givant, 'Tarski's System of Geometry', Bulletin of Symbolic Logic 5(2), 1999.
had role: Axiom-system author; metatheorist

Myles Axton
type: Person
description: Set the organizing question and metaphor (being 'trapped' in EuclideanSpace ℝ (Fin n) with only straightedge and compass), chose each descent (perpendiculars → compiling file → SST ch. 4 block → SST 7.13), and supplied the persistence that drove the artifact to zero `sorry`s. Directed the follow-up session that found a working Lean toolchain, compiled the artifact, and requested the fix for the sole compile error. Holds the director's and verifier's credit.
had role: conceptualization
had role: supervision
had role: validation

Tarski.lean
type: Entity
type: SoftwareSourceCode
contributor: Claude (Anthropic)
contributor: Euclid of Alexandria (fl. c. 300 BCE)
contributor: GeoCoq project (J. Narboux, M. Beeson, P. Boutry, G. Braun, C. Gries, P. Schreck, et al.)
contributor: Haragauri Narayan Gupta (1925–2016)
contributor: David Hilbert (1862–1943)
contributor: Moritz Pasch (1843–1930)
contributor: Wolfram Schwabhäuser (1931–1985)
contributor: Wanda Szmielew (1918–1976)
contributor: Alfred Tarski (1901–1983)
contributor: Myles Axton
relation: Dedication
table of contents: Theorem-to-source concordance
declaration: faia
iscc: ISCC:PENDING — see sub:isccNote
code repository: Tarski.lean
content size: 28435 bytes (648 lines)
description: A synthetic development of Tarski's Euclidean geometry following Schwabhäuser–Szmielew–Tarski (SST) chapters 2–7: eleven axioms over two primitives (betweenness, segment congruence), developed through SST 7.13/7.15 (point reflection is an isometry). Zero `sorry`s. Compiles cleanly (`lean Tarski.lean` and `lake build`, exit 0) under both leanprover/lean4-nightly:nightly-2023-05-16 and leanprover/lean4:v4.32.0, confirming the dependency-free (core-Lean-4-only) claim across toolchain versions.
programming language: Lean 4 (core language only; no Mathlib dependency)

Dedication
type: Comment
description: Myles Axton thanks his father, Richard Axton (1941–2021), for his introduction to Euclidean geometry and the inspiration to do more with less (straight edge and compass only).
about: Richard Axton (1941–2021)

faia
type: AIUsageDeclaration
ai contribution: Reconstruction of the SST/GeoCoq proof architecture from model memory; independent re-derivation where memory was insufficient (the SST 4.5 scaffold bookkeeping; SST 3.7(2) via mirror application of 3.7(1); the five-segment slot assignments in SST 7.13); translation into dependency-free core Lean 4; expository docstrings. In the follow-up session: diagnosed and fixed one compile error (the `example` at the end of Stage 5 used Mathlib's `∃!` unique-existence notation, unavailable in core Lean 4; rewritten as its explicit unfolding), then verified compilation.
ai system: Claude (Anthropic), Claude Fable 5, chat interface, sandboxed (no network, no Lean toolchain), for the original drafting session; Claude (Anthropic), Claude Sonnet 5, Claude Code CLI, with network and a working Lean 4 toolchain, for the subsequent compilation and fix session.
human oversight: Every construction and proof step was chosen or approved turn-by-turn in dialogue; the human set direction, scope, and the requirement of resolving all `sorry`s. The human also directed the follow-up build/fix/compile session and reviewed its result before this declaration was finalized.
known limitations: The artifact now compiles cleanly under two independent Lean 4 toolchains (see schema:description); this discharges the compilation-verification limitation noted in the original sandbox draft. Remaining limitations: the mathematical content has not been cross-checked against an independent formalization (e.g. GeoCoq itself) beyond the lemma-map correspondence in sub:sst-map, and no ISCC or trusted timestamp has yet been minted (see sub:isccNote, sub:timestampNote).
mode: AI-drafted, human-directed
originality statement: No new mathematics. Every theorem in the artifact is prior art carrying an SST number (see sub:sst-map). The creative contributions of the AI-human collaboration are formalization engineering and exposition only.

ISCC binding status
type: Comment
description: ISO 24138 ISCC generation (Meta-, Content-, Data-, Instance-Code units) requires the iscc-core reference implementation, unavailable when this declaration was drafted. The declaration is therefore provisionally bound by the SHA-256 digest recorded in sub:artifact, computed over the compiled, current version of Tarski.lean. Upon finalization: (1) run `iscc-core` over the frozen file to mint the ISCC and replace the PENDING value; (2) obtain an RFC 3161 trusted timestamp or ledger anchor for this document; (3) sign the nanopublication with the declarant's key (this step is completed as of publication of this nanopub).

Richard Axton (1941–2021)
type: Person
description: Introduced Myles Axton to Euclidean geometry. The artifact's governing constraint — do more with less, straight edge and compass only — is his inspiration, and it is the same austerity that runs from Euclid's instruments through Tarski's two primitives to Gupta's removal of the continuity axiom.
had role: Dedicatee; first teacher

Theorem-to-source concordance
type: Dataset
description: Lean name = SST number [= GeoCoq name where applicable]: cong_refl = 2.1; cong_symm = 2.2; cong_trans = 2.3; cong_left_comm = 2.4; cong_right_comm = 2.5; cong_trivial = 2.8; cong_add = 2.11 [l2_11]; construction_uniqueness = 2.12; betw_trivial = 3.1; betw_symm = 3.2; betw_left_trivial = 3.3; betw_inner_trans = 3.5; betw_exchange_left = 3.6(1); betw_exchange2 = 3.6(2) [between_exchange2]; betw_outer_trans = 3.7(1); betw_outer_trans' = 3.7(2); Cong3 = Def. 4.1 [Cong_3]; inner_five_segment = 4.2 [l4_2]; cong_sub = 4.3 [l4_3]; cong3_construction = 4.5 [l4_5]; betw_transfer = 4.6 [l4_6]; symmetric_point_exists = 7.4; symmetric_point_uniqueness = 7.5; reflect_cong = 7.13 [l7_13]; reflect_betw = 7.15 [l7_15]. Axioms A1–A8 = Tarski. Declared future work: Per = Euclid Def. I.10 / SST ch. 8; perpendiculars and midpoints = 8.18, 8.22 (Gupta); target theorem = Pythagoras, Euclid I.47–I.48, via segment arithmetic, SST ch. 14–15 (Hilbert).

Timestamp status
type: Comment
description: All timestamps herein are the system clock of the drafting/verification sessions (self-asserted), not trusted timestamps. They are honest but not tamper-evident.

Interactive formalization dialogue
type: Activity
description: A single sandboxed chat session beginning from the Pythagorean theorem in Mathlib's inner product spaces (norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero) and EuclideanSpace ℝ (Fin n), pivoting to the synthetic question, and building the Lean 4 artifact over successive turns. Sources were drawn from model memory of SST and GeoCoq; no network access and no Lean toolchain were available, so all proofs were verified by hand-tracing (and, for SST 7.13, by an additional coordinate check) rather than by compilation.
started at time: 2026-07-18
used: GeoCoq repository and papers (Narboux et al., 2006–)
used: Schwabhäuser, Szmielew, Tarski — Metamathematische Methoden in der Geometrie (Springer, 1983)
was associated with: Claude (Anthropic)
was associated with: Myles Axton

Build, fix, and compilation verification
type: Activity
description: A follow-up session with a working environment (network access, elan/Lean toolchains). Compiled `lean Tarski.lean` standalone and, separately, built it as a `lake` library target in two projects (pythagoras4, using leanprover/lean4-nightly:nightly-2023-05-16; and lean4-starter, using leanprover/lean4:v4.32.0). Found and fixed one error: the closing `example` used Mathlib's `∃!` notation, unavailable in core Lean 4, rewritten as its explicit unfolding. Both toolchains now build the file with zero errors and zero `sorry`s.
started at time: 2026-07-18
used: Tarski.lean
was associated with: Claude (Anthropic)
was associated with: Myles Axton

GeoCoq repository and papers (Narboux et al., 2006–)
type: Entity
description: Used from model memory as the formalization map; no code consulted or ported in-session.

Schwabhäuser, Szmielew, Tarski — Metamathematische Methoden in der Geometrie (Springer, 1983)
type: Entity
description: Used from model memory as the architectural source; not consulted directly in-session.

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