Every positive integer is the sum of 3 palindromes: https://arxiv.org/abs/1602.06208

Resolves YES if a formalization of this paper, in a computer proof assistant, is published before market close.

The paper provides a constructive proof, and the theory of digits and palindromes are well developed in both Coq and Lean. So it’s just a matter of whether someone will bother to do it.

Every positive integer is a sum of three palindromes

For integer $g\ge 5$, we prove that any positive integer can be written as a sum of three palindromes in base $g$.