The finite-horizon five-expert prediction problem
Jeff Calder, Nadejda Drenska
math.AP
Sep 29, 2026 · v1
cs.GT cs.LG math.OC
TL;DR
The proofs of the main theorems, including the interval-arithmetic sign certificates, are formalized in the Lean proof assistant.
Abstract
We give an explicit solution to the five expert prediction with expert advice partial differential equation (PDE) in the finite-time horizon setting. The solution formula establishes that the adversary's rank strategy $(1,0,1,0,0)$ is globally optimal, and the COMB strategy $(1,0,1,0,1)$ is optimal exactly on the set where $x_1=x_2$ and $x_3=x_4$. The formula is derived from the solution of the geometric-stopping problem given in our companion paper through the transform principle of Bayraktar, Ekren and Zhang, which links the two problems by a Laplace transform. Inverting the transform term by term expresses the solution through a series of Gaussian and complementary error function kernels. The optimality of $(1,0,1,0,0)$ is reduced to the signs of $41$ one-variable Gaussian series, which are certified with computer assistance by Poisson summation, first-mode domination and interval arithmetic on $1616$ rational cells. The proofs of our main theorems, certificates included, are also formalized in the Lean proof assistant.
Problem
The finite-horizon prediction-with-expert-advice PDE had explicit solutions only for up to four experts, and the optimality of the COMB adversary strategy for five experts was an open question.
Approach
The finite-horizon solution is derived from the companion paper's geometric-stopping solution via the Laplace-transform principle of Bayraktar, Ekren and Zhang. The transform is inverted term by term into series of Gaussian and complementary error function kernels. Optimality reduces to the signs of 41 one-variable Gaussian series. These signs are certified by Poisson summation, first-mode domination and interval arithmetic on 1616 rational cells, and the proofs and certificates are formalized in Lean.
Results
An explicit solution is given for five experts. The rank strategy (1,0,1,0,0) is globally optimal, and COMB (1,0,1,0,1) is optimal exactly where x1=x2 and x3=x4.
