Tarski.lean negative-space declaration
type: Nanopublication
has assertion: assertion
has provenance: provenance
has publication info: pubinfo
created: 2026-07-18T15:28:18Z
creator: https://orcid.org/0000-0002-8042-4131
creator: agent-claude
creator: agent-user
description: Negative-space companion to the Tarski.lean provenance declaration: what the artifact does not originate (the mathematics, all of it, and GeoLean as uncredited-until-now sibling prior art), and credit that was unclaimed as of first drafting. The neg: vocabulary used here is proposed and local to this declaration, not an established standard.
license: https://creativecommons.org/licenses/by/4.0/
generated at time: 2026-07-18T15:28:18Z

GeoLean citation and human verification
type: Comment
description: This statement was verified by Myles Axton (orcid:0000-0002-8042-4131) on 2026-07-18T15:17:00Z (16:17 UTC+1).
was attributed to: https://orcid.org/0000-0002-8042-4131
citation: Bhavik Mehta, Zulip (leanprover-community.github.io archive), "tarski axiom geometry" topic, Oct 20 2021 at 12:39: "In the GeoLean branch of mathlib I also did a development of Tarskis axioms, covering about 70% of the Tarski work in the GeoCoq project."

Why this negative-space companion exists
type: Motivation
description: The motivation of this nanopublication is to advance the use of FAIA and ISCC to add provenance and human/agent-role attribution to the formalization of our shared mathematical culture. In particular, this nanopublication explores the negative space of what was not done. Many people over roughly 2500 years of mathematics deserve credit for the development of formal mathematical axioms and theorems. By formalizing part of this historical trajectory, this artifact is offered as a substrate for nanopublications that restore context and provenance to results typically stripped down to their elegant statement and proof — to the lamentation of teachers, students, engineers, statisticians, and curious readers.

What the AI did not originate: the mathematics — all of it
type: NonOrigination
description: Every axiom and every theorem in the bound artifact is prior art. The AI's contribution is confined to Lean 4 engineering and exposition; where proof details were re-derived in-session rather than recalled, what was re-derived is known mathematics. The complete inventory:
concerns: artifact
items: Axioms A1–A8 (cong_pseudo_refl, cong_inner_trans, cong_identity, segment_construction, five_segment, betw_identity, inner_pasch, lower_dim) — Tarski, 1926–27; A7 after Pasch, 1882
items: Col, Out, SegLe and their permutation/trivia lemmas — SST ch. 4–6 vocabulary
items: Cong3 — SST Def. 4.1 (GeoCoq Cong_3)
items: Midpoint, midpoint_refl, midpoint_symm — SST ch. 7 vocabulary
items: betw_exchange2 — SST 3.6(2) (GeoCoq between_exchange2)
items: betw_exchange_left — SST 3.6(1)
items: betw_inner_trans — SST 3.5
items: betw_left_trivial — SST 3.3
items: betw_outer_trans — SST 3.7(1)
items: betw_outer_trans' — SST 3.7(2)
items: betw_symm — SST 3.2
items: betw_transfer — SST 4.6 (GeoCoq l4_6)
items: betw_trivial — SST 3.1
items: cong3_construction — SST 4.5 (GeoCoq l4_5)
items: cong_add — SST 2.11 (GeoCoq l2_11)
items: cong_comm — corollary of SST 2.4 + 2.5
items: cong_left_comm — SST 2.4
items: cong_refl — SST 2.1
items: cong_reverse_identity — corollary of axiom A3
items: cong_right_comm — SST 2.5
items: cong_sub — SST 4.3 (GeoCoq l4_3)
items: cong_symm — SST 2.2
items: cong_trans — SST 2.3
items: cong_trivial — SST 2.8
items: construction_uniqueness — SST 2.12
items: inner_five_segment — SST 4.2 (GeoCoq l4_2)
items: reflect_betw — SST 7.15 (GeoCoq l7_15)
items: reflect_cong — SST 7.13 (GeoCoq l7_13)
items: symmetric_point_exists — SST 7.4
items: symmetric_point_uniqueness — SST 7.5

Prior art the artifact does not originate: GeoLean
type: PriorArtDisclosure
description: To the drafting AI's knowledge, Claude did not consult or port GeoLean in producing Tarski.lean. But GeoLean — Joseph Myers's Lean formalization of a large portion of GeoCoq's Tarski development, on a mathlib3 branch — predates this artifact and must be cited as a sibling ancestor alongside GeoCoq. The community view at the time (see sub:geolean-citation) was that axiomatic geometry belongs in standalone projects rather than in Mathlib itself. Tarski.lean is therefore not the first formalization of Tarski's axioms in Lean, but is, to the same knowledge, the first done as a self-contained, native-style Lean 4 development (GeoLean is Lean 3, Coq-styled).
source: GeoLean citation and human verification
concerns: artifact

Credit that was unclaimed when this inventory was first drafted — since resolved
type: UnclaimedCredit
description: As of this nanopublication's original drafting (2026-07-18T11:11:40Z), credit:validation — verification by compilation (`lean Tarski.lean`) — was claimed by no party: the artifact had never been compiled, and every correctness claim was a hand-verification claim. That gap has since closed. A follow-up session compiled the artifact successfully under two independent Lean 4 toolchains (leanprover/lean4-nightly:nightly-2023-05-16 and leanprover/lean4:v4.32.0), after finding and fixing the one error present (a use of Mathlib's `∃!` notation, unavailable in core Lean 4). credit:validation is now jointly claimed by Claude and Myles Axton, as recorded in the companion positive-space nanopublication (see sub:pubinfo dct:references).
had role: validation

Negative-space inventory
type: Activity
description: Drafted in the same sandboxed session as the artifact it concerns, as a companion to the positive declaration, subsequently compiled, signed, and published as https://w3id.org/np/RAXut_tYBIBaf53frjHN9ttCnUj4zq8JhXllSz7MyKpME. The inventory was compiled by reading the artifact's theorem list against the SST concordance recorded there. Revised in a follow-up session to update the stale compilation-status claim, and to incorporate two further disclosures supplied by the human party: the motivation for this negative-space companion, and the GeoLean prior-art citation (with its Zulip source and human verification).
started at time: 2026-07-18T11:11:40Z
was associated with: agent-claude
was associated with: agent-user

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