theorem
proved
sum_of_squares_five
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1558.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
1555/-! ### Sum of two squares representations for Pythagorean primes -/
1556
1557/-- 5 = 1² + 2². -/
1558theorem sum_of_squares_five : (5 : ℕ) = 1^2 + 2^2 := by native_decide
1559
1560/-- 13 = 2² + 3². -/
1561theorem sum_of_squares_thirteen : (13 : ℕ) = 2^2 + 3^2 := by native_decide
1562
1563/-- 17 = 1² + 4². -/
1564theorem sum_of_squares_seventeen : (17 : ℕ) = 1^2 + 4^2 := by native_decide
1565
1566/-- 29 = 2² + 5². -/
1567theorem sum_of_squares_twentynine : (29 : ℕ) = 2^2 + 5^2 := by native_decide
1568
1569/-- 37 = 1² + 6². -/
1570theorem sum_of_squares_thirtyseven : (37 : ℕ) = 1^2 + 6^2 := by native_decide
1571
1572/-- 41 = 4² + 5². -/
1573theorem sum_of_squares_fortyone : (41 : ℕ) = 4^2 + 5^2 := by native_decide
1574
1575/-- 53 = 2² + 7². -/
1576theorem sum_of_squares_fiftythree : (53 : ℕ) = 2^2 + 7^2 := by native_decide
1577
1578/-- 137 = 4² + 11² (RS-relevant). -/
1579theorem sum_of_squares_onehundredthirtyseven : (137 : ℕ) = 4^2 + 11^2 := by native_decide
1580
1581/-! ### Prime quadruplets (four primes in close cluster p, p+2, p+6, p+8) -/
1582
1583/-- (5, 7, 11, 13) is a prime quadruplet (gaps: 2, 4, 2). -/
1584theorem prime_quadruplet_five : Prime 5 ∧ Prime 7 ∧ Prime 11 ∧ Prime 13 := by native_decide
1585
1586/-- (11, 13, 17, 19) is a prime quadruplet (gaps: 2, 4, 2). -/
1587theorem prime_quadruplet_eleven : Prime 11 ∧ Prime 13 ∧ Prime 17 ∧ Prime 19 := by native_decide
1588