https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/Head https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/assertion https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/provenance https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pubinfo https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/assertion https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pythagoras4-formalization http://purl.org/dc/terms/description An independent Lean 4 formalization of the Pythagorean theorem in a Euclidean geometry setting. https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pythagoras4-formalization http://purl.org/dc/terms/subject http://www.wikidata.org/entity/Q11518 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pythagoras4-formalization http://www.w3.org/1999/02/22-rdf-syntax-ns#type https://schema.org/SoftwareSourceCode https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pythagoras4-formalization http://www.w3.org/2000/01/rdf-schema#label pythagoras4 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pythagoras4-formalization http://www.w3.org/2000/01/rdf-schema#seeAlso https://github.com/ianjauslin-rutgers/pythagoras4 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pythagoras4-formalization http://www.w3.org/2004/02/skos/core#related http://www.wikidata.org/entity/Q162886 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pythagoras4-formalization https://schema.org/programmingLanguage Lean 4 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/provenance https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/assertion http://www.w3.org/ns/prov#wasAttributedTo https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://github.com/ianjauslin-rutgers/pythagoras4 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pythagoras4-formalization http://www.w3.org/ns/prov#wasAttributedTo https://orcid.org/0000-0001-8680-3100 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/pubinfo https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://purl.org/dc/terms/contributor https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/claude-fable-5 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://purl.org/dc/terms/created 2026-07-08T17:44:04Z https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://purl.org/dc/terms/creator https://orcid.org/0000-0002-8042-4131 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://purl.org/dc/terms/license https://creativecommons.org/licenses/by/4.0/ https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ http://www.w3.org/2000/01/rdf-schema#label Independent Lean 4 formalization (pythagoras4) of the Pythagorean theorem https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/claude-fable-5 http://purl.org/dc/terms/description AI assistant by Anthropic that drafted this nanopublication. https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/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/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/claude-fable-5 http://www.w3.org/2000/01/rdf-schema#label Claude Fable 5 https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAuf45jeLY8du2mdR9Nnr5u0VQC/Ry6wLMP4lGDZo7h5LMKigj2yOeeygfVuFKaaRl5QVvKaMn3VlZRTF14vIWPmP2gEjKsm5ItK0Ii58vh3CkqNLjSfUGreD/jLxvMRS9Urz3FBNy/fTFbK8OovkJLY84XrjTQCH0Z0ZxOXQT9msVYSMAtkA2pZVavwoMc9HFH7lixDHRgn2N8PiAzmvdKozaeFrwI6VykmJahdYGBg+o9fgCPtDSfvfJTEumUkNyRxnlj7U5g7Tq1KK4yWjPHbwQLoZSUwH/KR6pN7QD9sjUOZYRZehnUmn5GrEi17hZPZLisx0mzkmQV7Z/TPhNoQIDAQAB https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/sig http://purl.org/nanopub/x/hasSignature osD3Q71QcDbe8/SNMYsbntdgfF5p9tTZ8lIMm15EDxHRJ53X/N2KJ/spu88Hh72l7xWAc5Au7Wm5SQKfYZNmfRWqisDk7U7gyfmeFjjoKDVCJEO5vAEPH4ozwmLFfFmkPLU9Kw/YR4iVtKy8z3mpC6QtzyJzdynSuXFmUBJof+sYFQHbwMZr6vxI9MGNaOevWyMs9RK5uSO6MmWqejHac1FY7E8QNoWPcUv6r4GtsjNT72L+9PzZi3z1W93vZNr22KeWKHGA/7CNN6Wh2RTX/6Qk3qg6H6qr5l4OkFuUTWix7EaIGYjqi7m6675lLP/N9H3ct1discmhwyafYIkGeA== https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ https://w3id.org/np/RACB5B7C3N2NTXECAuKYCV8PQgMXPpGZYwUDRii5KoZzQ/sig http://purl.org/nanopub/x/signedBy https://w3id.org/np/RA2cLvTWQp8S1kkViFTLE2tWK2b7lBieP2Mc2_qTX7Woo/Cavia_porcellus_bourbakii