ProofAtlas

Lean evidence record

Sendov's Conjecture: Lean evidence

This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.

Read theorem page
Lean buildpassed
Unfinished proof stepsNone
Publication reviewsPending

Exact recorded Lean statement

The declaration this evidence supports

theorem sendov_conjecture : SendovConjecture

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.

Technical evidence record

Source identity, checker results, and assumptions

Main Lean declaration
sendov_conjecture
Source commit
f8b71644c02b

Mechanical evidence

Lean verification

These fields support the exact Lean declaration, not a broader informal claim.

Why ProofAtlas acceptance is still pending: the supplied release audit records a successful one-worker rehash build, no unfinished proof commands, and the reported axiom closure. It does not retain the complete command/output transcript and clean-source collection record required for accepted-result status.

Artifact ID
artifact.sendov.conjecture.lean-package.v001
Declarations covered by recorded evidence
Sendov.sendov_conjecture
Lean build
passed
Recorded build time
Not retained in the supplied release audit
Unfinished proof check
passed
Lean toolchain
leanprover/lean4:v4.30.0-rc2
Recorded source commit
f8b71644c02bf16d8e9f7e183428ac2d4b0f6bf1
Source SHA-256
sha256:8d11960bfa4f2c341e2fce83917271031b9885a9be68ffedef986bc075fc8c09
Statement alignment
not reviewed

Lean foundations

Standard foundations used by the proof

Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.

  • Classical.choice
  • Quot.sound
  • propext

Files and machine-readable evidence

Reproduce or inspect the recorded check

Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.

Complete checked Lean source · 1160 Lean files · 1 evidence record · Download ZIPBrowse counted source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license

Review results

Publication review remains open

This exact artifact has not yet cleared every publication-review gate. The Lean evidence below remains useful for inspecting what was checked, but it is not an accepted result record.

Read the publication-review details

Credit for this release

Contributors and roles

Authorship and other contributions are recorded separately for this version.

Authorship

Paper author
Lech Mazur

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

Selected review

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.