(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 `x`

and `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 `x`

and `y`

are both less than `sqrt(p)`

(or, better yet, less than `z`

). So unfortunately the number of constraints will be ~1600 after all.