# Proof Envy

* I wish I could have used Theorem X… *

IISC centenary source |

Vijaya Ramachandran is now the Blakemore Regents Professor of Computer Science at The University of Texas at Austin. Once upon a time she was my PhD student, at Princeton, working on the theory of VLSI chip design. Long ago she moved successfully into other areas of theory. She became a leader in cache oblivious algorithms, an area created by Charles Leiserson, whom I advised as an undergraduate many years ago. It’s a small world.

Today I want to talk about theorems, old theorems and new, that I wish I could have used in a paper.

Call the phenomenon *theorem envy*: There are theorems that I have long known, but have never been able to use in any actual paper, in any proof of my own. I find this curiously unsatisfying, to know a cool result and yet be unable to use it in one of my papers. Perhaps I am alone in having this feeling, perhaps you only care about solving your problem, not how you solve it. Mostly I would agree with that. But part of me would like to use Theorem X in one of my papers. It just seems like it would be cool to do that.

This isn’t about envying those who originally proved the theorems. It’s about those who actually use the big gear in their toolboxes. We may have lots of shiny gadgets in our boxes, but part reason they’re shiny is they haven’t been used.

## Stirring the Brew

I realized this years ago when Ramachandran was working on her thesis. One of her results solved a problem that most had ignored—could not solve—about the cost of resizing drivers to make a chip go faster. One way to make a signal propagate faster across a chip is to use more power: the larger the driver, the faster the signal can move. This remains as significant today as then. The issue is not the speed-of-light restriction, but is related to the time it takes to charge a capacitive load:more power makes it happen faster. The downside then, and much worse today, is the added heat that power causes.

There is a curious cyclic issue in resizing drivers. The approach was in two steps:

- Look at a chip and determine the wires that were too long and were slowing down the chip.
- Resize their respective drivers so that they would go faster.

In practice this worked quite well. Yet there is a subtle bug: the resizing of the drivers moves parts of the chip, and this can make some wires become new bottlenecks. The obvious answer is to do the following:

- Look at a chip and determine the wires that were long and were slowing down the chip.
- Resize their respective drivers so that they would go faster.
- Look at the chip, and if it is still slow repeat step 1.

The theoretical question is, does this process actually ever stop? Is it possible that the chip just blows up and thus no resizing will make it go faster? Or is this unlikely or even impossible?

The answer is that using the famous Brouwer Fixed-Point Theorem, Ramachandran was able to prove that this cannot happen. She showed that given some reasonable restrictions on the chip topology, the process becomes a continuous function on a convex compact set, which by the theorem has a fixed point. Brouwer means “brewer” in Dutch, and one way to visualize is stirring a brew in a pot—as opposed to a torus where the flow can go around with no vortex. The analysis also needs and shows quick convergence, but the essence is that things stop because the resizing operation has a fixed point.

I like her result. In my opinion its practical impact was shedding light on CAD, but I liked it even more because it used the wonderful Brouwer Fixed-Point Theorem. I never have been able to use that in any of *my* papers. Oh well.

So let me give a few other examples of other theorems that I would still like to get a chance to use in some future paper.

## A List

Here is a partial list of my top few:

*Regularity Lemma*. The famous Szemerédi regularity lemma states that every large enough graph can be divided into subsets of about the same size so that the edges between different subsets behave almost randomly. It was proved in a weaker form by Endre Szemerédi and used to prove his famous theorem on arithmetic progressions.

I have known it for many years, but have never been able to use it in my work. Of course many others have used it in their work. I would still like to be able to use it.

*Ax—Grothendieck theorem*. This is a famous theorem about the relationship between injectivity and surjectivity of multi-variate polynomials. It was proved independently by James Ax and Alexander Grothendieck. One version of the theorem is that if is a polynomial function from to and is injective then is bijective.

The full theorem is more general, and what’s remarkable is that the basic mechanism of the proof is really quite simple. It relies on the fact that injective implies surjective for finite sets: a map that is one-to-one on a finite set must be onto. I believe this should be useful in problems that concern polynomials, which after all is one of our main objects of study in complexity theory.

*Baire Category Theorem*. This is the famous theorem of René-Louis Baire, who proved it is in his 1899 doctoral thesis. It is an existence theorem showing that any countable family of open and everywhere-dense sets in a complete metric space has a non-empty intersection. It has been used in topology and analysis to prove the existence if many wonderful and exotic objects.

In our world we often prove the existence of exotic objects via the probabilistic method, but the Baire Category Theorem is another different method. It has constructive versions in certain settings, and complexity theorists have used them to show that certain oracle constructions are generic. I believe there should be some further interesting applications of it, and still hope to use it someday.

*Feit-Thompson theorem*: this is the famous theorem that every odd order group is solvable. It was proved by Walter Feit and John Thompson in the early 1960’s. It is a cornerstone to the understanding and eventual classification of finite simple groups: it implies that all simple groups are even order.

I have always thought that there might be some deep connection between this theorem and our inability in complexity theory to understand the power of computations modulo composites, but have never been able to make this idea into a theorem.

*Hilbert’s Nullstellensatz*. This does get applied, as we noted here. The cool German name is enough to induce envy. Particularly interesting are various effective and combinatorial forms of it.

This also stands for theorems in polynomial ideal theory and algebraic geometry in general, as used e.g. by Ketan Mulmuley and Milind Sohoni in their attack on type questions, and by Craig Gentry in crypto for some schemes of fully homomorphic encryption.

## Open Problems

Do you ever feel theorem envy? Which theorems would you like to use? Am I unique and alone in this affliction? Is there a cure?

all simple groups are even order

or prime order (Cyclic groups)

A cure for theorem envy ? I guess it’s what they call an axiom, a hypothesis, a conjecture, a phenomenon… Just repeat after me: “that’s the way it is!” 🙂

I thought the Brouwer Fixed-Point Theorem was proven unstable.

it seems you may have omitted some youve already mentioned in your blog. for example gromovs thm relates group theory & polynomial growth in a rare structural result giving sufficient/necessary conditions for a polynomial growth (& great blog on that). defn have proof envy on this one & seems like it ought to tie into TCS in some big way… ❓ 💡 ❗

also szemeredi’s thm has interested me also. its a big deal given that he got the $1M abel prize in part for it. this also caused some semimajor angst in mathematical circles because szemeredis work was more combinatorial than topological. (a possible paradigm shift/ phase transition going on in mathematics reaching the highest echelons.)

I envy Chandra-Furst-Lipton for being able to use a corollary of the multi-dim Van Der Warden theorem in their paper on multiparty protocols (STOC 1983).

Joel Spencer said that there are some theorems that just like you’d use them all the time but

you never seem to. Example: Every group is a group of perms. Group theorists must use this all the time. Alas, they rarely do. Another Example: Every number is the sum of at most four squares. Number theorists must use that all the time. Alas, they rarely due.

Cayley’s theorem is the opposite of a useless result – it’s so basic and deeply ingrained in group theory that its use becomes invisible. It’s the first line in a whole list of analogies between abstract groups and groups of symmetries.

Could you please provide a link to Ramachandran’s paper that uses the Brouwer Fixed-Point Theorem (or at least the title of the paper)?

In engineering contexts, what Pip calls “theorem envy” commonly manifests itself as the

Enchantment of Naturality:the desire and dream that complex systems can find elegant explanations within mathematically natural frameworks.Our consideration of the enchantment of naturality will be guided by Twain’s maxim “the humorous story is told gravely” and its by dual “the grave story is told humorously.”

To start, the enchanting naturality of Vijaya Ramachandran’s computational power metric is evident in a recent story in

Aviation Week & Space TechnologyA Natural PropositionSupposing that exascale computing comes to pass (as foreseen by research funding agencies), then each doubling of algorithmic efficiency will acquire a concrete monetary value of $300M-500M … an amount that nicely doubles the $237M budget of the NSF’s Division of Mathematical Sciences.Thus it is naturally evident that even

onedoubling of exascale algorithmic efficiency has sufficient power-value to support 3000-5000 mathematical researchers in perpetuity.We therefore wonder: How might the researches of next-generation exascale-enterprise mathematicians be coordinated with sufficient laxity as to allow ample scope for creativity, and yet sufficient discipline as to foster exascale enterprises?

The Enchanting Naturality of DynamicsExascale computations commonly are simulations broadly conceived, whose mathematical frameworks are presently set forth in magisterial textbooks such as Bird, Stewart, and Lightfoot’sTransport Phenomena, Frenkel and Smit’sUnderstanding Molecular Simulation, Nielsen and Chuang’sQuantum Computation and Quantum Information, and Kloeden and Platen’sNumerical Solution of Stochastic Differential Equations; such that the physical elements of dynamics are encompassed in (say) 10,000 pages of (say) ten-or-twenty graduate-level textbooks.It has to be said, however, that these books aren’t individually easy for students to read. Moreover, students often find that understanding any one of them doesn’t help all that much with understanding the others.

Geometry helps greatly to naturalize and unify the disparate physical elements of these textbooks, and toward this end mathematicians have blessed us (already) with Euclidean, Riemmannian, affine, symplectic, and algebraic notions of geometry; moreover in each decade striking new geometric notions are synthesized (see for example Terry Tao’s survey “Algebraic combinatorial geometry …”, arXiv:1310.6482).

This accelerating appreciation of mathematical naturality is good news, because otherwise 21st century students will scarcely be able to assimilate the accelerating extensions of our already-vast physical understanding. The prospect of rewriting and unifying the disorganized

corpusof 20th century textbooks is perhaps the chief ingredient in the enchantment of naturality. It’s true that a lot of 20th century textbooks need rewriting, but on the other hand, $500M/year suffices to support a lot of textbook-writing.In a nutshell, the mathematical beauty of the proofs in Erdős’

Bookoriginates equally in their enchanting naturality, and in their pedagogic concision, and in their inspiration for practical enterprise.Broadening Appreciations of NaturalityOur century’s sustained accelerations in computational capacity and in physical understanding are accompanied too by an broadening appreciation of mathematical naturality, that holds forth the promise of explaining what exascale computing is really all about … which for young students (especially), is the thrilling new enterprises and abundant family-supporting jobs that exascale computing promises to foster.The Enchantment of NaturalityIn aggregate, the preceding considerations suggest that mathematical naturality — and the theorems that are its distilled essence — is an enchantment both pragmatic and platonic; that provides a language not solely for proofs, but for education and enterprises too.An Answer to Pip’s QuestionTheorem envy is a natural and healthy expression of the Enchantment of Naturality.