Research paper

A Simplified Proof Candidate for Sendov's Conjecture with Exact Rational Certificates

Lech Mazur's public Revision 14 presents an all-degree computer-assisted proof candidate for Sendov's conjecture, supported by exact rational terminal certificates and accompanied by an explicit boundary between checked computation and written analysis.

Formal verification is planned, not complete. A formalization is planned, but no completed Lean-checked proof is linked to this publication. Hosting and editorial review do not establish the manuscript's mathematical claims as accepted ProofAtlas results.

The theorem under investigation

Let p be a complex polynomial of degree n ≥ 2 whose zeros all lie in the closed unit disk. Sendov's conjecture says that, for every zero a of p, there is a critical point w satisfying

p′(w) = 0 and |w − a| ≤ 1.

The manuscript presents an all-degree computer-assisted proof candidate for this statement. ProofAtlas is publishing the exact Revision 14 paper and source for scrutiny; this page does not report an accepted resolution of the conjecture.

What Revision 14 contributes

The candidate starts from a hypothetical counterexample and contracts it to a first-contact configuration. It then introduces reciprocal critical coordinates, derives a product-defect inequality, and reduces the polynomial geometry to a scalar parameter. Integration by parts and Maclaurin's inequality lead to a one-variable demand that the final master estimate is designed to contradict.

Revision 14 simplifies and hardens the route described in earlier drafts. Among other changes, it prints the polar-product normalization, makes the mismatch endpoint explicit, defines the exact ceiling predicates used by the verifiers, specifies the deterministic finite partition rule, and expands the envelope regularity argument.

Proof-candidate architecture

1. Normalize a hypothetical counterexample

A failing polynomial is scaled into the open disk and contracted about a distinguished zero until it reaches an exact first-contact barrier. All roots and critical points remain in the required geometric region, while at least one critical point reaches the boundary of the relevant distance-one disk.

2. Encode the critical geometry

Reciprocal critical coordinates give a strict cap and an antiderivative factorization. A division-free coefficient identity and an elementary product-defect estimate yield the double-defect inequality used later in the reduction.

3. Force a scalar parameter

A polar-product identity produces an explicit scalar parameter rather than leaving an implicit root. The manuscript derives a quantitative lower bound for that parameter from the first-contact geometry.

4. Reduce the remaining obstruction

Integration by parts and Maclaurin's inequality turn every proposed barrier of degree at least six into a one-variable scalar demand. Degrees two through five are handled separately.

5. Derive incompatible bounds

The candidate argues that any counterexample would force

(m + 1) E_m(λ) > 1 + λ, where m = n − 1,

while its master error estimate gives the reverse inequality throughout the feasible range.

6. Cover every degree range

The endpoint range is handled analytically. Degrees corresponding to 5 ≤ m ≤ 499 use a finite exact certificate, and the large-degree range uses a second analytic argument supported by a uniform exact certificate.

Exact computational evidence

The archival packet retains exact rational data and two verifier implementations for each terminal certificate design. Its reported proof objects include:

The Revision 13 audits reported no fatal mathematical error and independently reconstructed the terminal certificates. Revision 14 records how their exposition and release findings were addressed.

Certification boundary

The exact programs certify the two terminal scalar propositions used by the manuscript. They do not machine-check the earlier barrier reduction, product-defect bridge, polar forcing, integration-by-parts argument, mismatch theorem, or analytic range reductions. Those steps remain written mathematics.

The paired verifier implementations are useful transcription and implementation cross-checks of the same mathematical certificate designs. They are not independent formal proofs of the upstream argument, and no Lean or other proof-assistant formalization is currently attached.

Authorship and AI disclosure

Lech Mazur is the author and takes responsibility for the manuscript. The paper reports that OpenAI GPT-5.6 Pro played a substantial role in mathematical exploration, proof development, computational testing, adversarial auditing, and exposition, with human orchestration, selection, and reconciliation of the resulting work.

Public revision

This page hosts public Revision 14, dated August 2, 2026, with release identifier SENDOV-REV14-2026-08-02. The linked PDF and LaTeX source are fixed, digest-bound copies. The complete ZIP packet retains the certificate data, exact verifiers, generators, tests, reference logs, environment description, and release manifests associated with that revision. Later corrections or stronger certification should appear as a new public revision rather than silently replacing these bytes.

Current status

The manuscript is a proof candidate. It has substantial exact computational support and a documented adversarial-audit history, but it has not yet received the independent specialist certification needed to present Sendov's conjecture as an established theorem. Publication here makes the candidate and its exact dated source available for examination; it does not itself establish mathematical correctness or priority beyond those public bytes.

Documents and resources

Scope

What this page does not establish