https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0
.trig | .trig.txt | .jelly | .jelly.txt | .jsonld | .jsonld.txt | .nq | .nq.txt | .xml | .xml.txt
@prefix this: <https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0> .
@prefix sub: <https://w3id.org/np/RA74_wtHUon2rlDQyDGQ3ia3nMhKWu1SoDNR92DTLTFR0/> .
@prefix schema: <http://schema.org/> .
@prefix np: <http://www.nanopub.org/nschema#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix spdx: <http://spdx.org/rdf/terms#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix prov: <http://www.w3.org/ns/prov#> .
@prefix np1: <https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4/> .
@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:agent-reviewer a schema:SoftwareApplication, prov:SoftwareAgent;
schema:name "Google Gemini";
rdfs:comment "Performed the 2026-07-21 review pass. Specific model version not recorded." .
sub:erratum-concordance a schema:Claim, prov:Entity;
schema:about np1:concordance;
schema:datePublished "2026-07-29"^^xsd:date;
schema:name "Erratum: withdrawal of the substituted concordance";
schema:text "An intermediate revision replaced the concordance with the mapping inner_five_segment = SST 2.13, cong_sub = SST 2.14, cong3_construction = SST 2.16, betw_transfer = SST 3.17. That mapping is unsupported and is withdrawn. GeoCoq's convention is that the label lX_Y denotes SST Satz X.Y, so l4_2, l4_3, l4_5 and l4_6 denote Saetze 4.2, 4.3, 4.5 and 4.6, which is what the artifact's own source comments state and what the original concordance recorded. The concordance in NP1 was regenerated directly from the artifact's source text on 2026-07-29." .
sub:erratum-myers a schema:Claim, prov:Entity;
schema:about sub:prior-art-geolean;
schema:datePublished "2026-07-29"^^xsd:date;
schema:name "Erratum: misattribution of GeoLean to Joseph Myers";
schema:text "GeoLean is the work of Bhavik Mehta alone. An assistant turn on 2026-07-18 attributed it to Joseph Myers, conflating it with Myers' analytic EuclideanGeometry development in Mathlib, which is a different body of work using a different approach. The 2026-07-21 external review pass partially corrected this by adding Mehta but retained Myers, producing the compound misattribution 'GeoLean Project (J. Myers, B. Mehta)'. Both forms are wrong and are withdrawn. Corrected against the leanprover Zulip archive, thread 'tarski axiom geometry', in which Mehta refers to GeoLean in the first person and separately distinguishes it from Joseph's development." .
sub:erratum-sst-chapter a schema:Claim, prov:Entity;
dct:source <https://doi.org/10.1007/978-3-642-69418-9>;
schema:about np1:concordance;
schema:datePublished "2026-07-29"^^xsd:date;
schema:name "Erratum: withdrawal of the claimed SST chapter mismapping";
schema:text "An intermediate revision of this record asserted that SST chapter 4 is devoted exclusively to the upper dimension axiom, that the congruence-betweenness bridge lemmas belong to chapters 2 and 3, and that GeoCoq's 'Ch04' designation is a repository artifact. All three assertions are false and are withdrawn. In the 1983 Springer edition, chapter 4 is 'Einfache Saetze ueber Kongruenz und Zwischenbeziehung', pp. 34-38, which is exactly the bridge material; chapter 7 is 'Punktspiegelungen', pp. 49-56, the point reflections that SST 7.13 belongs to; and upper dimension is an axiom introduced with the axiom system, not a chapter. GeoCoq's file naming tracks the printed chapter sequence faithfully." .
sub:gap-geocoq-commit a schema:Claim;
schema:about np1:src-geocoq;
schema:name "Gap: no GeoCoq or SST edition is pinned";
schema:text "The artifact cites GeoCoq lemma labels but no commit, tag or version of GeoCoq was consulted or can be pinned, because the labels were reconstructed from the software agent's training data rather than read from the repository. Likewise no page-level citation to a specific printing of SST was checked at drafting time. Chapter titles and pagination were verified against the publisher's record on 2026-07-29; individual Satz numbers were not verified against the printed page and rest on GeoCoq's labelling convention." .
sub:gap-identity-binding a schema:Claim;
schema:about np1:agent-axton;
schema:name "Gap: repository identity is not bound to the declared ORCID";
schema:text "The artifact is hosted under a GitHub account whose ownership is not cryptographically or publicly linked to the ORCID declared in NP1. Until the declaration is signed with a key bound to that identity, the attribution rests on assertion alone." .
sub:gap-model-version a schema:Claim;
schema:about np1:agent-claude;
schema:name "Gap: the model version is not recorded";
schema:text "The conversation export identifies the software agent only as 'Claude (Anthropic PBC)'. The specific model version that produced the proofs is not recoverable from the record, which limits reproducibility of the generation step." .
sub:gap-no-license a schema:Claim;
schema:about np1:artifact;
schema:name "Gap: the artifact carries no licence";
schema:text "The hosting repository contains no LICENSE file and Tarski.lean carries no licence header, so the artifact is under default exclusive copyright and cannot lawfully be reused, redistributed or built upon by third parties. This blocks the citation and reuse that the rest of this record is designed to enable. A permissive licence, Apache-2.0 to match Lean and Mathlib, should be added before publication." .
sub:non-derivation-geolean a schema:Claim;
dct:references np1:src-geolean;
schema:about np1:artifact;
schema:name "Negative claim: no derivation relation holds between GeoLean and this artifact";
schema:text "GeoLean was not consulted during the development of Tarski.lean. It surfaced only afterwards, during a web search on 2026-07-18 undertaken to check the publication landscape. No identifier, tactic or proof structure in Tarski.lean is inherited from it. The naming that Tarski.lean does inherit comes from GeoCoq's lemma labels and from SST's theorem numbering, both of which predate GeoLean. Asserting a GeoLean-to-Tarski.lean derivation, as an intermediate draft of this record did, would misdescribe the artifact and misattribute its lineage." .
sub:non-origination a schema:Claim;
schema:about np1:artifact;
schema:name "The software agent did not originate the mathematics";
schema:text "No mathematics in Tarski.lean is new. Every proved statement carries a printed SST theorem number, enumerated in the concordance in NP1; the axiom system is Tarski's, the order axiom is Pasch's, the axiom simplifications are Gupta's, and the proof architecture is that of SST Part I as machine-checked at scale in GeoCoq. The software agent's contribution is translation, reconstruction and exposition into Lean 4, together with the re-derivation of proof details it could not recall. Novelty, if any, is confined to the Lean 4 rendering and to the particular route taken through SST 7.13." .
sub:prior-art-geolean a schema:Claim;
dct:references np1:src-geolean;
schema:about np1:artifact;
schema:name "Prior art: Tarski.lean is not the first Tarski formalisation in Lean";
schema:text "The GeoLean branch of mathlib3, by Bhavik Mehta, ports a large portion of GeoCoq into Lean 3 and predates this artifact. Any claim of priority for Tarski.lean must be narrowed accordingly: what is distinctive is that it is a dependency-free single file in Lean 4 core, not that it is first." .
sub:review-finding a schema:Claim;
schema:about sub:agent-reviewer;
schema:name "Finding: both automated review passes introduced citation errors";
schema:text "Two language models in sequence produced confident, well-formed, incorrect citations in the layer of the record whose function is trustworthiness: the drafting agent misattributed GeoLean, and the reviewing agent added a fabricated chapter erratum and a fabricated concordance while only partly fixing the misattribution it was reviewing. This is recorded as an empirical result about the method, not merely as housekeeping. It implies that a provenance record produced or reviewed by a language model requires source-level human or programmatic verification before it can carry evidential weight, and that the review step itself needs its own provenance." .
sub:scope-limit a schema:Claim;
schema:about np1:artifact;
schema:name "Scope: the development stops well short of Pythagoras";
schema:text "The artifact reaches SST 7.15. It does not define right angles, does not construct the dropped perpendicular without continuity (SST 8.18, after Gupta 1965), does not prove midpoint existence (SST 8.22), and contains no line reflections, angles, parallels or segment arithmetic. The Pythagorean theorem, which motivated the trajectory, is not proved and is many chapters away; reaching it requires the construction of an ordered field from the geometry." .
sub:unclaimed-independent-verification a schema:Claim;
schema:about np1:artifact;
schema:name "Unclaimed: independent verification by a human agent";
schema:text "Compilation has been performed and is asserted in NP3, but by a software agent in an ephemeral sandbox. No human agent has independently re-run the build, and no continuous integration exists in the hosting repository to make the result repeatable on every commit. The CRediT validation role is therefore claimed only in the weak sense recorded in NP3, and independent replication remains outstanding." .
sub:unclaimed-peer-review a schema:Claim;
schema:about np1:artifact;
schema:name "Unclaimed: peer review and archival deposit";
schema:text "The artifact has not been refereed, has no DOI, and has not been deposited in an archival repository. Compilation establishes that the proofs are accepted by the Lean kernel; it does not establish that the axioms as transcribed are a faithful rendering of Tarski's, that the definitions are the intended ones, or that the statements are the ones SST proves. Those are questions of adequacy, not of soundness, and only a human reader of both texts can settle them." .
}
sub:provenance {
sub:activity-correction a prov:Activity;
dct:description "Each disputed claim in the 2026-07-21 revision was checked against a primary or near-primary source: chapter titles and pagination against the publisher's table of contents for the 1983 edition, the GeoLean attribution against the leanprover community Zulip archive, and the concordance against the artifact's own source text, retrieved and re-hashed on the same date.";
schema:name "Source-level verification and correction of the declaration record";
prov:startedAtTime "2026-07-29T00:00:00Z"^^xsd:dateTime;
prov:used sub:evidence-springer, sub:evidence-zulip, np1:artifact;
prov:wasAssociatedWith np1:agent-axton, np1:agent-claude .
sub:activity-review a prov:Activity;
dct:description "Produced the revision superseded by this record. Its one substantive contribution, the GeoLean prior-art disclosure, is retained in corrected form; its three citation claims are withdrawn under the errata above.";
schema:name "External review pass";
prov:endedAtTime "2026-07-21T13:56:27Z"^^xsd:dateTime;
prov:generated sub:superseded-v1;
prov:wasAssociatedWith sub:agent-reviewer .
sub:assertion prov:wasAttributedTo np1:agent-axton, np1:agent-claude;
prov:wasGeneratedBy sub:activity-correction .
sub:checksum-superseded a spdx:Checksum;
spdx:algorithm spdx:checksumAlgorithm_sha256;
spdx:checksumValue "3ce67a1938db370e60e2ad6794f1a401119d0e27a999b64da8bc4e3a3a29ed80";
rdfs:comment "Computed over the file as received, which was RTF-encoded and did not parse as JSON-LD." .
sub:evidence-springer a prov:Entity;
schema:name "Publisher table of contents, SST 1983";
schema:url <https://link.springer.com/book/10.1007/978-3-642-69418-9>;
prov:wasUsedBy sub:activity-correction .
sub:evidence-zulip a prov:Entity;
schema:name "leanprover community Zulip archive, stream maths, topic 'tarski axiom geometry'";
schema:url <https://leanprover-community.github.io/archive/stream/116395-maths/topic/tarski.20axiom.20geometry.html>;
prov:wasUsedBy sub:activity-correction .
sub:superseded-v1 a prov:Entity;
schema:name "Tarski_negative-space.jsonld (2026-07-21 revision)";
spdx:checksum sub:checksum-superseded;
prov:wasInvalidatedBy sub:activity-correction .
}
sub:pubinfo {
this: dct:created "2026-07-29T15:00:47Z"^^xsd:dateTime;
dct:creator np1:agent-axton;
dct:description "Version 2. Records what the artifact does not claim, what credit is unclaimed, what the record itself does not know, and the specific errors introduced into earlier versions of this record by both the drafting and the reviewing agent.";
dct:license <http://creativecommons.org/publicdomain/zero/1.0/>;
dct:relation <https://w3id.org/np/RA7RBeB2OR8Az0j6CgSGuUakKatipUYZdWJtt335KfhP4>;
rdfs:label "Tarski.lean: negative space, limits and errata (v2)";
prov:wasAttributedTo np1:agent-axton .
sub:sig npx:hasAlgorithm "RSA";
npx:hasPublicKey "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB";
npx:hasSignature "DL8h/iZKQhW3dBm19cQeemf5y6vkDI9RgWuIhmGg2Ai/mChCJhNVFULVKJkT3lUZnvRBb7wSWgn52foCpejyY+G4UKgT2+fOe6vgaWXPc0evxnq9U3AFhwVRSZA9Gi/obCoIStBhLmS/TgEA2ziAbVQ63q//vx4Tcv5h9zKJdBaeciGuMr/Y8JBrtXdd3ZNpCR+oiPOQ1VHZAuaPWeQ5sivh4MCtbVBm71e8L7Jc29ACZsFNeGkElqgRJMOnuLDyHZylLkgy+VI6WMkSfeu75C7pid18R9Dh7o6ZibyvHOMlcXBiGeKqdzFKydVwyb+re9YsPJrJ8zuGUxM8XvGIUw==";
npx:hasSignatureTarget this:;
npx:signedBy <https://orcid.org/0000-0002-8042-4131> .
}