Papers With

← All papers
First page of From boundary geometry to counterexamples in Smale's mean value problem

From boundary geometry to counterexamples in Smale's mean value problem

Tom Adamczewski, Matthew J. Colbrook

math.CV Oct 26, 2026 · v1
formalization theorem-proving-ml analysis
Read PDF arXiv abstract Code
TL;DR
The counterexample arose from an AI model disproving the Lean statement of Smale's conjecture in Formal Conjectures; a Lean 4 disproof repository is cited.
Abstract
This paper provides a human digestion of the recent counterexample to Smale's mean value problem found by GPT-6 Astra. We give a geometric mechanism for constructing counterexamples. An outward normal that re-enters an analytic Jordan domain, subject to a curvature condition, yields a holomorphic model whose normalized divided differences exceed one in modulus on the boundary. Polynomial perturbations then concentrate every critical point near the boundary whilst preserving the strict inequality. This turns boundary geometry into counterexamples in every sufficiently large degree. We also locate these critical points to first order and show that their limiting distribution is the logarithmic equilibrium measure on the boundary. We end with an explicit example of degree $29\,984$, verified by interval arithmetic.
Problem

Smale's mean value problem asks whether every polynomial has a critical point whose normalized divided difference has modulus at most 1. GPT-6 Astra recently found a counterexample to this constant-one version, and that counterexample needs a human-understandable explanation.

Approach

The paper gives a geometric sufficient condition, the normal-return criterion. An outward normal from a boundary point of an analytic Jordan domain re-enters the domain, subject to a curvature inequality. This yields a holomorphic model whose normalized divided differences exceed one on the boundary. Polynomial perturbations built from Faber polynomials or high powers then push all critical points toward the boundary while keeping the strict inequality. A cubic-seed example illustrates the mechanism concretely.

Results

Counterexamples to the constant-one conjecture exist in every sufficiently large degree. The critical points are located to first order, and their limiting distribution is the logarithmic equilibrium measure on the boundary. An explicit degree-29,984 example is verified by interval arithmetic; the original disproof, found against the Lean statement in Formal Conjectures, has a Lean 4 artifact.