(Also posted on the Reddit thread)
I think the example is broken.
To see why, notice that we are dealing with field elements, not integers. Field elements are integers modulo
p. In the Ethereum case,
p = 21888242871839275222246405745257275088696311157297823662689037894645226208583. We can make a fake proof that a nontrivial
x * y = z by supplying any witnesses
y such that
x * y = p * k + z for some integer
k; the field math "wraps around". For example, I can show that 5 is "non-prime" via
x = 7 and
y = 18761351033005093047639776353077664361739695277683848853733461052553051035929, which equals 6 * p + 5 in regular arithmetic, but equals 5 in field arithmetic because of how it wraps around.
To solve this, I think you need to have an inequality check that
y are both less than
sqrt(p) (or, better yet, less than
z). So unfortunately the number of constraints will be ~1600 after all.