And yes, the point is not to construct theorems with ridiculously long proofs, the point is to proof the statements posed by mathematicians which attracted the

And yes, the point is not to construct theorems with ridiculously long proofs, the point is to proof the statements posed by mathematicians which attracted the interest of mathematicians. From this perspective, the proofs for the bounds found in both cases are the only available proofs and that is why the size is an interesting aspect. Notice that in EDP case, remarkable Tao's proof for the general case does not give an explicit bound close enough to computed using SAT proofs for a particular case (C=2).