Login
Home Users Spaces Query Publish
< 0000-0001-6825-9439
Content Explore

Tarski.lean provenance and credit declaration

https://w3id.org/np/RAXut_tYBIBaf53frjHN9ttCnUj4zq8JhXllSz7MyKpME ⧉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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-claude
agent-claude
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-euclid
agent-euclid
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-geocoq
agent-geocoq
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-gupta
agent-gupta
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-hilbert
agent-hilbert
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-pasch
agent-pasch
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-schwabhaeuser
agent-schwabhaeuser
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-szmielew
agent-szmielew
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-tarski
agent-tarski
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/contributor
contributor
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../agent-user
agent-user
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/relation
relation
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../dedication
dedication
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/dc/terms/tableOfContents
tableOfContents
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../sst-map
sst-map
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/faia/terms/declaration
declaration
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../faia
faia
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../artifact
artifact
http://purl.org/iscc/terms/iscc
iscc
(this is a literal)
"ISCC:PENDING — see sub:isccNote"
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../dedication
dedication
https://schema.org/about
about
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../person-richard-axton
person-richard-axton
.
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../src-geocoq src-geocoq .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../src-sst src-sst .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../agent-claude agent-claude .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../agent-user agent-user .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../artifact artifact .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../agent-claude agent-claude .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../agent-user agent-user .
This is a local identifier that was minted when the nanopublication was created. https://w3id.org/np/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../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/RAXut_tYBI.../activity activity .
This is the identifier for this whole nanopublication. https://w3id.org/np/RAXut_tYBI... 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-18T14:45:07Z"
(xsd:dateTime) .
This is the identifier for this whole nanopublication. https://w3id.org/np/RAXut_tYBI... 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/RAXut_tYBI... 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/RAXut_tYBI... 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/RAXut_tYBI... 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/RAXut_tYBI.../sig
sig
http://purl.org/nanopub/x/hasSignatureTarget has as target This is the identifier for this whole nanopublication. https://w3id.org/np/RAXut_tYBI... this nanopublication .
This is a local identifier minted within the nanopublication. https://w3id.org/np/RAXut_tYBI.../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)