theorem
proved
prime_threethousandfiveeleven
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2382.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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. -/
2390theorem prime_fivehundredthree : Prime 503 := by native_decide
2391
2392/-- 509 is prime. -/
2393theorem prime_fivehundrednine : Prime 509 := by native_decide
2394
2395/-- 521 is prime. -/
2396theorem prime_fivehundredtwentyone : Prime 521 := by native_decide
2397
2398/-- 523 is prime. -/
2399theorem prime_fivehundredtwentythree : Prime 523 := by native_decide
2400
2401/-- 541 is prime. -/
2402theorem prime_fivehundredfortyone : Prime 541 := by native_decide
2403
2404/-- 547 is prime. -/
2405theorem prime_fivehundredfortyseven : Prime 547 := by native_decide
2406
2407/-- 557 is prime. -/
2408theorem prime_fivehundredfiftyseven : Prime 557 := by native_decide
2409
2410/-- 563 is prime (Wilson prime). -/
2411theorem prime_fivehundredsixtythree : Prime 563 := by native_decide
2412