theorem
proved
twin_prime_fourhundredsixtyone_fourhundredsixtythree
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 2622.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2619theorem twin_prime_fourhundredthirtyone_fourhundredthirtythree : Prime 431 ∧ Prime 433 ∧ 433 = 431 + 2 := by native_decide
2620
2621/-- (461, 463) is a twin prime pair. -/
2622theorem twin_prime_fourhundredsixtyone_fourhundredsixtythree : Prime 461 ∧ Prime 463 ∧ 463 = 461 + 2 := by native_decide
2623
2624/-! ### Primes in the 600s -/
2625
2626/-- 601 is prime. -/
2627theorem prime_sixhundredone : Prime 601 := by native_decide
2628
2629/-- 607 is prime. -/
2630theorem prime_sixhundredseven : Prime 607 := by native_decide
2631
2632/-- 613 is prime. -/
2633theorem prime_sixhundredthirteen : Prime 613 := by native_decide
2634
2635/-- 617 is prime. -/
2636theorem prime_sixhundredseventeen : Prime 617 := by native_decide
2637
2638/-- 619 is prime. -/
2639theorem prime_sixhundrednineteen : Prime 619 := by native_decide
2640
2641/-- 631 is prime. -/
2642theorem prime_sixhundredthirtyone : Prime 631 := by native_decide
2643
2644/-- 641 is prime (Fermat prime related: divides F₅). -/
2645theorem prime_sixhundredfortyone : Prime 641 := by native_decide
2646
2647/-- 643 is prime. -/
2648theorem prime_sixhundredfortythree : Prime 643 := by native_decide
2649
2650/-- 647 is prime. -/
2651theorem prime_sixhundredfortyseven : Prime 647 := by native_decide
2652