G025 fully proved · constructive factor search · subtraction-free Euclid witnesses · Constructive arithmetic

Infinitely many primes three modulo four

∀B. ∃p q. Prime(p) ∧ B<p ∧ p=4q+3

Eighteen independently checked constructive theorems combine finite factorization, two-square obstructions, a subtraction-free Euclid construction, and actual bounded prime-divisor search to produce arbitrarily large primes congruent to three modulo four.

Open the definition-aware map Read the final theorem See campaign milestone G025

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 467 native tactic lines and 46 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem TF0012 and follow only the lemmas and conservative definitions supporting infinitely_many_primes_three_mod_four.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G025 milestone → theorem and definition dependencies.
Major independently established statements: TF0006 positive_number_with_admissible_prime_divisors_is_two_square · TF000D three_mod_four_prime_divisor_exists · TF000F euclid_three_progression_prime_exists · TF0011 euclid_three_prime_divisor_exceeds_bound · TF0012 infinitely_many_primes_three_mod_four.
Independently verified Alpha v34 checked-use theorem family: 18 dependency-curried kernel-checked theorem bodies · 46 proof prerequisites · 11 linked definitions · 9 definition-dependency arrows · 467 exact tactic lines · first admitted v23 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 617 bundle nodes; SHA-256 cc0051da2cac31e382c79223999d448a1119f62aa448f1c7f68a6b9c3edf9d11.
Exact mathematical boundary: The exact G025 progression-prime milestone is fully proved in unchanged constructive arithmetic; Mod4Three deliberately reuses its existing Quadratic Reciprocity definition PD0012. The much stronger full Dirichlet progression-prime milestone G030 remains open.