Can we quantify “nonconstructive advantage”?

Japan Times source

Péter Frankl has been in the news again this year. The news is substantial partial progress on his famous conjecture that for any finite family of nonempty sets that is closed under union, some element must belong to at least half of the sets. The progress shows that some must belong to at least of the sets, but does not tell you how to find .

Today, amid twelve days of gift-giving, we wonder why nonconstructive proofs are often easier than constructive ones—and by how much?

Another reason for mentioning Frankl is that he and Laci Babai wrote a wonderful resource titled “Linear Algebra Methods in Combinatorics.” Many of these methods are nonconstructive. They figure into our story at the end.

A Simple Example

Here is a simple example of a nonconstructive proof. Suppose you and a loved one are sharing a holiday chocolate bar.

Nutrition source

At each turn you break off a square and get all squares between it and the unwrapped corner. The goal is to leave your partner the last square. The game is called Chomp and was popularized by Martin Gardner in the 1970s.

The theorem is that the first player always has a winning strategy, for a bar of any dimensions other than . For suppose the second player could win. Then the second player would have a winning move in reply to the first player taking just the single square in the open corner. But any such move is also legal for the first player to begin with. The reasoning in full is:

• : For any size bar, one or the other player must have a winning strategy.
• : If the second player has the winning strategy, then the first player does—as reasoned above.
• : Hence the first player can always win.

This proof, however, does not tell you how the first player can win. It does not help you calculate a winning move. This makes it nonconstructive.

Quantifying Nonconstructive Advantage

Some sizes of chocolate bar have an easily calculable winning strategy. If the bar is square, for any , then the first player has a rather greedy winning move: chomp squares, leaving an L-shape with equal arms one square thick. Then whatever your partner plays in one arm you can mimic in the other arm, until your partner must take the opposite corner square.

For other dimensions , and for versions of this game in more than two dimensions, a winning move is not so easy to specify. Nor is it easy to verify even if guessed. Whereas, the above nonconstructive proof takes some fixed finite amount of computational effort to formalize in an automated proof system such as Coq or Leda or . This leads to our first thought on quantifying the ease of the nonconstructive proof:

For which tuples is less than the effort needed to find a winning first move in Chomp?

Here we mean to be the effort beyond that needed to specify the input . Note that any move will be a similar size tuple as .

The Frankl conjecture setting gives us a similar idea. For certain constants in the neighborhood of , the nonconstructive proof is quite short, for instance the 3-page paper by Zachary Chase and Shachar Lovett. Much other news has been collected by our friend Gil Kalai here and here. This prompts us to ask:

For which finite union-closed set systems is the effort needed to find an that belongs to at least of the sets greater than the one-shot effort of the nonconstructive proof?

To quantify , we need some concrete finite measure of complexity, not an asymptotic one. Notions of Kolmogorov complexity spring first to mind, but there are some caveats which we discuss next.

Kolmogorov Complexity Versus Verifying

Our friend Harvey Friedman put this point in a really nice and crisp way recently here in Plus Magazine, an e-publication that highlights the mathematical kernels of real-life developments. He raises Roth’s theorem and Faltings’s theorem as examples:

Both [theorems] assert that certain equations or inequalities in one or more unknowns have at most finitely many solutions. The constructivist wants to have a procedure for being able to list these solutions. …

For both theorems, we have a proof that there exists a whole number such that all of the solutions to the given equation or inequality can be expressed with fewer than that many digits. But we have no constructive proof of the existence of this whole number.

We covered Harvey’s research on the concrete face of undecidability here and here. The above quotation suggested to us the idea of comparing the complexity of the nonconstructive proof with the classical Kolmogorov complexity of the list of solutions. A subtlety here is that we can recursively enumerate solutions, but it is hard to calculate the fact of knowing when the enumeration is over. So the complexity of the whole number bound mentioned by Harvey enters in.

Youtube videos of piano and lectures

The issue, however, is that the bound can be a huge number that is innately simple. The complexity of its association to Roth’s theorem or to Faltings’s theorem is harder to capture.

A second issue complicates the Kolmogorov idea for Chomp. Suppose we want to define to be the classical Kolmogorov complexity of given , i.e., . The rub is that here we can define, say, the lexicographically least winning move as a computable function of . Thus . Perhaps more precisely, , where is the size of describing the rules of the game Chomp to the universal Turing machine underlying the metric . We can take for granted that the cost of this description is subsumed in the total effort for the proof, so that . This still says that classical Kolmogorov complexity is not adding anything.

We thus need to consider resource-bounded notions of Kolmogorov complexity. Doing so still leaves the first issue, however: Specifying as a tuple might not carry any association to the game. There may be that have a winning move like which are simple numbers but not in relation to and .

This takes us back to another complexity idea: the cost of verifying. Here the Frankl example helps most. We can associate to via the task of verifying that belongs to of the sets . We suppose this cost is linear in , whereas brute-force testing each of points would take time order-of . We put the verification cost in the same ledger as the fixed cost of the nonconstructive proof, opposite the true time to find an . Then the nonconstructive advantage just becomes a standard “NP vs. P”-type idea, but at the level of linear time.

The Nonconstructive Goody Bag

What prompted us to think again about the ease of nonconstructive proofs is a recent claim by David Jackson and Bruce Richmond to have found a nonconstructive proof of the Four-Color Theorem. The point is that their claimed proof is short, under ten pages. Whereas, the original proof by Kenneth Appel and Wolfgang Haken back in 1977 was monstruous and completely uncheckable by hand, a situation that has improved much but not fully since. See their book.

There are unfortunately numerous issues with their recent paper. Those have been collected by John Carlos Baez here. But its strategy is still noteworthy. They say:

The following assertion is to be proved. If there is a set of maps that can be 4-coloured and if the number of these maps with edges is a positive fraction of the number of all maps with edges, then there is no map that cannot be 4-coloured.

What we like about their new claimed proof is that it needs only prove a weaker statement: Roughly that a positive fraction of planar graphs can be 4-colored. This suggest that one might be able to prove a simpler result. I, Dick, wondered whether one might be able to use the separator type theorem to show most planar graphs are 4-colorable. For a few minutes I had an idea that seemed possible: But alas it fails. Incidentally, there was a similar nonconstructive proof claim of for Frankl, but we have not seen it discussed.

Noga Alon wrote a really nice survey titled “Nonconstructive Proofs in Combinatorics.” One example is the following theorem

Theorem 1 Every graph of maximum degree 5 and average degree greater than 4 contains a 3-regular subgraph.

The proof does not tell you how to find this subgraph. Rather it uses algebraic tools and applies the Chevalley-Warning Theorem, which we discussed a long time ago here. I, Dick, myself teamed with Noga and others to prove a related result here.

The point is that these results exemplify the goody bag of nonconstructive methods, even for theorems in the areas of mathematics that verge most on concrete computation. Enumerative methods, generating functions, probabilistic analysis, and the algebraic methods exemplified by Frankl and Babai, have all been wonderful gifts.

There is a basic distinction that may also bear stronger delineation. This is between nonconstructive proofs that an object exists and such proofs that an object doesn’t exist. The 4-color idea is the latter variety. We suppose the existence of a non-4-colorable map and derive a contradiction. The strategy for proving Fermat’s Last Theorem that was refined by Ken Ribet and others before Andrew Wiles and Paul Taylor brought it to fruition also has this nature: If a nontrivial solution with exists, then a certain kind of elliptic curve must exist. But the latter can be shown to lead to a contradiction.

Open Problems

Can the strategy for a short nonconstructive proof of the four-color theorem be made to work? Will the analytical ideas underlying the recent progress on Frankl’s conjecture prove its full form? And can we refine our ideas of quantifying the advantage achieved by these proof techniques? Perhaps even relate it to “quantum advantage”?

It strikes us that there should be a short non-constructive proof of the 5 color theorem along the lines of Jackson and Richmond’s paper, though it may require some of the same fixup.