Login
Home Users Spaces Query Publish
< project1
Content Explore

Tarski.lean provenance and credit declaration

https://w3id.org/np/RAZnSuo6CBwVYALiaZ45kg_9T9Oq_EBAKwbSb5SW8iduc ⧉copy

Status: Loading...

📌 Nanopublication

 Tarski.lean provenance and credit declaration comment... approve/disapprove... edit as derived nanopublication... edit as overriding nanopublication... create new with same template...

This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-claude
agent-claude
https://schema.org/name
name
(this is a literal)
"Claude (Anthropic)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-euclid
agent-euclid
http://www.w3.org/ns/prov#hadRole
hadRole
(this is a literal)
"Intellectual ancestor"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-euclid
agent-euclid
https://schema.org/name
name
(this is a literal)
"Euclid of Alexandria (fl. c. 300 BCE)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-geocoq
agent-geocoq
http://www.w3.org/ns/prov#hadRole
hadRole
(this is a literal)
"Formal ancestor"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-gupta
agent-gupta
https://schema.org/name
name
(this is a literal)
"Haragauri Narayan Gupta (1925–2016)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-hilbert
agent-hilbert
http://www.w3.org/ns/prov#hadRole
hadRole
(this is a literal)
"Program architect"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-hilbert
agent-hilbert
https://schema.org/name
name
(this is a literal)
"David Hilbert (1862–1943)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-pasch
agent-pasch
http://www.w3.org/ns/prov#hadRole
hadRole
(this is a literal)
"Axiom source"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-pasch
agent-pasch
https://schema.org/name
name
(this is a literal)
"Moritz Pasch (1843–1930)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-szmielew
agent-szmielew
https://schema.org/name
name
(this is a literal)
"Wanda Szmielew (1918–1976)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-tarski
agent-tarski
http://www.w3.org/ns/prov#hadRole
hadRole
(this is a literal)
"Axiom-system author; metatheorist"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-tarski
agent-tarski
https://schema.org/name
name
(this is a literal)
"Alfred Tarski (1901–1983)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-user
agent-user
https://schema.org/name
name
(this is a literal)
"Myles Axton"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-claude
agent-claude
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-euclid
agent-euclid
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-geocoq
agent-geocoq
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-gupta
agent-gupta
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-hilbert
agent-hilbert
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-pasch
agent-pasch
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-schwabhaeuser
agent-schwabhaeuser
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-szmielew
agent-szmielew
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-tarski
agent-tarski
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../agent-user
agent-user
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/relation
relation
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../dedication
dedication
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/dc/terms/tableOfContents
tableOfContents
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../sst-map
sst-map
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/faia/terms/declaration
declaration
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../faia
faia
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
http://purl.org/iscc/terms/generator
generator
(this is a literal)
"iscc-sdk - v0.9.4"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
https://schema.org/contentSize
contentSize
(this is a literal)
"28435 bytes (648 lines)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
https://schema.org/encodingFormat
encodingFormat
(this is a literal)
"text/plain"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../artifact
artifact
https://schema.org/name
name
(this is a literal)
"Tarski.lean"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../dedication
dedication
https://schema.org/about
about
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../person-richard-axton
person-richard-axton
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../dedication
dedication
https://schema.org/name
name
(this is a literal)
"Dedication"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../faia
faia
http://purl.org/faia/terms/aiContribution
aiContribution
(this is a literal)
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../faia
faia
http://purl.org/faia/terms/mode
mode
(this is a literal)
"AI-drafted, human-directed"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../isccNote
isccNote
http://purl.org/dc/terms/description
description
(this is a literal)
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../isccNote
isccNote
https://schema.org/name
name
(this is a literal)
"ISCC binding status"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../person-richard-axton
person-richard-axton
https://schema.org/name
name
(this is a literal)
"Richard Axton (1941–2021)"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../sst-map
sst-map
https://schema.org/description
description
(this is a literal)
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../sst-map
sst-map
https://schema.org/name
name
(this is a literal)
"Theorem-to-source concordance"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../timestampNote
timestampNote
https://schema.org/name
name
(this is a literal)
"Timestamp status"
.
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity http://purl.org/dc/terms/description description "A single sandboxed chat session beginning from the Pythagorean theorem in Mathlib's inner product spaces (norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero) and EuclideanSpace ℝ (Fin n), pivoting to the synthetic question, and building the Lean 4 artifact over successive turns. Sources were drawn from model memory of SST and GeoCoq; no network access and no Lean toolchain were available, so all proofs were verified by hand-tracing (and, for SST 7.13, by an additional coordinate check) rather than by compilation." .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity http://www.w3.org/ns/prov#endedAtTime endedAtTime "2026-07-19" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity http://www.w3.org/ns/prov#startedAtTime startedAtTime "2026-07-18" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity http://www.w3.org/ns/prov#used used This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity http://www.w3.org/ns/prov#used used This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-geocoq src-geocoq .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity http://www.w3.org/ns/prov#used used This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-sst src-sst .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity http://www.w3.org/ns/prov#wasAssociatedWith wasAssociatedWith This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../agent-claude agent-claude .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity http://www.w3.org/ns/prov#wasAssociatedWith wasAssociatedWith This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../agent-user agent-user .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity https://schema.org/name name "Interactive formalization dialogue" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-iscc activity-iscc http://purl.org/dc/terms/description description "Generated the ISCC-CODE (ISO 24138) for Tarski.lean using iscc-sdk v0.9.4 via a standalone content-identification workflow (iscc-workflow/generate_iscc.py). Fetched the commit-pinned GitHub blob (johnmaxton/lean4-starter @ 90018aec70b2bb8950c1045cac443731825d79ef) and confirmed it is byte-identical (same SHA-256) to the local working copy before generating the code. Because the .lean extension is unrecognized by iscc-sdk's mediatype map, content-based text auto-detection (added to the workflow for this case) was used to process the file as text/plain rather than a raw-bytes fallback." .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-iscc activity-iscc http://www.w3.org/ns/prov#startedAtTime startedAtTime "2026-07-21" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-iscc activity-iscc http://www.w3.org/ns/prov#used used This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../artifact artifact .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-iscc activity-iscc http://www.w3.org/ns/prov#wasAssociatedWith wasAssociatedWith This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../agent-claude agent-claude .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-iscc activity-iscc http://www.w3.org/ns/prov#wasAssociatedWith wasAssociatedWith This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../agent-user agent-user .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-iscc activity-iscc https://schema.org/name name "ISCC-CODE generation" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-verify activity-verify http://purl.org/dc/terms/description description "A follow-up session with a working environment (network access, elan/Lean toolchains). Compiled `lean Tarski.lean` standalone and, separately, built it as a `lake` library target in two projects (pythagoras4, using leanprover/lean4-nightly:nightly-2023-05-16; and lean4-starter, using leanprover/lean4:v4.32.0). Found and fixed one error: the closing `example` used Mathlib's `∃!` notation, unavailable in core Lean 4, rewritten as its explicit unfolding. Both toolchains now build the file with zero errors and zero `sorry`s." .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-verify activity-verify http://www.w3.org/ns/prov#startedAtTime startedAtTime "2026-07-18" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-verify activity-verify http://www.w3.org/ns/prov#used used This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../artifact artifact .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-verify activity-verify http://www.w3.org/ns/prov#wasAssociatedWith wasAssociatedWith This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../agent-claude agent-claude .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-verify activity-verify http://www.w3.org/ns/prov#wasAssociatedWith wasAssociatedWith This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../agent-user agent-user .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity-verify activity-verify https://schema.org/name name "Build, fix, and compilation verification" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation http://purl.org/dc/terms/description description "Full transcript export (36 messages, participants 'Claude (Anthropic PBC)' and the human ORCID holder, per the export's own metadata) of the sandboxed formalization dialogue recorded as sub:activity; the source-of-record for this nanopublication's account of that session, ISCC-identified for tamper-evident reference." .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation http://purl.org/iscc/terms/datahash datahash "1e20ba75fff4f8f4c444367ab1a8b2a6dc174d8594a5e0a608629c783c3672ed9d13" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation http://purl.org/iscc/terms/generator generator "iscc-sdk - v0.9.4" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation http://purl.org/iscc/terms/iscc iscc "ISCC:KACVLHAC56XUUSQOQMH3UGAUADDVMRS5VJT3THHCNW5HL77U7D2MIRA" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation http://purl.org/iscc/terms/metahash metahash "1e203058b6a3e88931d06f05aaf71f1baef07909f330d8d6fa48952fa3a8184e823f" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation https://schema.org/dateCreated dateCreated "2026-07-18T08:47:56Z" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation https://schema.org/dateModified dateModified "2026-07-19T07:51:20Z" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation https://schema.org/encodingFormat encodingFormat "application/json" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-conversation src-conversation https://schema.org/name name "Pythagorean theorem in Lean4 inner product spaces" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-geocoq src-geocoq http://purl.org/dc/terms/description description "Used from model memory as the formalization map; no code consulted or ported in-session." .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-geocoq src-geocoq https://schema.org/name name "GeoCoq repository and papers (Narboux et al., 2006–)" .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-sst src-sst http://purl.org/dc/terms/description description "Used from model memory as the architectural source; not consulted directly in-session." .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../src-sst src-sst https://schema.org/name name "Schwabhäuser, Szmielew, Tarski — Metamathematische Methoden in der Geometrie (Springer, 1983)" .
local:assertion local:assertion http://www.w3.org/ns/prov#wasGeneratedBy wasGeneratedBy This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAZnSuo6CB.../activity activity .
This is the identifier for this whole nanopublication. https://w3id.org/np/RAZnSuo6CB... This nanopublication date and time when the nanopublication was created http://purl.org/dc/terms/created was created on (this is a literal)
"2026-07-21T13:56:27Z"
(xsd:dateTime) .
This is the identifier for this whole nanopublication. https://w3id.org/np/RAZnSuo6CB... This nanopublication links to the assertion template that was used to create this nanopublication https://w3id.org/np/o/ntemplate/wasCreatedFromTemplate was created from the assertion template http://purl.org/np/RAFu2BNmgH...
RAFu2BNmgH
.
This is the identifier for this whole nanopublication. https://w3id.org/np/RAZnSuo6CB... This nanopublication links to the provenance template that was used to create this nanopublication https://w3id.org/np/o/ntemplate/wasCreatedFromProvenanceTemplate was created from the provenance template http://purl.org/np/RANwQa4ICW...
RANwQa4ICW
.
This is the identifier for this whole nanopublication. https://w3id.org/np/RAZnSuo6CB... This nanopublication links to the publication info template that was used to create this nanopublication https://w3id.org/np/o/ntemplate/wasCreatedFromPubinfoTemplate was created from the publication info template http://purl.org/np/RAA2MfqdBC...
RAA2MfqdBC
.
This is the identifier for this whole nanopublication. https://w3id.org/np/RAZnSuo6CB... This nanopublication links to the publication info template that was used to create this nanopublication https://w3id.org/np/o/ntemplate/wasCreatedFromPubinfoTemplate was created from the publication info template http://purl.org/np/RAjpBMlw3o...
RAjpBMlw3o
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../sig
sig
http://purl.org/nanopub/x/hasSignatureTarget has as target This is the identifier for this whole nanopublication. https://w3id.org/np/RAZnSuo6CB... this nanopublication .
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAZnSuo6CB.../sig
sig
http://purl.org/nanopub/x/hasAlgorithm has the algorithm (this is a literal)
"RSA"
.

Myles Axton,

Raw formats

Full nanopublication: TriG(txt), JSON-LD(txt), N-Quads(txt), XML(txt)

Assertions only: Turtle(txt), JSON-LD(txt), N-Triples(txt), RDF/XML(txt)