Formal evidence
An independent reviewer must inspect the recorded build, declarations, unfinished-proof-step check, and disclosed foundations.
ProofAtlas research case study
Starting frontierLongstanding Sendov conjecture→AI-developed Lean-checked candidateProof manuscript + complete Lean package
Evidence and status →Complex analysis · formal theorem
Sendov's Conjecture
A complete Lean formalization of Sendov's conjecture: every zero of a nonzero complex polynomial of degree at least two, with all zeros in the closed unit disk, lies within distance one of a zero of the derivative.
Scope: For every nonzero complex polynomial p of degree at least two whose zeros all lie in the closed unit disk, and for every zero a of p, there exists a zero w of p' with ‖w − a‖ ≤ 1.
Lean checkedRecorded build passed
Unfinished proof stepsNone
PublicationReview pending
Exact formal proposition
Hypotheses and conclusion
theorem sendov_conjecture : SendovConjectureResult boundary
What this theorem does—and does not—establish
For every nonzero complex polynomial p of degree at least two whose zeros all lie in the closed unit disk, and for every zero a of p, there exists a zero w of p' with ‖w − a‖ ≤ 1.
- No historical priority or first-proof claim is made.
- The Lean development is not a line-by-line formalization of the manuscript.
- Lean does not verify the manuscript's supplementary Python programs.
- The current ProofAtlas evidence record retains a source-supplied successful build and axiom audit but not the complete command/output transcript required for accepted-result status.
- The disclosed Lean foundations are standard logical foundations, not assumptions of Sendov's conjecture.
Companion research paper
A Computer-Assisted Proof of Sendov's Conjecture
The August 5 manuscript develops a computer-assisted proof of Sendov's conjecture, reducing a normalized obstruction to exact finite certificates and a uniform large-degree estimate. A separate Lean development proves the same theorem through a streamlined formal route.
Author-authorized early release. This fixed paper package first appeared while independent presentation review was pending; hosting it does not mark the Lean result accepted.
Paper, rights, and source relationship
Hosting authorized by the rightsholder. Original ProofAtlas metadata cover; not a reproduction of a paper page.
Lech Mazur, “A Computer-Assisted Proof of Sendov's Conjecture,” 5 August 2026.
- The Lean development proves the same public Sendov proposition but is not a line-by-line formalization of the manuscript's argument.
- Lean does not verify the supplementary Python programs. Those programs certify two terminal scalar propositions used by the manuscript, not every preceding analytic reduction.
- The submitted Lean audit reports a successful rehash build, no unfinished proof commands, and the standard foundation closure propext, Classical.choice, and Quot.sound. ProofAtlas accepted-result status remains separate because the retained audit is a summary rather than the complete build transcript required by the current evidence contract.
- The title is the manuscript's bibliographic title; this package makes no historical priority or first-proof claim.
Paper overview
Sendov's conjecture: theorem, milestones, and proof assets
Author-supplied overview of the manuscript's theorem claim, historical milestones, and proof assets. ProofAtlas separately labels the Lean formalization's publication review as pending.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
Open questions and extensions
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
What the source ZIP contains
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Formal theorem review status — 4 questions open
Independent review
Four review questions remain open
Lean has checked the exact source, but ProofAtlas has not accepted this result. Independent AI, human, or mixed reviewers may examine the build evidence, statement alignment, result boundary, and public wording. Review does not replace Lean's check or broaden the theorem.
Statement alignment
The formal declaration must be reviewed against the theorem wording and its exact variant.
Result boundary
The limits must be checked so the page cannot imply a broader theorem.
Public wording
The explanation, infographic labels, and source presentation need independent review.
Canonical source
The permanent source link and downloadable files must be approved for public citation.
Accepted result
After the four reviews and source route are ready, an accepted-result record must bind them to this exact formalization.
Credit for this release
Contributors and roles
Authorship and other contributions are recorded separately for this version.
Contributions
- Direct contributionOpenAI GPT-5.6 Pro
OpenAI GPT-5.6 Pro contributed to exploration, proof development, exact computational testing, adversarial auditing, and exposition.
- Computation
- Exposition
- Gap or error discovery
- Proof strategy
- Direct contributionLech Mazur
Lech Mazur is the sole named manuscript author, accountable curator, workflow designer, and reconciler of model outputs.
- Exposition
- Research direction
- Source maintenance
Selected reviews
Review record
Each entry names the question reviewed, its exact scope, and the reviewer provenance recorded for this release.
Download exact review bindings
Routine public-wording review of the exact production presentation.
- Reviewer
- OpenAI Codex
- Independence
- Independence not asserted
Limits of this review
- The backfill report retains the review record's earlier extracted digest; this binding uses the exact current tracked record bytes.
- The lane did not establish formal-evidence, statement-alignment, result-boundary, novelty, specialist-review, or accepted-result status.
Citation
Cite this release
Use the version-specific citation so the authorship, scope, and public record remain attached.
Release history
Versions and public record
- Release
- Paper release
- Version
- public version of 5 August 2026
- Published
- Canonical page
- Open canonical page
Release chronology
This version is part of the release history. No independent external timestamp is claimed.
Scope of this release
- No accepted-result record exists for the Sendov artifact in this snapshot.
- No independent external priority anchor is recorded.
- Specialist novelty review and independent statement-alignment review remain unrecorded.
- The paper, bundle, and supplied infographic are authorized for ProofAtlas distribution but have no general open-content license.