Skip to content

Proof Envy

June 11, 2014


I wish I could have used Theorem X…

vijayaramachandran
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:

  1. Look at a chip and determine the wires that were too long and were slowing down the chip.

  2. 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:

  1. Look at a chip and determine the wires that were long and were slowing down the chip.

  2. Resize their respective drivers so that they would go faster.

  3. 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:

{\bullet } 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.

{\bullet } 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 {F} is a polynomial function from {\mathbb{C}^{n}} to {\mathbb{C}^{n}} and {F} is injective then {F} 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.

{\bullet } 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.

{\bullet } 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.

{\bullet} 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 {\mathsf{P \neq NP}} 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?

8 Comments leave one →
  1. June 11, 2014 3:57 pm

    all simple groups are even order
    or prime order (Cyclic groups)

  2. Serge permalink
    June 11, 2014 4:38 pm

    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!”🙂

  3. June 11, 2014 5:02 pm

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

  4. June 11, 2014 6:11 pm

    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.)

  5. gasarcg permalink
    June 11, 2014 9:50 pm

    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.

    • Colin permalink
      June 15, 2014 12:01 am

      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.

  6. Max permalink
    June 12, 2014 3:34 am

    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)?

  7. June 15, 2014 9:29 am

    Pip asks  “Do you ever feel theorem-envy? Which theorems would you like to use?”

    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 Technology

    Looming Shift in Supercomputing
    by Graham Warwick, 19 May, 2014

    Exascale computing — machines 1,000 times faster than today’s fastest supercomputers — will be prohibitively power-hungry without a fundamental change in how they operate.

    Today’s top supercomputers consume around a watt of electricity for every 2 gigaflops of computing power [such that] exascale computations will need at least 500 megawatts — the Energy Department estimates 1-2 gigawatts — which would cost $300-500 million a year for power.

    A Natural Proposition  Supposing 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 one doubling 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 Dynamics  Exascale computations commonly are simulations broadly conceived, whose mathematical frameworks are presently set forth in magisterial textbooks such as Bird, Stewart, and Lightfoot’s Transport Phenomena, Frenkel and Smit’s Understanding Molecular Simulation, Nielsen and Chuang’s Quantum Computation and Quantum Information, and Kloeden and Platen’s Numerical 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 corpus of 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’ Book originates equally in their enchanting naturality, and in their pedagogic concision, and in their inspiration for practical enterprise.

    Broadening Appreciations of Naturality  Our 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 Naturality  In 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 Question  Theorem envy is a natural and healthy expression of the Enchantment of Naturality.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s