ProofAtlas

First-party checked source

Source for Sendov's Conjecture

This pinned Lean source formalizes the following mathematical result: 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. Download the complete checked closure, open the endpoint, or browse its supporting modules to study the proof or develop an extension.

Read the theorem overviewComplete checked Lean source · 1160 Lean files · 1 evidence record · Download ZIPOpen Theorem.lean

Immutable source commit: f8b71644c02bf16d8e9f7e183428ac2d4b0f6bf1

License and notice commit: a2c408da983f4a47b48fe0a24c64e539b0721993

Each ZIP contains the checked first-party local Lean import closure, exact statements and boundaries, license, notice, evidence, a source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled; this is not a portable whole-repository release.

Proof and source

What is checked—and how much source supports it

Browse the counted source
Declarations covered by evidence
1
First-party Lean files
1,160
Lean source lines
92,816
Main recorded file
20 lines
How the source is counted

Line counts exclude blank lines; comments and documentation count. The total is the deduplicated, commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded. Declaration count means names covered by the artifact's recorded evidence, not every declaration in the source. Source footprint is not a difficulty or proof-quality score.

Exact theorem evidence

Sendov's Conjecture

Sendov.sendov_conjecture

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit
f8b71644c02bf16d8e9f7e183428ac2d4b0f6bf1
Main Lean file
Sendov/Theorem.lean
Main-file footprint
20 lines
File SHA-256
sha256:8d11960bfa4f2c341e2fce83917271031b9885a9be68ffedef986bc075fc8c09
Complete Lean closure
1,160 files · 92,816 lines
Toolchain
leanprover/lean4:v4.30.0-rc2
Open main Lean file Download main Lean fileDownload checker evidence (JSON)Download Apache-2.0 licenseDownload Advameg, Inc. notice

Deduplicated checked source

Complete Lean import closure

This closure supports the theorem evidence record above.

Complete checked Lean closure

1160 Lean files are available here

Start with the principal theorem and proof-architecture files below, or search the complete commit-pinned closure.

1160Lean files
Search and browse all 1160 checked Lean files

Every listed file is read from the same pinned Git commit. File links open raw source in a new tab; use the ZIP download for the complete package. External Mathlib modules are dependency-locked but are not copied into this first-party source tree.

Showing all 1160 files

Sendov2 files · 40 lines
Sendov/Certificate581 files · 17,237 lines
Sendov/Certificate/Generated527 files · 66,411 lines
Sendov/Optimized/Algebra16 files · 2,751 lines
Sendov/Optimized/Analysis11 files · 2,198 lines
Sendov/Optimized/Defect3 files · 936 lines
Sendov/Optimized/Geometry2 files · 234 lines
Sendov/Scalar18 files · 3,009 lines
Source hashMatches checked record
Lean buildPassed in recorded evidence
LicenseApache-2.0 · Advameg, Inc.

Provenance and reproducibility

Exact checked source, with reuse terms

The endpoint and every listed local import come from the exact recorded Git commit, and the endpoint matches the stored source hash byte for byte. The locally authored package material is licensed under Apache-2.0 by Advameg, Inc.; Mathlib and cited third-party material remain under their own terms. Machine-readable checker evidence is included.