An independent Lean 4 formalization of the Pythagorean theorem in a Euclidean geometry setting.
Independent Lean 4 formalization (pythagoras4) of the Pythagorean theorem
AI assistant by Anthropic that drafted this nanopublication.