In the digestion of the proof of Sendov's conjecture, one step reduces to showing that an inequality — call it (stat) — is infeasible for every integer degree n in [5,200] and every α in [0,17] (with a side constraint). The right-hand side R(n,α) stays strictly below 1. Step n with the ↑/↓ arrow keys and watch the curve never touch the threshold.
An original interactive applet, part of tao-web.
Heatmap of R(n,α) over the entire range. Every admissible cell is coloured by its value; none reaches 1, so (stat) is infeasible throughout. Grey = outside the constraint c(α)2 ≤ a2. The vertical marker is the current degree; the bracket shows the α window above.
Writing R(n, α) for the right-hand side below, the inequality (stat) is the assertion 1 ≤ R(n, α). This applet illustrates that it is infeasible — that is, R(n, α) < 1 — throughout the stated range.
a2 = 1 − 2α/(n−1)
c(α) = 1 − α/(n−1) − α/(2(3+α))
The range to be covered is all integer degrees n and reals α with 5 ≤ n ≤ 200, 0 ≤ α ≤ 17, and c(α)2 ≤ a2 = 1 − 2α/(n−1). (The last constraint keeps α away from its upper limit (n−1)/2, and makes the quadratic 1 − 2c(α)t + a2t2 positive on [0,1], so the integral is real.)
The integral I(n,α)=∫01 t3(1−2c t+a2t2)(n−4)/2 dt is evaluated by a fixed 64-node Gauss–Legendre rule (about 14-digit accuracy for every n here, regardless of parity). For even n the integrand is a polynomial, so I also has an exact closed form; the readout cross-checks the quadrature against that exact value computed in BigInt rational arithmetic. For odd n there is no obvious elementary closed form — but the quadrature does not care.
Sendov's conjecture asserts that if a degree-n polynomial has all of its zeros in the closed unit disk, then within distance 1 of every zero there lies a critical point. It was recently resolved for all n ≥ 2 by Lech Mazur, using an AI tool, with the resulting proof verified in Lean. Terence Tao then digested that AI-generated proof — placing it in context with the earlier literature and streamlining the argument — and in the course of the digestion reduced one step to showing that the inequality (stat) above is infeasible over the range shown. The full digestion is in Tao's blog post below; the entire n ≥ 5 argument, this infeasibility bound included, has also been formalized in Lean.