A lightly edited transcript of the conversation that built the Sendov infeasibility explorer, an interactive companion to the digestion of the proof of Sendov's conjecture. It visualizes that a certain inequality — labelled (stat) in the digestion — is infeasible for every degree 5 ≤ n ≤ 200 and every 0 ≤ α ≤ 17.
How to read this. Terence Tao's messages appear verbatim in the blockquotes; the assistant's replies are summarised in italics between them. Routine "looks good, continue" replies are folded into the narration.
1. The concept, and a worry about one integral
I'm writing a blog post concerning a proof of Sendov's conjecture. One of the steps is to show that a certain inequality, labeled "stat" in the blog post, is infeasible for a specific range of n and alpha. I'd like to design an app to illustrate this inequality for n and alpha in the indicated ranges. The one tricky thing is that it involves an integral which can be computed exactly for n even but does not have an obvious closed form as far as I can tell for n odd. Can you look at the post and assess the feasibility of making an app to visualize this inequality, perhaps with some arrow keys or other GUI to move n up and down, and perhaps also some way to select the range of alpha being plotted?
The assistant read the blog source and pinned down the object to plot. Writing R(n, α) for the right-hand side, (stat) is the assertion 1 ≤ R(n, α), where R is an explicit expression whose only non-elementary ingredient is the integral ∫₀¹ t³ (1 − 2c(α)t + a²t²)^((n−4)/2) dt, with a² = 1 − 2α/(n−1) and c(α) = 1 − α/(n−1) − α/(2(3+α)). "Infeasible" means R(n, α) < 1 throughout the region 5 ≤ n ≤ 200, 0 ≤ α ≤ 17, c(α)² ≤ a².
On the worry about odd n: for a numerical picture the parity turns out to be a non-issue. A single fixed 64-node Gauss–Legendre rule evaluates the integral to about 14 digits for every n in the range, both parities — checked against a 60-digit reference. The surprise ran the other way: the even-n closed form is the numerically dangerous one, since the naive binomial expansion of the integrand suffers catastrophic cancellation at large n (it returned a spurious value near 10³⁸ around n = 200 in double precision). So the plot should be driven by quadrature, with the closed form kept only as an exact cross-check in exact (BigInt) arithmetic. A quick scan also confirmed the inequality really does hold, with a margin large enough to be visible: R peaks at about 0.853 near (n, α) = (53, 17).
2. Two scope choices
The assistant asked whether to show only a single α-slice per degree or also a full two-dimensional picture, and whether to include the exact even-n cross-check. Tao chose both the one-dimensional slice and a two-dimensional heatmap, and opted to include the exact cross-check.
So the app got two linked views: an R-vs-α curve for the current degree — the arrow keys step n up and down, and the α-window is selectable — drawn against the threshold R = 1, and a heatmap of R over the whole (n, α) rectangle with the admissible region outlined, the "infeasible everywhere" view. For even n the app also evaluates the integral exactly in BigInt rational arithmetic and shows how closely the 64-node quadrature agrees with it.
3. Getting the numbers exactly
The mathematics lives in a DOM-free core, tested under node. It carries the 64-node Gauss–Legendre rule for the integral, the admissibility test c(α)² ≤ a², the admissible α-interval and the worst-case α for each degree, and the exact even-n integral. That exact path is done in pure integer arithmetic — the dyadic coefficients are scaled up to integers, the quadratic is raised to its integer power, and the result is reduced only once at the very end — which sidesteps an early version that was hopelessly slow because it took gcds of thousand-digit numbers inside the inner loop. The tests check the integral and R against the 60-digit reference values, the exact-even path against the quadrature, and — the point of the whole exercise — that R < 1 across a dense sweep of the entire region.
4. Documenting the inequality
the blog post has been updated ... and a Lean formalization is underway at github.com/teorth/sendov. Can you update the documentation of the app page to state the precise form of {stat} and link to the repo ... One can also mention the original proof of Sendov's conjecture by Mazur (mentioned in the blog post).
The page gained a precise statement of (stat) — rendered in plain HTML and Unicode, since the app's content-security policy rules out a MathJax CDN — together with the definitions of a and c(α) and the exact range to be covered, plus a background section: Sendov's conjecture, Lech Mazur's AI-generated proof (verified in Lean), Tao's digestion, and a link to the Lean formalization repository. The page went live at its own URL first, deliberately unlisted, so it could serve as a stable reference for the blog post before appearing on the applets index.
5. Publishing
The Sendov blog post is up. Update the sendov app page, link to applet main page with making of, and push.
With the digestion now public, the app page links straight to it, and the applet joined the catalogue in the Complex analysis category — a recent original sitting alongside the legacy Java applets — with this making-of beside it.