<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://www.nanopub.org/nschema#hasAssertion> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/Head> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://www.nanopub.org/nschema#hasProvenance> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/provenance> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/Head> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://www.nanopub.org/nschema#hasPublicationInfo> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/Head> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://www.nanopub.org/nschema#Nanopublication> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/Head> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <http://purl.org/dc/terms/description> "Machine-verified Lean 4 formalization of the Pythagorean theorem in Mathlib, stated in if-and-only-if angle-at-point form: dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ angle p₁ p₂ p₃ = π/2. Proved for points of a metric space that is a torsor over a real inner product space (Euclidean affine space)."@en <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <http://purl.org/dc/terms/isPartOf> <https://github.com/leanprover-community/mathlib4> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <http://purl.org/dc/terms/subject> <http://www.wikidata.org/entity/Q11518> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://schema.org/SoftwareSourceCode> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <http://www.w3.org/2000/01/rdf-schema#label> "EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two" <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <http://www.w3.org/2000/01/rdf-schema#seeAlso> <https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.html#EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <http://www.w3.org/2004/02/skos/core#related> <http://www.wikidata.org/entity/Q162886> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <http://www.w3.org/2004/02/skos/core#related> <http://www.wikidata.org/entity/Q214159> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/mathlib-formalization> <https://schema.org/programmingLanguage> "Lean 4" <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> <http://www.w3.org/ns/prov#wasAttributedTo> <https://orcid.org/0000-0002-8042-4131> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/provenance> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> <http://www.w3.org/ns/prov#wasDerivedFrom> <https://github.com/leanprover-community/mathlib4> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/provenance> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/assertion> <http://www.w3.org/ns/prov#wasDerivedFrom> <https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.html> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/provenance> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://purl.org/dc/terms/contributor> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/claude-fable-5> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://purl.org/dc/terms/created> "2026-07-08T17:44:04Z"^^<http://www.w3.org/2001/XMLSchema#dateTime> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://purl.org/dc/terms/creator> <https://orcid.org/0000-0002-8042-4131> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://purl.org/dc/terms/license> <https://creativecommons.org/licenses/by/4.0/> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <http://www.w3.org/2000/01/rdf-schema#label> "Lean 4 Mathlib formalization of the Pythagorean theorem" <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/claude-fable-5> <http://purl.org/dc/terms/description> "AI assistant by Anthropic that drafted this nanopublication."@en <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/claude-fable-5> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://www.w3.org/ns/prov#SoftwareAgent> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/claude-fable-5> <http://www.w3.org/2000/01/rdf-schema#label> "Claude Fable 5" <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/sig> <http://purl.org/nanopub/x/hasAlgorithm> "RSA" <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/sig> <http://purl.org/nanopub/x/hasPublicKey> "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAuf45jeLY8du2mdR9Nnr5u0VQC/Ry6wLMP4lGDZo7h5LMKigj2yOeeygfVuFKaaRl5QVvKaMn3VlZRTF14vIWPmP2gEjKsm5ItK0Ii58vh3CkqNLjSfUGreD/jLxvMRS9Urz3FBNy/fTFbK8OovkJLY84XrjTQCH0Z0ZxOXQT9msVYSMAtkA2pZVavwoMc9HFH7lixDHRgn2N8PiAzmvdKozaeFrwI6VykmJahdYGBg+o9fgCPtDSfvfJTEumUkNyRxnlj7U5g7Tq1KK4yWjPHbwQLoZSUwH/KR6pN7QD9sjUOZYRZehnUmn5GrEi17hZPZLisx0mzkmQV7Z/TPhNoQIDAQAB" <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/sig> <http://purl.org/nanopub/x/hasSignature> "Laaccg+S8tF1wsaPc3nkaiaVSSa+ZZHBTm0WRVTYW7sJ/obnPg4kiIsIRj4SqaRosQ0YFK3TkmIFCw5mPTmsMetBb5NsQPeOQFho03IAfsd2d9xkP5+hJv7LEKuSiYemyQM3HR3cfkKTWVzDovWtkIjp/xnN22vGMKITAcYbJIoDUooRMKvUMsNrZSg4dttc4ab+2rhyfJtWBCbcRrSl/ZOlNvRZenpgiuXb6YOGzYm+ZYF9RPxKn2x4QGehUZzQX8tXJEs33lZVL2RDwVDEey1WGu/NbsuDjf4FnPayg/vsLR/uwluU6mKuav4jmkcL4qUuAY9IjDgRjaMeTL4Fpg==" <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/sig> <http://purl.org/nanopub/x/hasSignatureTarget> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .
<https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/sig> <http://purl.org/nanopub/x/signedBy> <https://w3id.org/np/RA2cLvTWQp8S1kkViFTLE2tWK2b7lBieP2Mc2_qTX7Woo/Cavia_porcellus_bourbakii> <https://w3id.org/np/RAoekRBLxdNKjYD2dIgqZk4RtGdf76LE8ncIbXSgKmO4Q/pubinfo> .