Skip to content

Proof Checking: Not Line by Line

June 13, 2020

Proofs and perpetual motion machines

Leonardo da Vinci is, of course, famous for his paintings and drawings, but was also interested in inventions, and in various parts of science including mathematics and engineering. It is hard to imagine that he died over 500 years ago, given his continued impact on our world. He invented practical and impractical inventions: musical instruments, a mechanical knight, hydraulic pumps, reversible crank mechanisms, finned mortar shells, and a steam cannon.

Today I wish to discuss proofs and perpetual motion machines.

You might ask: What do proofs and perpetual motion machines have in common? Proofs refer to math proofs that claim to solve open problems like P {\neq} NP. Ken and I get such claims all time. I take a look at them, not because I think they are likely to be correct. Rather because I am interested in understanding how people think.

I started to work on discussing such proofs when I realized that such “proofs” are related to claims about perpetual motion machines. Let’s see how.

Perpetual Motion Machines

A perpetual motion machine is a machine that operates indefinitely without an energy source. This kind of machine is impossible, as da Vinci knew already:

Oh ye seekers after perpetual motion, how many vain chimeras have you pursued? Go and take your place with the alchemists.
—da Vinci, 1494

I like this statement about applying for US patents on such machines:

Proposals for such inoperable machines have become so common that the United States Patent and Trademark Office (USPTO) has made an official policy of refusing to grant patents for perpetual motion machines without a working model.

Here is a classic attempt at perpetual motion: The motion goes on “forever” since the right side floats up and the left side falls down.

The analogy of proofs and to perpetual motion machines is: The debunking such a machine is not done by looking carefully at each gear and lever to see why the machine fails to work. Rather is done like this:

Your machine violates the fundamental laws of thermodynamics and is thus impossible.

Candidate machines are not studied to find the exact flaw in their design. The force of fundamental laws allows a sweeping, simple, and powerful argument against them. There are similar ideas in checking a proof. Let’s take a look at them.


Claims are made about proofs of open problems all the time. Often these are made for solutions to famous open problems, like P{\neq}NP or the Riemann Hypothesis (RH).

Math proofs are used to try to get to the truth. As we said before proofs are only as good as the assumptions made and the rules invoked. The beauty of the proof concept is that arguments can be checked, even long and complex ones. If the assumptions and the rules are correct, then no matter how strange the conclusion is, it must be true.

For example:

{\bullet } The Riemann rearrangement theorem. A sum

\displaystyle  a_{1} + a_{2} + a_{3} + \dots

that is conditionally convergent can be reordered to yield any number. Thus there is series

\displaystyle  b_{1} + b_{2} + b_{3} + \dots

that sums conditionally to your favorite number {M} and yet the {b_{1},b_{2},\dots} is just a arrangement of the {a_{1},a_{2},\dots}. This says that addition is not commutative for infinite series.

{\bullet } Cover the largest triangle by two unit squares: what is the best? The following shows that it is unexpected:

The point of a proof is that it is a series of small steps. If each step is correct, then the whole is correct. But in practice proofs are often checked in other ways.

Checking Proofs

The starting point for my thoughts—joined here with Ken’s—are these two issues:

  1. A proof that only has many small steps but no global picture is hard to motivate.

  2. A proof with complex logic at the high level is hard to understand.

Note that a deep, hard theorem can still have straightforward logic. A famous theorem of Littlewood has for its proof the structure:

  • Case the RH is false: Then {\dots}

  • Case the RH is true: Then {\dots}

The RH-false case takes under a page. The benefit with this logic is that one gets to assume RH for the rest. The strategy for the famous proof by Andrew Wiles of Fermat’s Last Theorem (FLT)—incorporating the all-important fix by Richard Taylor—has this structure:

  • If {X} then {Y}.

  • If not-{X} then {Z}.

  • {Y} implies FLT.

  • {Z} implies FLT.

Wiles had done the last step long before but had put aside since he didn’t know how to get {Z}. The key was framing {X} so that it enabled bridged the gap in his originally-announced proof while its negation enabled the older proof.

Thus what we should seek are proofs with simple logic at the high level that breaks into cases or into sequential sub-goals so that the proof is a chain or relatively few of those goals.

Shapes and Barriers

This makes Ken and I think again about an old paper by Juris Hartmanis with his students Richard Chang, Desh Ranjan, and Pankaj Rohatgi in the May 1990 Bulletin of the EATCS titled, “On IP=PSPACE and Theorems With Narrow Proofs.” Ken’s post on it included this nice diagram of what the paper calls “shapes of proofs”:

Ken’s thought now is that this taxonomy needs to be augmented with a proof shape corresponding to certain classes believed to be properly below polynomial time—classes within the NC hierarchy. Those proofs branch at the top into manageable-size subcases, and/or have a limited number of sequential stages, where each stage may be wide but is shallow in its chains of dependencies. Call this shape a “macro-tree.”

The difference between the macro-tree shape and the sequential shapes pictured above is neatly captured by Ashley Ahlin on a page about “Reading Theorems”:

Note that, in some ways, the easiest way to read a proof is to check that each step follows from the previous ones. This is a bit like following a game of chess by checking to see that each move was legal, or like running a spell-checker on an essay. It’s important, and necessary, but it’s not really the point. … The problem with this is that you are unlikely to remember anything about how to prove the theorem, if you’ve only read in this manner. Once you’re read a theorem and its proof, you can go back and ask some questions to help synthesize your understanding.

The other high-level structure that a proof needs to make evident—before seeing it is reasonable to expend the effort to check it—is shaped by barriers. We have touched on this topic several times but maybe have not stated it full on for P versus NP. A recent essay for a course led by Li-Yang Tan at Stanford does so in just a few pages. A proof should state up front how it works around barriers, and this alone makes its strategy easier to follow.

The idea of barriers extends outside P versus NP, of course. Peter Scholze seems to be invoking it in a comment two months ago in a post by Peter Woit in April on the status of Shinichi Mochizuki’s claimed proof of the ABC conjecture:

I may have not expressed this clearly enough in my manuscript with Stix, but there is just no way that anything like what Mochizuki does can work. … The reason it cannot work is a[nother] theorem of Mochizuki himself. … If the above claims [which are negated by the theorem] would have been true, I would see how Mochizuki’s strategy might have a nonzero chance of succeeding. …

Thus what Ken and I conclude is that in order for a proof to be checkable chunk by chunk—not line by line—it needs to have:

  1. A top-level decomposition into a relatively small number of components and stages—like legs in a sailing race—and

  2. A demonstration of how the stages navigate around known barriers.

Lack of a clear plan in the first already says the proof attempt cannot avoid being snagged on a barrier, as surely as natural laws prevent building a perpetual-motion machine.

Open Problems

Does this help in ascertaining what shape a proof that resolves the P versus NP problem must have?

12 Comments leave one →
  1. June 14, 2020 2:48 am

    It is hard to imagine that he died over 500 years ago, given his continued impact on our world. Despite his famous paintings he was also interested in inventions. We havent yet discovered more interesting facts about him. I know he was a real mastermind. Suprisingly Da Vinci was good at mathematics and engineering. He was truly talented

  2. June 14, 2020 7:32 am

    Dear Dick/Ken,

    Here’s a place where I explore several different shapes of proofs within propositional calculus deriving from the graphical systems of Charles S. Peirce and G. Spencer Brown.

    Propositional Equation Reasoning Systems • Analysis of Contingent Propositions

    I don’t know whether that helps any with \mathrm{P} \overset{\underset{?}{}}{=} \mathrm{NP} but it does supply a lot of nice pictures to contemplate.



    • rjlipton permalink*
      June 14, 2020 1:59 pm

      Dear Jon:

      Thanks as always. I will check this out…

      Best and be safe


  3. Gabriel permalink
    June 14, 2020 7:41 pm

    Thanks for the post!
    I agree with the ideas suggested and think they are very interesting.

    Regarding a “top-level decomposition” I think using structured proofs à la Leslie Lamport
    (they are presented here: ) is a nice way to keep the proof organized and hierarchically clear.

    If you have time.. what do you think?



  4. Peter Gerdes permalink
    June 15, 2020 6:28 am

    I’ve long thought that it would be very beneficial to give some kind of quantitative theory about the extent to which multiple levels of abstraction can simplify complexity. For instance, if you require each level to be a formal proof system (eg a computable language such that an accepted input corresponds to a valid proof of some claim) and bound the length of the program which must probably translate proofs at level n to proofs at level n-1 with level 0 being say first order Peano arithmetic how does the length of the shortest proof of a claim at level n vary with n. In other words try to quantitatively estimate how much abstraction is able to turn long proofs into short ones.

    This matters because in the sciences one often hears arguments about the attractiveness of a theory based on its simplicity but if the function relating proof length at level n to level 0 grows quickly with b that argument isn’t as strong.

    Also I suspect results about lower bounds on space complexity for nondeterministic machines give limits on the extent you can hope to do this. After all after verifying the reduction from level n to n-1 you can toss out the description of level n-1 so if you can ultimately prove/compute using short descriptions at level n and each level transition can be checked in small space you’ve given a non-deterministic algorithm for solving the problem in small space.

  5. June 15, 2020 9:09 am

    Meanwhile, even in elementary geometry its
    still possible to found gaps.
    I’ve discovered two following elegant theorems;

    Notice, that the second one can be similarly
    obtained for 4 and 6-sided polygon, not just for triangle,
    and even generalized for n-dimension hypercube.

  6. Ralf Wüsthofen permalink
    June 21, 2020 5:43 pm

    Dear Dick/Ken,

    Your considerations about “shapes and barriers” make sense, but when you refer to “solutions to famous open problems”, one important psychological aspect is missing here:

    In such a case, most readers are not prepared to read the proof by simply checking if each step follows from the previous ones. Instead, they start by their own probabilistic “reasoning” that the proof MUST be wrong. Of course, such an attitude isn’t that helpful and it already undermines the reader’s willingness to really want to understand.

    A prime example for this phenomenon is this (almost) trivial proof of the Goldbach conjecture

    Click to access 2004.0683v8.pdf

    that is circulating a long time. Moreover, here it seems that the “willingness” of some professionals is also influenced by the taboo outcome that the solution immediately leads to an arithmetic antinomy, i.e. to the inconsistency of arithmetic.



  1. Proof Checking: Not Line by Line – 備忘6
  2. === === popular today
  3. Animated Logical Graphs • 32 | Inquiry Into Inquiry
  4. P<NP | Gödel's Lost Letter and P=NP

Leave a Reply

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

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

Google photo

You are commenting using your Google 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 )

Connecting to %s