I assume you'd want to prove common-sense invariants, like "you can't be taxed more than your income" or "tax credit 123-45 is worth more for two children than for one". Lean might disprove a few of these, and the counterexamples are potential loopholes.
Well put. A similar way to say it: ask the 9 year old to draw ALL of the possible lines connecting two points in the set — of course this is possible, just might take awhile. The theorem says that at least one of the lines drawn must hit ONLY the two points the 9 year old used when drawing that particular line, not any others.
I just thought of another way to restate. Suppose you give me any finite set of points, any finite set at all, and you also tell me that when the 9 year old draws any line through any two of them, she will always hit a third. Then I can immediately conclude all the points lie on a single line, that is, that any line the 9 year old draws will hit all the points.
reply