Immutable source snapshot
Sendov's Conjecture source at f8b71644c02b
This permanent route identifies the exact Git snapshot used by the recorded Lean theorem. The complete checked import closure, source footprint, downloads, and checker evidence are available on the source page.
Git commitf8b71644c02bf16d8e9f7e183428ac2d4b0f6bf1
Recorded theorem endpoint
Sendov.sendov_conjecture
The submitted Lean package checks Sendov.sendov_conjecture: for a nonzero complex polynomial of degree at least two whose zeros lie in the closed unit disk, every zero lies within distance 1 of a critical point. Its relationship to the informal Sendov conjecture is not yet reviewed, and ProofAtlas accepted-result review remains pending.