Registry · Theorem III.T68 tau-effective formalized

III.T68 — Goldbach Verified to 500

Goldbach verified to 500 via sieve: every even n in [4,500] = p+q with p,q prime.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D102

Lean Formalization

Module: TauLib.BookIII.Spectral.GoldbachDeep

Symbol: goldbach_500