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.
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."
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.
Why this negative-space companion exists
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:
What the AI did not originate: the mathematics — all of it
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
Col, Out, SegLe and their permutation/trivia lemmas — SST ch. 4–6 vocabulary
Midpoint, midpoint_refl, midpoint_symm — SST ch. 7 vocabulary
betw_exchange2 — SST 3.6(2) (GeoCoq between_exchange2)
cong3_construction — SST 4.5 (GeoCoq l4_5)
cong_reverse_identity — corollary of axiom A3
inner_five_segment — SST 4.2 (GeoCoq l4_2)
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).
Prior art the artifact does not originate: GeoLean
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).
Credit that was unclaimed when this inventory was first drafted — since resolved
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).