The finite-horizon five-expert prediction problem

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 x1=x2 and x3=x4. 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.