theorem
proved
repunit_prime_two
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2359.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2356/-! ### Repunit-related primes -/
2357
2358/-- R_2 = 11 is a repunit prime. -/
2359theorem repunit_prime_two : Prime 11 ∧ 11 = (10^2 - 1) / 9 := by native_decide
2360
2361/-- R_19 component: 19 is prime (indexes repunit R_19 which is also prime). -/
2362theorem repunit_index_nineteen : Prime 19 := by native_decide
2363
2364/-- R_23 component: 23 is prime (indexes repunit R_23 which is also prime). -/
2365theorem repunit_index_twentythree : Prime 23 := by native_decide
2366
2367/-- 111 = 3 × 37 is not prime (R_3 factors as 3 × 37, RS-relevant: 37). -/
2368theorem repunit_three_composite : ¬ Prime 111 ∧ 111 = 3 * 37 := by native_decide
2369
2370/-- 1111 = 11 × 101 is not prime (R_4 factors). -/
2371theorem repunit_four_composite : ¬ Prime 1111 ∧ 1111 = 11 * 101 := by native_decide
2372
2373/-- 11111 = 41 × 271 is not prime (R_5 factors). -/
2374theorem repunit_five_composite : ¬ Prime 11111 ∧ 11111 = 41 * 271 := by native_decide
2375
2376/-! ### Wieferich prime candidates -/
2377
2378/-- 1093 is prime (first Wieferich prime). -/
2379theorem prime_onethousandninetythree : Prime 1093 := by native_decide
2380
2381/-- 3511 is prime (second known Wieferich prime). -/
2382theorem prime_threethousandfiveeleven : Prime 3511 := by native_decide
2383
2384-- Note: primeCounting for values > 1000 requires careful verification
2385-- Leaving larger primeCounting values for future sessions
2386
2387/-! ### Primes in the 500s -/
2388
2389/-- 503 is prime. -/