https://w3id.org/np/RAbyUSg8hPy5xsGsGyFVyIoSk3XkETkUo3mg0aMxepyPg
.trig | .trig.txt | .jelly | .jelly.txt | .jsonld | .jsonld.txt | .nq | .nq.txt | .xml | .xml.txt
@prefix this: <https://w3id.org/np/RAbyUSg8hPy5xsGsGyFVyIoSk3XkETkUo3mg0aMxepyPg> .
@prefix sub: <https://w3id.org/np/RAbyUSg8hPy5xsGsGyFVyIoSk3XkETkUo3mg0aMxepyPg/> .
@prefix schema: <https://schema.org/> .
@prefix neg: <urn:sandbox:tarski-lean4-negative-space:vocab#> .
@prefix np: <http://www.nanopub.org/nschema#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix pos: <https://w3id.org/np/RAXut_tYBIBaf53frjHN9ttCnUj4zq8JhXllSz7MyKpME/> .
@prefix nt: <https://w3id.org/np/o/ntemplate/> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix orcid: <https://orcid.org/> .
@prefix credit: <https://credit.niso.org/contributor-roles/> .
@prefix prov: <http://www.w3.org/ns/prov#> .
@prefix npx: <http://purl.org/nanopub/x/> .
sub:Head {
this: a np:Nanopublication;
np:hasAssertion sub:assertion;
np:hasProvenance sub:provenance;
np:hasPublicationInfo sub:pubinfo .
}
sub:assertion {
sub:geolean-citation a schema:Comment;
dct:description "This statement was verified by Myles Axton (orcid:0000-0002-8042-4131) on 2026-07-18T15:17:00Z (16:17 UTC+1).";
prov:wasAttributedTo orcid:0000-0002-8042-4131;
schema: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.\"";
schema:name "GeoLean citation and human verification";
schema:url <https://leanprover-community.github.io/archive/stream/116395-maths/topic/tarski.20axiom.20geometry.html> .
sub:motivation a neg:Motivation;
dct: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.";
schema:name "Why this negative-space companion exists" .
sub:non-origination a neg:NonOrigination;
dct: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:";
schema:name "What the AI did not originate: the mathematics — all of it";
neg:concerns pos:artifact;
neg: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",
"Col, Out, SegLe and their permutation/trivia lemmas — SST ch. 4–6 vocabulary", "Cong3 — SST Def. 4.1 (GeoCoq Cong_3)",
"Midpoint, midpoint_refl, midpoint_symm — SST ch. 7 vocabulary", "betw_exchange2 — SST 3.6(2) (GeoCoq between_exchange2)",
"betw_exchange_left — SST 3.6(1)", "betw_inner_trans — SST 3.5", "betw_left_trivial — SST 3.3",
"betw_outer_trans — SST 3.7(1)", "betw_outer_trans' — SST 3.7(2)", "betw_symm — SST 3.2",
"betw_transfer — SST 4.6 (GeoCoq l4_6)", "betw_trivial — SST 3.1", "cong3_construction — SST 4.5 (GeoCoq l4_5)",
"cong_add — SST 2.11 (GeoCoq l2_11)", "cong_comm — corollary of SST 2.4 + 2.5", "cong_left_comm — SST 2.4",
"cong_refl — SST 2.1", "cong_reverse_identity — corollary of axiom A3", "cong_right_comm — SST 2.5",
"cong_sub — SST 4.3 (GeoCoq l4_3)", "cong_symm — SST 2.2", "cong_trans — SST 2.3",
"cong_trivial — SST 2.8", "construction_uniqueness — SST 2.12", "inner_five_segment — SST 4.2 (GeoCoq l4_2)",
"reflect_betw — SST 7.15 (GeoCoq l7_15)", "reflect_cong — SST 7.13 (GeoCoq l7_13)",
"symmetric_point_exists — SST 7.4", "symmetric_point_uniqueness — SST 7.5" .
sub:prior-art-geolean a neg:PriorArtDisclosure;
dct: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).";
dct:source sub:geolean-citation;
schema:name "Prior art the artifact does not originate: GeoLean";
neg:concerns pos:artifact .
sub:unclaimed-credit a neg:UnclaimedCredit;
dct: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).";
prov:hadRole credit:validation;
schema:name "Credit that was unclaimed when this inventory was first drafted — since resolved" .
}
sub:provenance {
sub:activity a prov:Activity;
dct: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).";
prov:startedAtTime "2026-07-18T11:11:40Z"^^xsd:dateTime;
prov:wasAssociatedWith pos:agent-claude, pos:agent-user;
schema:name "Negative-space inventory" .
sub:assertion prov:wasGeneratedBy sub:activity .
}
sub:pubinfo {
this: dct:created "2026-07-18T15:28:18Z"^^xsd:dateTime;
dct:creator orcid:0000-0002-8042-4131, pos:agent-claude, pos:agent-user;
dct: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.";
dct:license <https://creativecommons.org/licenses/by/4.0/>;
dct:references <https://w3id.org/np/RAXut_tYBIBaf53frjHN9ttCnUj4zq8JhXllSz7MyKpME>;
rdfs:label "Tarski.lean negative-space declaration";
prov:generatedAtTime "2026-07-18T15:28:18Z"^^xsd:dateTime;
nt:wasCreatedFromProvenanceTemplate <http://purl.org/np/RANwQa4ICWS5SOjw7gp99nBpXBasapwtZF1fIM3H2gYTM>;
nt:wasCreatedFromPubinfoTemplate <http://purl.org/np/RAA2MfqdBCzmz9yVWjKLXNbyfBNcwsMmOqcNUxkk1maIM>,
<http://purl.org/np/RAjpBMlw3owYhJUBo3DtsuDlXsNAJ8cnGeWAutDVjuAuI>;
nt:wasCreatedFromTemplate <http://purl.org/np/RAFu2BNmgHrjOTJ8SKRnKaRp-VP8AOOb7xX88ob0DZRsU> .
sub:sig npx:hasAlgorithm "RSA";
npx:hasPublicKey "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB";
npx:hasSignature "ilPSEUWaOvn8cmE4tvw6QHZMEVgQkg4A7w5+qnOaBRocdJsCwodvJRx1H05mJyWRzGU/IERv7S6hnE62IdEa0w80qsm1X9aTvFPJex1RDJHuq9kfwG+vuONkrKIZxjA0FD1jSo7QNUJ9m//b0/iJ3Q+hehkjA1quXKNeWq5MozKsF/9fCt8sqQ2eKOw2gK/r65ksO4c+1n6xO+wQ29Z1tQhiT49suYD8x2AGRSmPuAvRDKVGAlv/LOYN3Bdiu62wsHNoY5xcXh2yGz9v3ZXBfS+xuCeziu6kXHybtXr/ca0uj7inYY4oQCFWBOwAppbbHYmroqlIS1xk/GVqLnegTw==";
npx:hasSignatureTarget this:;
npx:signedBy orcid:0000-0002-8042-4131 .
}