Proof Checking: Not Line by Line
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 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.
Proofs
Claims are made about proofs of open problems all the time. Often these are made for solutions to famous open problems, like PNP 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:
The Riemann rearrangement theorem. A sum
that is conditionally convergent can be reordered to yield any number. Thus there is series
that sums conditionally to your favorite number and yet the
is just a arrangement of the
. This says that addition is not commutative for infinite series.
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:
- A proof that only has many small steps but no global picture is hard to motivate.
- 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
-
Case the RH is true: Then
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
then
.
-
If not-
then
.
-
implies FLT.
-
implies FLT.
Wiles had done the last step long before but had put aside since he didn’t know how to get . The key was framing
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:
- A top-level decomposition into a relatively small number of components and stages—like legs in a sailing race—and
- 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?
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 incatalog.kz
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
but it does supply a lot of nice pictures to contemplate.
Regards,
Jon
Dear Jon:
Thanks as always. I will check this out…
Best and be safe
Dick
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: https://lamport.azurewebsites.net/pubs/proof.pdf ) is a nice way to keep the proof organized and hierarchically clear.
If you have time.. what do you think?
Regards,
Gabriel.
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.
Meanwhile, even in elementary geometry its
still possible to found gaps.
I’ve discovered two following elegant theorems;
https://vixra.org/abs/1909.0638
https://vixra.org/abs/1909.0028
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.
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
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.
Regards,
Ralf
Why doesn’t the link appear in the above post? Here it is again:
https://vixra.org/abs/2004.0683