Sendov’s conjecture

Sendov's conjecture

Model / AI: ProofAtlas, Claude Opus 5

Lech Mazur, working through the ProofAtlas agent platform, resolved the conjecture for all n >= 2; Tao digested and streamlined the argument, then re-formalized it in Lean with Claude Opus 5 (15,152 lines, no sorry, no native_decide, exact rational Bernstein certificates). That development descends from Mazur's proof rather than being a second discovery, but is separately checkable.

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

• Context — Sendov's conjecture
• Lean — 15,152 lines