Mathematicians can code, and even the mathematical conjectures that have plagued mankind for 90 years can’t stop it.
Four mathematicians from Stanford, CMU and other universities directly transformed a mathematical problem into a “violent search” of 1 billion results.
△ Marijn Heule, Assistant Professor of CMU, one of the authors of the paper
They entered this string of codes into a computing cluster composed of 40 computers. After 30 minutes, the computer gave a proof result of 200GB size:
Keller’s conjecture is correct in spaces not exceeding 7 dimensions.
Now, anyone can go to GitHub to clone this code to verify this mathematical theorem.
What’s more reversal is that this program, which won the best paper award of the computer academic conference IJCAR (International Joint Conference on Automatic Reasoning), went online for half a year on GitHub, and only won one star.
So, what exactly is the “Keller Conjecture” that these four mathematicians want to prove? Why have to use computers to prove it? Are the computer-proven results reliable?
Let us come one by one below.
What is Keller’s conjecture
Suppose a batch of identical square tiles are used to cover the ground, leaving no gaps in between. Obviously, the tiles will share an edge, as shown by the blue line in the following figure:
In a 3-dimensional space, if you want to use a cube to fill the space, is it similar to a 2-dimensional space?
Imagine that if you randomly put several cubes in the space like the picture below, and expand to fill the entire space, the only way is to make the connected cubes share the blue surface.
This is true for both 2 and 3 dimensions. What will happen to the higher dimensional space?
In 1930, the German mathematician Keller guessed that if an n-dimensional cube is used to fill an infinite space, there will inevitably be “face to face” between the cubes, which is true for any dimension.
This is Keller’s conjecture.
But mathematical conjectures cannot rely solely on intuition, they must be strictly proven. For 90 years, mathematicians have worked tirelessly.
In 1940, the mathematician Perron proved that Keller’s conjecture was correct in 1 to 6 dimensions.
In 1992, two other mathematicians, Lagarias and Shor, proved that Keller’s conjecture was wrong on a 10-dimensional space.
(Note: This Shor is the mathematician who proposed Shor’s algorithm for solving prime factorization with a quantum computer.)
Unfortunately, Keller’s guess was wrong! However, the problem does not end there.
There are still 3 dimensions left unsolved! Does Keller’s conjecture hold in the three-dimensional space of 7, 8, and 9 dimensions?
As long as these three dimensions are solved, the problems that have entangled mathematicians for decades will be completely solved.
Mathematical arguments show that if Keller’s conjecture is wrong in n-dimensional space, then it must be wrong in dimensions higher than n.
In 2002, the mathematician Mackey proved that Keller’s conjecture does not hold in 8-dimensional space and therefore does not hold in 9-dimensional space.
So far, the 7-dimensional space has become the only problem.
△ CMU Professor Mackey who proved Keller’s conjecture in 8-dimensional space was wrong
Improvement of proof method
Maybe you have discovered that since the 1990s, the speed of proof of Keller’s conjecture has been greatly accelerated. It took mathematicians only 10 years to reduce the problem to three dimensions.
This is mainly due to the contributions of two mathematicians.
Back then, when Perron solved the dimensions 1 to 6, there was no special shortcut. By 1990, the method of proof of Keller’s conjecture had undergone tremendous changes.
Mathematicians Corrádi and Szabó proposed a new way of thinking, turning the original infinite space problem into a finite, discrete problem, and letting the computer solve itKeller’s conjecture is made possible.
They cleverly turned Keller’s conjecture into a graph theory problem, which is to construct the so-called Keller Graph, and graph theory is what computers are good at.
Under the guidance of this method, Lagarias and Shor quickly proved the situation in 10-dimensional space after 2 years: Keller’s conjecture was not valid. After another 10 years, Mackey proved that Keller’s conjecture was not valid in 8-dimensional space.
So, what exactly is the Keller diagram and why can it accelerate the proof of Keller’s conjecture?
Construct “Keller Diagram”
First, let’s start with the simplest 2-dimensional situation.
Now, we have a card with two colored dots drawn on it. The two points are in order and cannot be exchanged. For example, 1 black 2 white ≠ 1 white 2 black.
Two points can be painted in 4 colors in total, and the colors are divided into 2 pairs: red to green, white to black.
Mathematicians have proved that the colors assigned to points are equivalent to the coordinates of a square in space. Whether the colors of the two cards match indicates the relative position of the two squares.
The specific relationship between the color of the point and the square is as follows:
1. The two pairs of points are exactly the same, which means that the two squares are completely overlapped
2. The colors of the two pairs of points are different, and the colors are not matched, which means that the two squares partially overlap.
The Keller diagram with 16 cards depicts all the possibilities for a square to fill a plane.
If Keller’s conjecture is not true in the 2-dimensional space, then we must be able to find 4 squares, which have no shared edges but can be filled together seamlessly. Then copy these 4 squares infinitely on the screen to fill the entire screen.
It’s actually impossible. If you follow this operation, you will only get a filling method with countless pores (the purple part in the figure below).
Corresponding to the Keller diagram, it means to find 4 cards in the diagram, and there is a connection between them. (In mathematics, this is called a complete graph.)
Obviously, in the Keller diagram of the 2-dimensional problem, we cannot find such 4 cards. (You can go to the Keller picture above to find it yourself.)
In this way, we connect the n-dimensional cube and the displacement s with the number n of the card and the logarithm s of the color.
As a more general rule, if you want to prove that the n-dimensional Keller conjecture is wrong, you must find 2n cards in the corresponding Keller diagram, and these cards are connected in pairs.
Because you can’t find a complete graph composed of 4 cards, the Keller’s conjecture in 2D space is correct.
In order to prove Keller’s conjecture in a 3-dimensional space, 216 cards can be used, with 3 points on each card, and 3 pairs of colors can be used (this is relatively flexible). Then, we need to look for 23=8 cards. There are connections between them, but they still cannot be found.
In the 8-dimensional space, we can finally find 256 cards that meet the conditions, so the Keller’s conjecture in the 8-dimensional space is wrong.
A counterexample in △8-dimensional space (a holon subgraph of a Keller diagram)
The next thing is to find a complete subgraph on the Keller graph corresponding to the 7-dimensional space. However, this problem was shelved for 17 years after the 8-dimensional problem was solved.
According to the previous description, to solve the Keller’s conjecture in 8-dimensional space and 10-dimensional space, we need to find 28=256 and 210=1024 cards. Graph, and the 7-dimensional space only needs to find a subgraph of 27=128 cards.
The latter seems to be less difficult, and the 7-dimensional space problem should be simpler! actually not.
Because, in a sense, 8-dimensional and 10-dimensional can be “decomposed” into lower dimensions that are easy to calculate, but 7-dimensional cannot.
Lagarias, who proved the 10-dimensional case, said: “7-dimensional is not good because it is a prime number, which means you cannot decompose it into lower dimensions. So there is no choice but to deal with all combinations of these graphs.”
For the human brain, finding a subgraph with a size of 128 is a difficult task, but this is precisely a question that computers are good at answering.
Computer help
Just do it. CMU professor Mackey, who has proved 8-dimensional problems before, has joined Stanford’s Ph.D. in mathematics Brakensiek and assistant professor Heule who specializes in computer-aided proof.
Recalling the day when the project was established, Mackey said that Brakensiek was a real genius and looked at him like James in the NBA Finals. Brakensiek himself is really good. He was the gold medal winner of the 2013/14 International Informatics Olympiad.
△ Brakensiek, the first author of the paper
Get back to business. In order to facilitate the computer to solve, they changed their thinking:
First set the cards to have 7 points and 6 possible colors, and color these cards according to the previous “Condition 4” to see if you can find 128 different coloring methods. If it can’t be found, then Keller’s conjecture holds.
Using computer-assisted proving math problems, you also need to turn it into a series of logical operations, that is, handle the AND-NOR relationship between 01.
If it is required to solve 7 dimensions, there are 39000 different Boolean variables (0 or 1) in total, and there are 239000 possibilities. This is a very very large number with 11741 digits .