Smale's 9th problem: polynomial-time LP feasibility over $\mathbb{R}$

Open

SmaleNinth.smale_ninth_problem

by ORdos · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

computational-complexitylinear-programmingopen-problemsmale-problemsstrongly-polynomial

Consider the decision problem: given a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ of arbitrary real numbers, decide whether the system of linear inequalities has a solution, that is, whether

\{\,x \in \mathbb{R}^n \;\mid\; Ax \ge b\,\} \;\ne\; \emptyset ,

where the inequality is componentwise. The instance is presented to a machine over the real numbers as $mn + m + 2$ tape cells (the two dimensions, the entries of $A$ in row-major order, then $b$ ), and the cost of a computation is the number of instructions it executes, each arithmetic operation, comparison and shift costing one unit regardless of the magnitude of the reals involved.

The assertion. There exist a single program $P$ , and constants $C, d \in \mathbb{N}$ , such that for every $m$ , every $n$ , every $A \in \mathbb{R}^{m\times n}$ and every $b \in \mathbb{R}^m$ , the program $P$ started on the encoded instance halts with the correct verdict within

C\,(mn + m + 2)^{d}

steps: it accepts if $\{x \mid Ax \ge b\}$ is nonempty, and rejects otherwise.

Reading the quantifiers. The program and both constants are chosen once, before any instance is seen; only the verdict and the actual halting time depend on the instance. The algorithm is therefore required to be uniform — one finite instruction list for all dimensions — and its running time to be bounded by a fixed polynomial in the number of input reals. In particular the bound may not depend on the magnitudes, the bit lengths, or any conditioning of $A$ and $b$ ; every algorithm currently known for this problem violates exactly this, its iteration count being governed by a quantity that is unbounded over real instances of fixed dimension.

What the statement deliberately leaves unfixed. Neither the degree $d$ , nor the constant $C$ , nor any structure of the program is prescribed: the claim is only that some polynomial bound holds, so it is invariant under future quantitative improvements and cannot be invalidated by a sharper analysis. Conversely, an algorithm is here a finite program in the fixed instruction set, not an arbitrary function of the input reals — a set-theoretic decision function always exists, and would make the statement vacuous.

This is Problem 9 on Smale's list of mathematical problems for the next century, and it is open.

Preamble

import Definitions.Def_Polyhedron
import Definitions.Def_SmaleNinth_BSSMachine

/-!
Smale's 9th problem: polynomial-time linear programming feasibility over
the real numbers.

Source: S. Smale, *Mathematical problems for the next century*, Mathematical
Intelligencer 20(2):7–15, 1998, Problem 9: "Is there a polynomial-time
algorithm over the real numbers which decides the feasibility of the linear
system of inequalities $Ax \ge b$?" — in the machine model of Blum–Shub–
Smale (Bull. AMS 21(1):1–46, 1989), formalized in
`Definitions.Def_SmaleNinth_BSSMachine`.

The statement asks for a single BSS program `P` (one uniform algorithm, with
arbitrary real machine constants) and constants `C, d` such that on every
instance — every `m`, `n`, every real `A : m × n` and `b : m` — the program,
run on the standard input encoding, halts within `C·(mn + m + 2)^d` steps
(unit cost per arithmetic operation, comparison, or shift; `mn + m + 2` is
the number of input cells) and accepts exactly when `{x | Ax ≥ b}` is
nonempty.
-/

open LinearOptimization

/-- **Smale's 9th problem** (Smale 1998, Problem 9; Blum–Shub–Smale model).
There is a uniform BSS program over `ℝ` deciding the feasibility of
`Ax ≥ b` in a number of steps polynomial in the number `mn + m + 2` of
input reals. -/

Formal statement

theorem SmaleNinth.smale_ninth_problem :
    ∃ (P : BSSProgram) (C d : ℕ),
      ∀ (m n : ℕ) (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ),
        ∃ result : Bool,
          BSSDecidesInTime P (encodeLP A b) (C * (m * n + m + 2) ^ d) result ∧
          (result = true ↔ (polyhedron A b).Nonempty) := by sorry

Source

S. Smale, Mathematical problems for the next century, Mathematical Intelligencer 20(2):7-15, 1998, Problem 9 (also in: Mathematics: Frontiers and Perspectives, AMS 2000). Machine model: Blum-Shub-Smale, Bull. AMS 21(1):1-46, 1989.

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `SmaleNinth.smale_ninth_problem`

The machine model referenced by the statement. A BSS program $P$ is a finite list of instructions, each of one of the following kinds, where every address is a fixed integer $\mathbb{Z}$ hard-coded in the instruction and the machine's memory is a two-way-infinite tape $x : \mathbb{Z} \to \mathbb{R}$ of real registers:

$x[\mathrm{dst}] := c$ for an arbitrary fixed real constant $c$ (real machine constants are allowed);
$x[\mathrm{dst}] := x[i] + x[j]$ , $x[i] - x[j]$ , $x[i] \cdot x[j]$ , or $x[i] / x[j]$ (division is total, with $r/0 = 0$ );
shift-left (new $x[k] =$ old $x[k+1]$ for every $k$ ) and shift-right (new $x[k] =$ old $x[k-1]$ );
a conditional jump on register $i$ : if $x[i] \le 0$ (non-strict), set the program counter to a fixed target index; otherwise fall through to the next instruction;
two halting instructions, accept and reject.

Execution starts with program counter $0$ on a given initial tape; each step executes the instruction at the current program counter and (except for jumps and halts) advances the counter by one. A configuration whose counter points at accept, at reject, or outside the program list is a fixed point of the step function (nothing further changes).

The predicate " $P$ decides on input $x$ within $T$ steps with output $r$ " (the unfolding of $\mathrm{BSSDecidesInTime}\ P\ x\ T\ r$ ) asserts:

\exists\, t \le T \text{ such that after exactly } t \text{ steps from } (\mathrm{pc}=0,\ \mathrm{tape}=x), \text{ the program counter points at the instruction } \textit{accept} \text{ if } r = \mathrm{true},\ \textit{reject} \text{ if } r = \mathrm{false}.

Note $t \le T$ is non-strict, and merely running off the end of the program never counts as either output: the counter must sit on an actual accept/reject instruction.

The input encoding. For $m, n \in \mathbb{N}$ , a matrix $A \in \mathbb{R}^{m \times n}$ and a vector $b \in \mathbb{R}^m$ , the tape $\mathrm{encodeLP}(A,b) : \mathbb{Z} \to \mathbb{R}$ is:

cell $0$ holds the real number $m$ ; cell $1$ holds the real number $n$ ;
cells $2, \dots, mn+1$ hold the entries of $A$ in row-major order (cell $2 + (i n + j)$ holds $A_{ij}$ ; if $n = 0$ or the offset is out of range, the row-major lookup returns the junk value $0$ , so this segment is empty when $mn = 0$ );
cells $2 + mn, \dots, 2 + mn + m - 1$ hold $b_0, \dots, b_{m-1}$ ;
every other cell — including all negative cells — holds $0$ .

The feasibility set. $\mathrm{polyhedron}(A, b) = \{\, x \in \mathbb{R}^n \mid b \le A x \,\}$ , where $\le$ is componentwise: $\forall\, i \in \{0,\dots,m-1\},\ b_i \le (Ax)_i$ with $(Ax)_i = \sum_{j=0}^{n-1} A_{ij} x_j$ . "Nonempty" means $\exists\, x \in \mathbb{R}^n$ satisfying all $m$ inequalities.

What the theorem asserts. There exist a single finite BSS program $P$ (with whatever real constants its instructions carry) and natural numbers $C, d \in \mathbb{N}$ — all three chosen once, uniformly, before any instance is seen — such that for every $m, n \in \mathbb{N}$ , every $A \in \mathbb{R}^{m \times n}$ , and every $b \in \mathbb{R}^m$ , there exists a Boolean $r$ (chosen per instance, after $m, n, A, b$ ) with both:

$P$ , started on the tape $\mathrm{encodeLP}(A,b)$ , reaches an accept (if $r = \mathrm{true}$ ) or reject (if $r = \mathrm{false}$ ) instruction within at most

C \cdot (m n + m + 2)^{\,d}

steps, each step being one instruction execution (one arithmetic operation, constant load, shift, jump, at unit cost); and 2. $r = \mathrm{true}$ if and only if $\{x \in \mathbb{R}^n \mid b \le Ax\}$ is nonempty.

So the program and the polynomial bound are uniform over all dimensions and all real data, while the output bit and the halting time $t \le C(mn+m+2)^d$ may depend on the instance. The two conjuncts together force $P$ to halt with the correct answer on every instance within the stated bound.

Edge cases the quantifiers silently include.

$m = 0$ : there are no constraints; $b$ is the empty vector, and every $x \in \mathbb{R}^n$ (including the unique empty vector when $n = 0$ ) satisfies the empty system vacuously, so the polyhedron is all of $\mathbb{R}^n$ and is always nonempty — the program must accept, within $C \cdot 2^d$ steps (the bound evaluates to $C\cdot(0 + 0 + 2)^d$ ). The input tape then holds $m=0$ , $n$ , no $A$ -segment and no $b$ -segment.
$n = 0$ : the only candidate point is the empty vector, and $Ax = 0$ , so the polyhedron is nonempty iff $b_i \le 0$ for all $i$ ; the tape holds no $A$ -entries and the bound is $C \cdot (m+2)^d$ .
$C$ and $d$ range over all of $\mathbb{N}$ , including $0$ ; since $mn + m + 2 \ge 2$ , the bound $C(mn+m+2)^d$ is $0$ exactly when $C = 0$ (in which case halting would have to occur at step $0$ , which is impossible for a nonempty requirement — but $C, d$ are the prover's choice, so this only restricts which witnesses can work).
Division by zero inside the machine yields $0$ rather than being undefined, and the branch test is the non-strict $x[i] \le 0$ .

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by ORdos · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Smale's 9th problem: polynomial-time LP feasibility over R\mathbb{R}R

Read-back: SmaleNinth.smale_ninth_problem

Smale's 9th problem: polynomial-time LP feasibility over $\mathbb{R}$

Read-back: `SmaleNinth.smale_ninth_problem`