https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/Head https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/assertion https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/provenance https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/pubinfo https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/assertion https://provenance.example/tarski-lean/activity-bare-api-attempt http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://provenance.example/tarski-lean/activity-bare-api-attempt http://www.w3.org/2000/01/rdf-schema#label First attempt via a bare messages.create() API call (claude_convo_.py, no tools bound) https://provenance.example/tarski-lean/activity-bare-api-attempt http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-bare-api-validation https://provenance.example/tarski-lean/activity-bare-api-attempt http://www.w3.org/ns/prov#used https://provenance.example/tarski-lean/activity-request https://provenance.example/tarski-lean/activity-bare-api-attempt http://www.w3.org/ns/prov#wasAssociatedWith https://provenance.example/tarski-lean/agent-claude-bare-api https://provenance.example/tarski-lean/activity-bare-api-attempt https://provenance.example/tarski-lean/outcome No machine- or source-verified content was produced by this activity. Superseded by d:activity-claude-code-session below, which had actual tool access. https://provenance.example/tarski-lean/activity-bare-api-attempt https://provenance.example/tarski-lean/producedClaim Explicit refusal to fabricate hash/ISCC/compilation/concordance results, on the grounds that no tools were available in that call; produced only a negative-space accounting, itself truncated at max_tokens=16000 before completion. https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/2000/01/rdf-schema#label Claude Code session: retrieval, compilation, axiom audit, grounding, and nanopublication drafting https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#generated https://provenance.example/tarski-lean/activity-ground https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#generated https://provenance.example/tarski-lean/activity-negative-space https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#generated https://provenance.example/tarski-lean/activity-retrieve-execute https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#generated https://provenance.example/tarski-lean/activity-separate https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-investigation https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-software https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-validation https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-writing https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#wasAssociatedWith https://provenance.example/tarski-lean/agent-claude-sonnet-5 https://provenance.example/tarski-lean/activity-claude-code-session http://www.w3.org/ns/prov#wasInformedBy https://provenance.example/tarski-lean/activity-bare-api-attempt https://provenance.example/tarski-lean/activity-request http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://provenance.example/tarski-lean/activity-request http://www.w3.org/2000/01/rdf-schema#label User specifies the five-step provenance protocol and, on request, the repo URL for Tarski.lean https://provenance.example/tarski-lean/activity-request http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-request-conceptualization https://provenance.example/tarski-lean/activity-request http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-request-supervision https://provenance.example/tarski-lean/activity-request http://www.w3.org/ns/prov#wasAssociatedWith https://provenance.example/tarski-lean/agent-user https://provenance.example/tarski-lean/activity-user-review http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Activity https://provenance.example/tarski-lean/activity-user-review http://www.w3.org/2000/01/rdf-schema#label User reviews NP-A through NP-E before any signing or publication https://provenance.example/tarski-lean/activity-user-review http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-review-supervision https://provenance.example/tarski-lean/activity-user-review http://www.w3.org/ns/prov#wasAssociatedWith https://provenance.example/tarski-lean/agent-user https://provenance.example/tarski-lean/activity-user-review https://provenance.example/tarski-lean/status Pending at the time NP-E was drafted -- this activity node is declared in advance of its own completion, and its outcome (approved / revised / rejected) is not yet an assertable fact. See NP-D for the general rule that unsigned, unpublished status holds for this entire set. https://provenance.example/tarski-lean/agent-claude-bare-api http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#SoftwareAgent https://provenance.example/tarski-lean/agent-claude-bare-api http://www.w3.org/2000/01/rdf-schema#label Claude Sonnet 5 (Anthropic Messages API, no tools) https://provenance.example/tarski-lean/agent-claude-bare-api https://provenance.example/tarski-lean/hasCapability text generation only -- no file access, no shell, no network fetch, no Lean toolchain https://provenance.example/tarski-lean/agent-claude-sonnet-5 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#SoftwareAgent https://provenance.example/tarski-lean/agent-claude-sonnet-5 http://www.w3.org/2000/01/rdf-schema#label Claude Sonnet 5 (Anthropic), running as Claude Code https://provenance.example/tarski-lean/agent-claude-sonnet-5 https://provenance.example/tarski-lean/hasCapability Bash, file read/write, WebSearch, and an installed elan/Lean 4.32.0 toolchain https://provenance.example/tarski-lean/agent-user http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Person https://provenance.example/tarski-lean/agent-user http://www.w3.org/2000/01/rdf-schema#label Myles Axton https://provenance.example/tarski-lean/agent-user http://www.w3.org/ns/prov#actedOnBehalfOf https://orcid.org/0000-0002-8042-4131 https://provenance.example/tarski-lean/agent-user http://xmlns.com/foaf/0.1/name Myles Axton https://provenance.example/tarski-lean/attr-bare-api-validation http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://provenance.example/tarski-lean/attr-bare-api-validation http://www.w3.org/ns/prov#agent https://provenance.example/tarski-lean/agent-claude-bare-api https://provenance.example/tarski-lean/attr-bare-api-validation http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/validation https://provenance.example/tarski-lean/attr-request-conceptualization http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://provenance.example/tarski-lean/attr-request-conceptualization http://www.w3.org/ns/prov#agent https://provenance.example/tarski-lean/agent-user https://provenance.example/tarski-lean/attr-request-conceptualization http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/conceptualization https://provenance.example/tarski-lean/attr-request-supervision http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://provenance.example/tarski-lean/attr-request-supervision http://www.w3.org/ns/prov#agent https://provenance.example/tarski-lean/agent-user https://provenance.example/tarski-lean/attr-request-supervision http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/supervision https://provenance.example/tarski-lean/attr-review-supervision http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://provenance.example/tarski-lean/attr-review-supervision http://www.w3.org/ns/prov#agent https://provenance.example/tarski-lean/agent-user https://provenance.example/tarski-lean/attr-review-supervision http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/supervision https://provenance.example/tarski-lean/attr-session-investigation http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://provenance.example/tarski-lean/attr-session-investigation http://www.w3.org/ns/prov#agent https://provenance.example/tarski-lean/agent-claude-sonnet-5 https://provenance.example/tarski-lean/attr-session-investigation http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/investigation https://provenance.example/tarski-lean/attr-session-software http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://provenance.example/tarski-lean/attr-session-software http://www.w3.org/ns/prov#agent https://provenance.example/tarski-lean/agent-claude-sonnet-5 https://provenance.example/tarski-lean/attr-session-software http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/software https://provenance.example/tarski-lean/attr-session-validation http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://provenance.example/tarski-lean/attr-session-validation http://www.w3.org/ns/prov#agent https://provenance.example/tarski-lean/agent-claude-sonnet-5 https://provenance.example/tarski-lean/attr-session-validation http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/validation https://provenance.example/tarski-lean/attr-session-writing http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Attribution https://provenance.example/tarski-lean/attr-session-writing http://www.w3.org/ns/prov#agent https://provenance.example/tarski-lean/agent-claude-sonnet-5 https://provenance.example/tarski-lean/attr-session-writing http://www.w3.org/ns/prov#hadRole https://credit.niso.org/contributor-roles/writing-original-draft https://provenance.example/tarski-lean/claim-set-np-a http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/ClaimSet https://provenance.example/tarski-lean/claim-set-np-a http://www.w3.org/2000/01/rdf-schema#label NP-A (machine-verified): hashing, ISCC, compilation, axiom audit https://provenance.example/tarski-lean/claim-set-np-a http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-investigation https://provenance.example/tarski-lean/claim-set-np-a http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-software https://provenance.example/tarski-lean/claim-set-np-a http://www.w3.org/ns/prov#wasGeneratedBy https://provenance.example/tarski-lean/activity-retrieve-execute https://provenance.example/tarski-lean/claim-set-np-b http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/ClaimSet https://provenance.example/tarski-lean/claim-set-np-b http://www.w3.org/2000/01/rdf-schema#label NP-B (source-verified): license, authorship, historical citations, concordance spot-check https://provenance.example/tarski-lean/claim-set-np-b http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-investigation https://provenance.example/tarski-lean/claim-set-np-b http://www.w3.org/ns/prov#wasGeneratedBy https://provenance.example/tarski-lean/activity-ground https://provenance.example/tarski-lean/claim-set-np-c http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/ClaimSet https://provenance.example/tarski-lean/claim-set-np-c http://www.w3.org/2000/01/rdf-schema#label NP-C (asserted): self-reported claims quoted but not independently verified https://provenance.example/tarski-lean/claim-set-np-c http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-writing https://provenance.example/tarski-lean/claim-set-np-c http://www.w3.org/ns/prov#wasGeneratedBy https://provenance.example/tarski-lean/activity-separate https://provenance.example/tarski-lean/claim-set-np-d http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/ClaimSet https://provenance.example/tarski-lean/claim-set-np-d http://www.w3.org/2000/01/rdf-schema#label NP-D (negative space): explicit non-claims https://provenance.example/tarski-lean/claim-set-np-d http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-writing https://provenance.example/tarski-lean/claim-set-np-d http://www.w3.org/ns/prov#wasGeneratedBy https://provenance.example/tarski-lean/activity-negative-space https://provenance.example/tarski-lean/claim-set-np-e http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://provenance.example/tarski-lean/ClaimSet https://provenance.example/tarski-lean/claim-set-np-e http://www.w3.org/2000/01/rdf-schema#label NP-E (this record): the drafting/review provenance graph itself https://provenance.example/tarski-lean/claim-set-np-e http://www.w3.org/ns/prov#qualifiedAttribution https://provenance.example/tarski-lean/attr-session-writing https://provenance.example/tarski-lean/claim-set-np-e http://www.w3.org/ns/prov#wasGeneratedBy https://provenance.example/tarski-lean/activity-claude-code-session https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/provenance https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/assertion http://purl.org/dc/terms/description This graph is a first-person account of the session's own activities and is therefore self-attested by the same agent (d:agent-claude-sonnet-5) that performed them, checked against no external source -- it is provenance about provenance, not a claim about Tarski.lean itself. https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/assertion http://www.w3.org/ns/prov#wasGeneratedBy https://provenance.example/tarski-lean/activity-claude-code-session https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/pubinfo https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM http://purl.org/dc/terms/created 2026-08-10T12:57:30Z https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM http://purl.org/dc/terms/creator https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM http://purl.org/dc/terms/license https://creativecommons.org/licenses/by/4.0/ https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM http://www.w3.org/2000/01/rdf-schema#label Tarski.lean provenance record: drafting and review process (who produced which claim) https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM https://provenance.example/tarski-lean/verificationBucket https://provenance.example/tarski-lean/ProcessProvenance https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEArujXziJVj9wv0856QcQukv3fw7UGog0oDe9ztQ79aozK0giP2f0DvLD1x87SX3o4W/NbRPI4UyMh8HF5NxKQzuo/sgXz96maOF2RyzJq6wa4PMUH7hVO5bB9KT8lmd9FVa9ZCi3aX47ScTAp3xdHwjCG8k+hNfBOMD9/8nxd70FHp55AwUurX4E/LlWKVTrJSPwtJoENaQz1uu5YPv0AdvBuMDcD7ZXMXE6CvO4yEvQamWctKDnwkb8s1L4e4jEWGurRiTSS/zi+Jff8R/c/TZA78JIxMhXJQp/HVOJRC7IJC9cujx/b3UFZbCHUqxWqvckiCxmP9GR9Z95McV780wIDAQAB https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/sig http://purl.org/nanopub/x/hasSignature qwab78tZhOq8DabP7Ncc3dBXVnV6kaE7Mu+SLDzXPzjst4sqUae0C1Y9r7w/en2VffcJfJDuH+jabv89hjNePgSbR6JQ9gKfzv91SpPcYYNrMbnSHIuCgplBhRUFIqtU//1CcOUENNc961wIwlRpJpN8tczSCpJHzYWTj6LfbSlZYUSyTtaXNHbMTesYlK4hrdRRtYny4oiR+y740Fj9mPxdJVJf6V4+YJWSRwJ92wSdQ0kkHkDQQ7+dqmcvRzlLzL0x80lkAOcolVmydXxu9GZqHtLrXh9JT4joI6MwU6q8Asy9ZkEpmFwEhZIvCvzWit9m+I0Tvc3LQj3sIL9avw== https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM https://w3id.org/np/RAeBGiCv6aLdcyxiiejwP2B8uhQbwdNR-OR4YJzSCCOZM/sig http://purl.org/nanopub/x/signedBy https://orcid.org/0000-0002-8042-4131