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
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.
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 presents a computer-assisted proof candidate for Sendov's conjecture, reducing a normalized obstruction to exact finite certificates and a uniform large-degree estimate. A separate Lean development checks the exact displayed endpoint Sendov.sendov_conjecture; manuscript-to-formal-statement alignment is not yet reviewed, and ProofAtlas accepted-result review remains pending.
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 checks the exact displayed endpoint Sendov.sendov_conjecture but is not a line-by-line formalization of the manuscript's argument. Manuscript-to-formal-statement alignment is not yet reviewed.
- 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 publication status
Publication review
Accepted-result publication remains pending
Lean has checked the exact source; this public release is not presented as a ProofAtlas accepted result. The linked evidence page shows individual review decisions where they are publicly available. The requirements below describe publication coverage, not a count of unfinished reviews. 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 review question, exact subject coverage, and reviewer provenance recorded for this release. A selected review concerns only its named question and is not by itself proof or acceptance of a broader claim. These bindings alone do not establish that proof or computation checks were rerun.
Download exact review bindings
Public-wording review
- Coverage
- 2 exact subject bindings
- Reviewer
- OpenAI Codex
- Independence
- Independence not asserted
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.