Kung–Traub conjecture on optimal order of multipoint iteration without memory

### What is the conjecture

The Kung–Traub conjecture concerns the optimal convergence order of multipoint iterative methods for finding roots of nonlinear equations.

Let $f: \mathbb{R} \to \mathbb{R}$ be a function and suppose we have an iterative method $x_{k+1} = \Phi(x_k, f(a_1(x_k)), f(a_2(x_k)), \ldots, f(a_n(x_k)))$ that uses exactly $n$ evaluations of the function $f$ (with no derivatives) at each iteration step to compute the next iterate. Such a method is called a **multipoint iteration without memory**.

**Conjecture:** For any multipoint iteration without memory using $n$ function evaluations, the optimal (maximum achievable) order of convergence is $p = 2^{n-1}$.

In other words, an iterative method based on $n$ function evaluations cannot achieve a convergence order higher than $2^{n-1}$, and methods achieving this bound are considered optimal.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- 1. Kung, H. T., & Traub, J. F. (1974). "Optimal Order of One-Point and Multipoint Iteration." *Journal of the ACM*, 21(4), 643-651. https://dl.acm.org/doi/10.1145/321850.321860

2. Kung, H. T., & Traub, J. F. (1974). PDF version. https://www.eecs.harvard.edu/~htk/publication/1974-jacm-kung-traub.pdf

3. Traub, J. F. (1964). *Iterative Methods for the Solution of Equations*. Prentice-Hall.

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-03-08)

Building blocks (1-3; from search results):
- Real functions and numerical analysis concepts in Mathlib (Analysis library)
- Convergence and order of convergence notions (metric spaces, limits)
- Function evaluation and iteration mechanics

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of "order of convergence" for iterative methods in Lean (convergence order as a limit of a ratio of successive errors)
- Formal definition of "multipoint iteration without memory" and the constraint on number of function evaluations per step

Rating justification (1-2 sentences): The conjecture is a statement about the achievable order of convergence in numerical methods and requires careful formalization of convergence rates and iteration constraints. While basic analysis concepts exist in Mathlib, the specific notion of "order of convergence" for iterative methods and the precise formulation of multipoint iterations without memory would need to be defined, requiring moderate infrastructure development.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-65
* ams-41

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

No repository files, tests, or entry points are named. Start by checking the repository's existing formalizations and Mathlib's analysis and convergence APIs, then determine how iterative methods and evaluation constraints are represented. Done means the conjecture is stated precisely in Lean with the required definitions and supporting infrastructure.

Written by the indexing model from the issue text.