Commit 2025-10-15 16:18 97ffe6c2
View on Github →feat(NumberTheory/SumTwoSquares): it is decidable whether a number is the sum of two squares (#30273)
Add a Decidable instance for the already proven theorem of being the sum of two squares.
Try #eval Finset.range 50 |>.filter (∃ x y, · = x ^ 2 + y ^ 2)