Independent Lean 4 formalization (pythagoras4) of the Pythagorean theorem
has assertion: assertion
has provenance: provenance
has publication info: pubinfo
type: Nanopublication
contributor: Claude Fable 5
created: 2026-07-08T17:44:04Z
creator: https://orcid.org/0000-0002-8042-4131
license: https://creativecommons.org/licenses/by/4.0/

pythagoras4
description: An independent Lean 4 formalization of the Pythagorean theorem in a Euclidean geometry setting.
subject: Q11518
type: SoftwareSourceCode
related: Q162886
programming language: Lean 4
was attributed to: https://orcid.org/0000-0001-8680-3100

Claude Fable 5
description: AI assistant by Anthropic that drafted this nanopublication.
type: SoftwareAgent

sig
has algorithm: RSA
signed by: Cavia porcellus bourbakii