A Reduction of Goldbach's Conjecture to an Auditable Trust Surface: Classical Primitives, Zero Open Analytic Atoms, and a Machine-Checked Envelope
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Summary
We present a reduction of the binary Goldbach conjecture whose entire external dependency surface is explicit, auditable, and machine-checked in Lean 4.
Length
7,975 words
Status
Draft
Target
Journal of Number Theory (research announcement)