rows {
  options {
    physical_type: PHYSICAL_STREAM_TYPE_QUADS
    max_name_table_size: 128
    max_prefix_table_size: 16
    max_datatype_table_size: 16
    logical_type: LOGICAL_STREAM_TYPE_DATASETS
    version: 2
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/"
  }
}
rows {
  name {
    value: "RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q"
  }
}
rows {
  namespace {
    name: "this"
    value {
      prefix_id: 1
    }
  }
}
rows {
  prefix {
    value: "https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/"
  }
}
rows {
  name {
  }
}
rows {
  namespace {
    name: "sub"
    value {
      prefix_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://schema.org/"
  }
}
rows {
  namespace {
    name: "schema"
    value {
      prefix_id: 3
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.nanopub.org/nschema#"
  }
}
rows {
  namespace {
    name: "np"
    value {
      prefix_id: 4
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://purl.org/dc/terms/"
  }
}
rows {
  namespace {
    name: "dct"
    value {
      prefix_id: 5
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/2001/XMLSchema#"
  }
}
rows {
  namespace {
    name: "xsd"
    value {
      prefix_id: 6
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/2004/02/skos/core#"
  }
}
rows {
  namespace {
    name: "skos"
    value {
      prefix_id: 7
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/2000/01/rdf-schema#"
  }
}
rows {
  namespace {
    name: "rdfs"
    value {
      prefix_id: 8
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "https://orcid.org/"
  }
}
rows {
  namespace {
    name: "orcid"
    value {
      prefix_id: 9
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/ns/prov#"
  }
}
rows {
  namespace {
    name: "prov"
    value {
      prefix_id: 10
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.wikidata.org/entity/"
  }
}
rows {
  namespace {
    name: "wd"
    value {
      prefix_id: 11
      name_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://purl.org/nanopub/x/"
  }
}
rows {
  namespace {
    name: "npx"
    value {
      prefix_id: 12
      name_id: 2
    }
  }
}
rows {
  name {
    value: "hasAssertion"
  }
}
rows {
  name {
    value: "assertion"
  }
}
rows {
  name {
    value: "Head"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 1
      name_id: 1
    }
    p_iri {
      prefix_id: 4
      name_id: 3
    }
    o_iri {
      prefix_id: 2
    }
    g_iri {
    }
  }
}
rows {
  name {
    value: "hasProvenance"
  }
}
rows {
  name {
    value: "provenance"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 4
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  name {
    value: "hasPublicationInfo"
  }
}
rows {
  name {
    value: "pubinfo"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 4
    }
    o_iri {
      prefix_id: 2
    }
  }
}
rows {
  prefix {
    value: "http://www.w3.org/1999/02/22-rdf-syntax-ns#"
  }
}
rows {
  name {
    value: "type"
  }
}
rows {
  name {
    value: "Nanopublication"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 13
    }
    o_iri {
      prefix_id: 4
    }
  }
}
rows {
  name {
    value: "mathlib-formalization"
  }
}
rows {
  name {
    value: "description"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
    }
    p_iri {
      prefix_id: 5
    }
    o_literal {
      lex: "Machine-verified Lean 4 formalization of the Pythagorean theorem in Mathlib, stated in if-and-only-if angle-at-point form: dist p\342\202\201 p\342\202\203 * dist p\342\202\201 p\342\202\203 = dist p\342\202\201 p\342\202\202 * dist p\342\202\201 p\342\202\202 + dist p\342\202\203 p\342\202\202 * dist p\342\202\203 p\342\202\202 \342\206\224 angle p\342\202\201 p\342\202\202 p\342\202\203 = \317\200/2. Proved for points of a metric space that is a torsor over a real inner product space (Euclidean affine space)."
      langtag: "en"
    }
    g_iri {
      prefix_id: 2
      name_id: 4
    }
  }
}
rows {
  name {
    value: "isPartOf"
  }
}
rows {
  prefix {
    value: "https://github.com/leanprover-community/"
  }
}
rows {
  name {
    value: "mathlib4"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 14
    }
    o_iri {
      prefix_id: 14
    }
  }
}
rows {
  name {
    value: "subject"
  }
}
rows {
  name {
    value: "Q11518"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
    }
    o_iri {
      prefix_id: 11
    }
  }
}
rows {
  name {
    value: "SoftwareSourceCode"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 13
      name_id: 10
    }
    o_iri {
      prefix_id: 3
      name_id: 18
    }
  }
}
rows {
  name {
    value: "label"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 8
    }
    o_literal {
      lex: "EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two"
    }
  }
}
rows {
  name {
    value: "seeAlso"
  }
}
rows {
  prefix {
    value: "https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.html#"
  }
}
rows {
  name {
    value: "EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 15
    }
  }
}
rows {
  name {
    value: "related"
  }
}
rows {
  name {
    value: "Q162886"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 7
    }
    o_iri {
      prefix_id: 11
    }
  }
}
rows {
  name {
    value: "Q214159"
  }
}
rows {
  quad {
    o_iri {
    }
  }
}
rows {
  name {
    value: "programmingLanguage"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 3
    }
    o_literal {
      lex: "Lean 4"
    }
  }
}
rows {
  name {
    value: "wasAttributedTo"
  }
}
rows {
  name {
    value: "0000-0002-8042-4131"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 4
    }
    p_iri {
      prefix_id: 10
      name_id: 26
    }
    o_iri {
      prefix_id: 9
    }
    g_iri {
      prefix_id: 2
      name_id: 7
    }
  }
}
rows {
  name {
    value: "wasDerivedFrom"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 10
      name_id: 28
    }
    o_iri {
      prefix_id: 14
      name_id: 15
    }
  }
}
rows {
  prefix {
    value: "https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Euclidean/Angle/Unoriented/"
  }
}
rows {
  name {
    value: "RightAngle.html"
  }
}
rows {
  quad {
    o_iri {
      prefix_id: 16
      name_id: 29
    }
  }
}
rows {
  name {
    value: "contributor"
  }
}
rows {
  name {
    value: "claude-fable-5"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 1
      name_id: 1
    }
    p_iri {
      prefix_id: 5
      name_id: 30
    }
    o_iri {
      prefix_id: 2
    }
    g_iri {
      name_id: 9
    }
  }
}
rows {
  name {
    value: "created"
  }
}
rows {
  datatype {
    value: "http://www.w3.org/2001/XMLSchema#dateTime"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 32
    }
    o_literal {
      lex: "2026-07-08T17:44:04Z"
      datatype: 1
    }
  }
}
rows {
  name {
    value: "creator"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 9
      name_id: 27
    }
  }
}
rows {
  name {
    value: "license"
  }
}
rows {
  prefix {
    id: 6
    value: "https://creativecommons.org/licenses/by/4.0/"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 5
      name_id: 34
    }
    o_iri {
      prefix_id: 6
      name_id: 2
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 8
      name_id: 19
    }
    o_literal {
      lex: "Lean 4 Mathlib formalization of the Pythagorean theorem"
    }
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 31
    }
    p_iri {
      prefix_id: 5
      name_id: 13
    }
    o_literal {
      lex: "AI assistant by Anthropic that drafted this nanopublication."
      langtag: "en"
    }
  }
}
rows {
  name {
    value: "SoftwareAgent"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 13
      name_id: 10
    }
    o_iri {
      prefix_id: 10
      name_id: 35
    }
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 8
      name_id: 19
    }
    o_literal {
      lex: "Claude Fable 5"
    }
  }
}
rows {
  name {
    value: "sig"
  }
}
rows {
  name {
    value: "hasAlgorithm"
  }
}
rows {
  quad {
    s_iri {
      prefix_id: 2
      name_id: 36
    }
    p_iri {
      prefix_id: 12
    }
    o_literal {
      lex: "RSA"
    }
  }
}
rows {
  name {
    value: "hasPublicKey"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAuf45jeLY8du2mdR9Nnr5u0VQC/Ry6wLMP4lGDZo7h5LMKigj2yOeeygfVuFKaaRl5QVvKaMn3VlZRTF14vIWPmP2gEjKsm5ItK0Ii58vh3CkqNLjSfUGreD/jLxvMRS9Urz3FBNy/fTFbK8OovkJLY84XrjTQCH0Z0ZxOXQT9msVYSMAtkA2pZVavwoMc9HFH7lixDHRgn2N8PiAzmvdKozaeFrwI6VykmJahdYGBg+o9fgCPtDSfvfJTEumUkNyRxnlj7U5g7Tq1KK4yWjPHbwQLoZSUwH/KR6pN7QD9sjUOZYRZehnUmn5GrEi17hZPZLisx0mzkmQV7Z/TPhNoQIDAQAB"
    }
  }
}
rows {
  name {
    value: "hasSignature"
  }
}
rows {
  quad {
    p_iri {
    }
    o_literal {
      lex: "Laaccg+S8tF1wsaPc3nkaiaVSSa+ZZHBTm0WRVTYW7sJ/obnPg4kiIsIRj4SqaRosQ0YFK3TkmIFCw5mPTmsMetBb5NsQPeOQFho03IAfsd2d9xkP5+hJv7LEKuSiYemyQM3HR3cfkKTWVzDovWtkIjp/xnN22vGMKITAcYbJIoDUooRMKvUMsNrZSg4dttc4ab+2rhyfJtWBCbcRrSl/ZOlNvRZenpgiuXb6YOGzYm+ZYF9RPxKn2x4QGehUZzQX8tXJEs33lZVL2RDwVDEey1WGu/NbsuDjf4FnPayg/vsLR/uwluU6mKuav4jmkcL4qUuAY9IjDgRjaMeTL4Fpg=="
    }
  }
}
rows {
  name {
    value: "hasSignatureTarget"
  }
}
rows {
  quad {
    p_iri {
    }
    o_iri {
      prefix_id: 1
      name_id: 1
    }
  }
}
rows {
  name {
    value: "signedBy"
  }
}
rows {
  prefix {
    id: 4
    value: "https://w3id.org/np/RA2cLvTWQp8S1kkViFTLE2tWK2b7lBieP2Mc2_qTX7Woo/"
  }
}
rows {
  name {
    value: "Cavia_porcellus_bourbakii"
  }
}
rows {
  quad {
    p_iri {
      prefix_id: 12
      name_id: 41
    }
    o_iri {
      prefix_id: 4
    }
  }
}