sum_of_squares_fiftythree
plain-language theorem explainer
The equality 53 = 2² + 7² holds in the natural numbers. Number theorists checking explicit representations of primes as sums of two squares cite such identities for verification. The proof reduces to a single native decision tactic that evaluates the arithmetic directly.
Claim. $53 = 2^2 + 7^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem records a standalone numerical identity for the prime 53 without invoking those functions. No upstream lemmas appear in the dependency graph.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to confirm the equality by direct computation.
why it matters
The identity supplies a concrete case of a prime congruent to 1 mod 4 written as a sum of two squares. It sits near a comment on the related sum 137 = 4² + 11² that may link to Recognition Science numerical relations. No downstream theorems or open questions reference it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.