sum_of_squares_thirtyseven
plain-language theorem explainer
The equality 37 = 1² + 6² is recorded as a basic numerical identity. Number theorists examining sums of two squares for primes congruent to 1 mod 4 would reference this fact. The proof reduces to a single native computation that directly evaluates the arithmetic statement.
Claim. $37 = 1^2 + 6^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and its basic properties. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once interfaces stabilize. No upstream lemmas are invoked for this identity.
proof idea
Term-mode proof consisting of a one-line wrapper that applies native_decide to evaluate the equality by direct computation.
why it matters
The result supplies a concrete instance of a prime that is a sum of two squares. It sits among other arithmetic facts in the file and may support later classification of primes or function properties, though no downstream uses are recorded. It touches integer representations that appear in broader number-theoretic scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.