A stability order barrier and SSP bound for Runge–Kutta methods with non-negative coefficients: AI-assisted proofs
Sigal Gottlieb, Zachary Grant, Lior Horesh, Lajos Lóczi, Avraham Shinnar, Barry Trager
math.NA
Nov 5, 2026 · v1
TL;DR
The paper's SSP bounds, phase-type moment inequalities and algebraic-stability order barrier are formalized in Lean 4 with Mathlib, with no sorry and only standard axioms.
Abstract
We prove three results about Runge–Kutta methods with non-negative coefficients. First, every $s$-stage implicit Runge–Kutta method of order at least two has SSP coefficient at most $2s$; the bound is sharp and is attained by a known diagonally implicit method, so full implicitness gives no advantage over DIRK at second order. This extends the second-order DIRK result of Kocsis & Németh to full coefficient matrices and settles a conjecture of Ketcheson, Macdonald & Gottlieb. These proofs were found with the assistance of AI tools, which uncovered an interesting relationship between the Butcher matrices for SSP methods and phase-type distributions, and led to the proof of the second result: a bound on the SSP coefficient of $s$-stage implicit Runge–Kutta method of order at least three. The third result in this work is a proof that a third-order Runge–Kutta method with entrywise non-negative $A$ and $b$ cannot be algebraically stable. This algebraically intensive proof was also AI-assisted. This paper describes the iterative process of AI-assisted results, and presents an approach that centers human understanding and creativity in the AI-assisted mathematical endeavor.
Problem
Several conjectured results about Runge–Kutta methods with non-negative coefficients lacked proofs. These include the bound SSP coefficient ≤ 2s for second-order s-stage implicit methods, a sharp bound for third-order methods, and the incompatibility of third-order accuracy with algebraic stability.
Approach
The authors used ChatGPT, Claude and Gemini to explore candidate proofs. The AI tools surfaced a dictionary between SSP conditions and absorbing Markov chains / phase-type distributions, which turns order conditions into moment inequalities (Aldous–Shepp, Osogami, and a new moment-ratio hierarchy). Human-digested proofs were then formalized in Lean 4 with Mathlib, and the formalization exposed unnecessary hypotheses.
Results
The 2s bound is proved sharp for all implicit second-order methods, settling a conjecture of Ketcheson, Macdonald and Gottlieb. A third-order SSP bound and an order-three barrier for algebraic stability with non-negative coefficients are also proved. All elementary results are machine-checked in Lean, and the r ≤ 2s result is verified end to end.
| Result | Lean identifier | Status |
|---|
| Theorem 2 | ssp_bound_of_conditions | Verified |
| Theorem 4 | aldous_shepp | Verified |
| Theorem 7 | cyclic_hierarchy | Verified |
| Theorem 8 | order3_bound_of_invMat | Verified |
| Theorem 9 | barrier_unsorted | Verified |
Selected correspondences between results and Lean formalizations (namespace SSP.MainRevised)
