This is Manuel Kauers' solution to the challenge raised in

https://sites.math.rutgers.edu/~zeilberg/tokhniot/MKchallenge.txt

A donation to the OEIS in honor of Manuel Kauers has been made
(see https://oeisf.org/donate/#DONATE)

------------------------
Your new polynomial P is nonnegative for all x,y,z>=0.

Here is why.

First, if you write your polynomial in powers of (x-1), (y-3/2), and
(z-1/2) instead of in powers of x, y, z, you will find that all
coefficients are nonnegative. This implies that P(x,y,z)>=0 whenever
x>=1, y>=3/2, and z>=1/2.

For the range 0<=x<=1 and y,z>=0, view P as polynomial in y, z with
coefficients that are polynomials in x. Replace each of these
coefficients by its minimum in the range 0<=x<=1 (rounded down to the
next integer for convenience). This gives a polynomial Q in y, z such
that P >= Q for all 0<=x<=1 and all y,z. Collins's algorithm finds
that Q >= 0 for all y,z >= 0, except for some points in the box [1/2,
17/10] x [3/10, 3/2]. We can conclude that in the range 0<=x<=1, we
have P>=0 unless perhaps for some (y,z) in [1/2, 8/5] x [3/10, 3/2].

For the range 0<=y<=3/2, we find in the same way that P>=0 unless
perhaps for (x,z) in [1/4,27/10] x [0,9/10].

For the range 0<=z<=1/2, we find in the same way that P>=0 unless
perhaps for (x,z) in [0,11] x [0, 8].

Altogether, we have shown P>=0 for all points (x,y,z) outside the
union of three finite boxes:
[0,1] x [1/2,17/10] x [3/10,3/2] union [1/4,27/10] x [0,3/2] x
[0,9/10] union [0,11] x [0,8] x [0,1/2].

It remains to check what's going on in these boxes. Let's merge them
to [0,11]x[0,8]x[0,2]. The bivariate polynomials obtained from P by
setting x=0 or x=11 or y=0 or y=8 or z=0 or z=2 are positive in the
box. In other words, P is positive on the boundary. If P is negative
somewhere in the interior, there must be some real roots.

By Decartes' rule of signs, the number of positive real roots of a
univariate polynomial is bounded by the number of sign changes in its
coefficient list. Reading P as polynomial in z with coefficients in
x,y, we can use Collins's algorithm to show that for (x,y) in
[0,11]x[0,8] \ [0,2]x[0,2], all coefficients are positive, so there
can't be any roots in this range. This reduces the critical box to
[0,2]^3.

We can reduce the box even further. Reading P(x,y,z+1+1/10000) as
polynomial in z with coefficients in x,y, then for all (x,y) in
[0,2]^2 all coefficients are positive, so there is no root with
z>1+1/10000. Likewise, P has no roots for y>1+1/10000 and no roots for
x>1+1/10000. This reduces the box to [0,1+1/10000]^3.

Since P(1,1,1)=0, we can't reduce much further.

To show that P>=0 in a small box centered at (1,1,1), consider the
Taylor expansion of P around this point. Of course, this is just P
itself, but we want to get something of lower degree because P itself
is too big. So we write P = T + R where T is the Taylor polynomial and
R is the remainder term. Then P >= T - |R|, and we can bound |R| using
the coefficients of P and the textbook formula. A truncation order 4
suffices to show that P >= 0 for all x,y,z with -1/10 < x-1,y-1,z-1 <
1/10.

In the same way, we can show for every i,j=0,...,10 and every
k=3,...,10, that P>=0 in a small cube of side length 1/10 centered at
(i/10,j/10,k/10).

So we are down to [0,1+1/10000]x[0,1+1/10000]x[0,3/10]. Here we can
use the following idea: for a univariate polynomial f(x) = a0 + a1*x +
... + ad*x^d and an e>0, we have f(x) >= a0 - |a1|*e - |a2|*e^2 - ...
- |ad|*e^d for all x in [-e, e]. If the number on the right hand side
is nonnegative, then f is positive in the range [-e, e]. With the
natural extension to three variables, it is possible to show for all
i,j=0...,250 and all k=0...75 that P>=0 in a small cube of side length
1/250 (i.e., e=1/500) centered at (i/250, j/250, k/250).

This completes the proof.

Best wishes,
Manuel