Adversarial Wronskians: A proof of the Kung–Traub conjecture
Matthew J. Colbrook
math.NA
Sep 20, 2026 · v1
cs.CC math.CA
TL;DR
The paper's results on the Kung–Traub conjecture are formally verified in Lean 4, with a public repository, ChatGPT-assisted proofs, and checks using Lean 4 Comparator.
Abstract
We prove the Kung–Traub conjecture: a deterministic stationary root-finding method without memory, using at most $n$ real scalar function or derivative evaluations per iteration, cannot have local order greater than $2^{n-1}$ on every real analytic function with a simple zero. For $n\geq2$, the bound is attained by the methods of Kung and Traub. The local estimate is required at every sufficiently close starting point, with constants that may depend on the function. Evaluation points and derivative orders may be chosen adaptively, and the rules for choosing them and processing the data are unrestricted. The proof uses a localisation property of polynomial Wronskians to obtain a lower bound at each fixed scale. A diagonal construction then gives one entire function, with derivative bounded above and below on the real line, for which every larger order fails. We also obtain a sharper bound when evaluations are made in prescribed groups, and prove the corresponding result for complex scalar evaluations. The results of this paper are also formally verified in Lean.
Problem
The Kung–Traub conjecture (1974) states that a memoryless deterministic root-finding iteration using at most n function or derivative evaluations cannot have local order greater than 2^{n-1} on every real analytic function with a simple zero. Kung–Traub methods attain this bound, but the matching upper bound had not been proved.
Approach
A localisation property of polynomial Wronskians gives a lower bound on the error at each fixed scale against any adaptive algorithm. A diagonal construction then builds a single entire function, with derivative bounded above and below on the real line, on which every order larger than 2^{n-1} fails. Each successive correction preserves all previously queried derivative values. The results were formalized in Lean 4 with ChatGPT assistance and checked using Lean 4 Comparator for unintended axioms.
Results
The conjecture is proved for real scalar evaluations, with a sharper bound when evaluations are made in prescribed groups and an analogous result for complex evaluations. A Lean verification is available at github.com/MColbrook/Kung-Traub_conjecture.
