An explicit solution of the five-expert prediction PDE and the exact optimality set of COMB
Jeff Calder, Nadejda Drenska
math.AP
Sep 14, 2026 · v2
cs.GT cs.LG math.OC
TL;DR
A Lean 4/Mathlib formalization machine-checks the Bernstein certificate verification, regularity, boundedness, and both main theorems except the viscosity characterization.
Abstract
In this paper, we derive an explicit solution of the stationary prediction with expert advice PDE for five experts. The formula is given in three regions. In the first two regions, it is the four-expert solution plus a single integral with an elementary positive density. In the third region, it is a finite sum of hyperbolic products whose coefficients are determined by one scalar quadrature. Our formula establishes that the direction $(1,0,1,0,0)$ is optimal throughout the ordered sector, and that the COMB strategy $(1,0,1,0,1)$ is optimal only on a lower dimensional subset of the sector (where $x_1=x_2$ and $x_3=x_4$). This disproves the COMB optimality conjecture of Gravin, Peres and Sivan. The verification of the Hamiltonian inequalities is a tedious task, part of which is completed with a computer assisted proof. The verification reduces to 21 scalar inequalities, which we prove using 147 exact rational Bernstein polynomial certificates. The exact certificates and their independent arithmetic checks are included in a supplement to this paper, and a Lean 4 formalization machine-checks the verification and both main theorems, apart from the viscosity characterization.
Problem
The goal is an explicit solution of the stationary prediction-with-expert-advice PDE for five experts under geometric stopping. The solution is used to test the conjecture of Gravin, Peres and Sivan that the COMB strategy is optimal.
Approach
An explicit formula is derived in three regions of the ordered sector. In two regions it is the four-expert solution plus a single integral; in the third it is a sum of hyperbolic products governed by one scalar quadrature. The Hamiltonian inequalities reduce to 21 scalar inequalities, which are proved with 147 exact rational Bernstein polynomial certificates. The certificates, the reduction to them, the regularity, and the optimality-set result are formalized in Lean 4 on top of Mathlib.
Results
The direction (1,0,1,0,0) is optimal throughout the ordered sector. COMB (1,0,1,0,1) is optimal only on the lower-dimensional subset where x1=x2 and x3=x4, which disproves the COMB optimality conjecture. The Lean artifact covers both main theorems apart from the viscosity characterization.
