{"id":"palomar/PALOMAR-2026-08-13-000001","url":"https://github.com/teorth/sendov/tree/1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-13-000001-v2.json","repo":"https://github.com/teorth/sendov","tags":["math.CV","msc:30C15","msc:30C10","msc:12D10","complex-analysis","polynomials","lean-formalization","sendov-conjecture"],"score":0,"title":"teorth/sendov","trust":"high","domain":"math.CV","source":"palomar","authors":["Terence Tao"],"reviews":0,"subject":"math.CV","summary":"A Lean formalization of Sendov's conjecture, and of its Phelps-Rodriguez strengthening, in full generality: if every zero of a complex polynomial p of degree n >= 2 lies in the closed unit disk, then every zero a of p has a critical point of p within distance 1 of it, and within distance strictly less than 1 unless |a| = 1 and p is a scalar multiple of z^n - a^n. The proof is by contradiction. Degrees 2 to 4 fall to an elementary integral computation; degree 5 upward goes through two estimates on the same integral -- a polar channel and an origin channel -- which are shown to be…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","reactions":{},"formalized":true,"formalizes":[{"title":"A digestion of the proof of Sendov's conjecture","identifier":"https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/","relationship":"formalizes"},{"title":"Some properties of extremal polynomials for the Ilieff conjecture","identifier":"https://zbmath.org/3386011","relationship":"formalizes"},{"title":"Sendov conjecture proof (ProofAtlas manuscript)","identifier":"https://www.proofatlas.ai/papers/sendov-conjecture/","relationship":"adapts"}]}