Comment by LegionMammal978

To be fair, in the most literal sense, the vast majority of syntactically-valid statements in a typical FOL encoding will be trivial. One of my side-projects has been trying to find the shortest statements independent of ZF and some of its fragments. In fact, for every slightly nontrivial statement that requires actually building a construction, there are billions more that can be instantly solved via a few simplifications, and statically pruning the search tree a bit is the best we can do.

To actually get independence, we need very rigid statements that don't allow any simple way to fudge a solution or counterexample. If anything, statements that mathematicians (and programmers) care about are biased toward undecidability, simply because they're extremely biased toward nontriviality. We put in the hard work of building towers of rigid definitions to that effect.