The 21-digit solution to the decades-old problem suggests many more solutions exist.
What do you do after solving the answer to life, the universe, and everything? If you're mathematicians Drew Sutherland and Andy Booker, you go for the harder problem.
In 2019, Booker, at the University of Bristol, and Sutherland, principal research scientist at MIT, were the first to find the answer to 42. The number has pop culture significance as the fictional answer to "the ultimate question of life, the universe, and everything," as Douglas Adams famously penned in his novel "The Hitchhiker's Guide to the Galaxy." The question that begets 42[*], at least in the novel, is frustratingly, hilariously unknown.
In mathematics, entirely by coincidence, there exists a polynomial equation for which the answer, 42, had similarly eluded mathematicians for decades. The equation x3+y3+z3=k is known as the sum of cubes problem. While seemingly straightforward, the equation becomes exponentially difficult to solve when framed as a "Diophantine equation" — a problem that stipulates that, for any value of k, the values for x, y, and z must each be integers.
When the sum of cubes equation is framed in this way, for certain values of k, the integer solutions for x, y, and z can grow to enormous numbers. The number space that mathematicians must search across for these numbers is larger still, requiring intricate and massive computations.
Over the years, mathematicians had managed through various means to solve the equation, either finding a solution or determining that a solution must not exist, for every value of k between 1 and 100 — except for 42.
In September 2019, Booker and Sutherland, harnessing the combined power of half a million home computers around the world, for the first time found a solution to 42. The widely reported breakthrough spurred the team to tackle an even harder, and in some ways more universal problem: finding the next solution for 3.
Booker and Sutherland have now published the solutions for 42 and 3, along with several other numbers greater than 100, recently in the Proceedings of the National Academy of Sciences.
[*] 42: Wikipedia Entry.
Journal Reference:
Andrew R. Booker, Andrew V. Sutherland. On a question of Mordell [open], Proceedings of the National Academy of Sciences (DOI: 10.1073/pnas.2022377118)
Previously:
Sum-of-Three-Cubes Problem Solved for "Stubborn" Number 33.
(Score: 4, Interesting) by Anonymous Coward on Tuesday March 23 2021, @10:33PM (16 children)
They were "old school" mathematicians, and when the 4-color map theorem was proved with a computer they scoffed at it. In their mind, the idea was that if you brute-forced a problem with a computer, you hadn't really solved it. I guess I can kind of see the point--mathematics is usually about striving for the most elegant solution possible. If you just brute-force it with computation, you might be missing some really interesting math. However, a big problem with that PoV is that an elegant solution may not exist.
(Score: 1, Interesting) by Ethanol-fueled on Tuesday March 23 2021, @10:52PM
I heard differently, that proving something with a computer is a totally different approach to solving it on paper. I'd hesitate to call it "brute force" simply because it uses iteration or recursion.
(Score: 0) by Anonymous Coward on Tuesday March 23 2021, @11:17PM (11 children)
It's just one of a few fairly common weird ideas (another one is that pure math > applied math, the weirder and more spaced out your little subset is apparently the greater you are -- so there is a hierarchy among the mathematicians even tho not everyone cares). But it is not uncommon or rare that computer assisted solutions are, sometimes, not considered to be real or proper solutions since they tend to lack mathematical elegance, which is vague as heck -- it's sort of you know it when you see it but it should be simple. That your supercomputer spat out an answer is not considered to be elegant or simple. Some of it might also have to do with that they are not always sure if it is A solution or THE solution. In their minds only stringent logic and a proper set of equations is considered to be a real solution.
Perhaps then it's really all just about presentation, if you can get the computer to write it as a proper mathematical proof then perhaps the idea will take less of an effort to sink in and be accepted.
(Score: 1, Insightful) by Anonymous Coward on Tuesday March 23 2021, @11:44PM (4 children)
Related: https://xkcd.com/435/ [xkcd.com]
(Score: 0) by Anonymous Coward on Wednesday March 24 2021, @01:33AM (3 children)
What I find amusing about that comic is that he forgot Logisticians, who are the next step past Mathematicians.
(Score: 0) by Anonymous Coward on Wednesday March 24 2021, @07:22AM (1 child)
i always thought of logic as applied philosophy
(Score: 0) by Anonymous Coward on Thursday March 25 2021, @10:27AM
... and isn't philosophy just applied sociology?
(Score: 2) by maxwell demon on Wednesday March 24 2021, @08:05AM
Isn't logistics a very practical problem?
The Tao of math: The numbers you can count are not the real numbers.
(Score: 2, Interesting) by khallow on Wednesday March 24 2021, @12:19AM (5 children)
This. How do we know the computer program actually found a solution? As I recall, the first proof of the four color theorem was checked years later (partly by hand, but still mostly by computer) and they found some errors (which allowed them to simplify the proof a little). It didn't break the proof, but it could have.
(Score: 1, Interesting) by Anonymous Coward on Wednesday March 24 2021, @01:55AM
The modern way is to use tools like Coq or ACL2, which are mathematically proven mathematical proof provers. This has the advantage that if they don't work then manual proofs don't either. The original four colour proof was suspect because it didn't achieve this level of recursive navel gazing.
(Score: 2) by bzipitidoo on Wednesday March 24 2021, @12:42PM (1 child)
Verification is often trivial compared to discovery. That's the essence of the debate about whether P=NP. If P≠NP, as most people strongly suspect, then there are all kinds of problems in which checking whether an answer is correct is easy, while finding a correct answer is hard.
A proof of the four color theorem that is an exhaustive check of all the possibilities is a perfectly valid proof whether a computer or a human did the checking. That's really what proofs are: checked all the possibilities. Found a way to cover all the cases. It's nice when there's an elegant way to break a problem down into a handful of cases, but this is not always possible. Like with this sum of cubes problem, we know that any sum s in which s%9 is 4 or 5, does not have a solution. So, no solution for 13 or 14, or 22, 23, 31, 32, etc. Why? Because any cube c%9 is always -1 (or 8), 0, or 1. There's no combination of -1,0,1 for which 3 of them can add up to 4 or -4, can only get to 3 or -3. So that's a nice, elegant elimination of 2/9ths of all the numbers, leaving the other 7/9ths an open question whether there are always 3 cubes that can sum up to them.
You could reason that, yes, a cube and the adjacent numbers always have such solutions, as they are trivial to construct c^3 = c^3 + 0^3 + 0^3 = c^3 +1^3 - 1^3. Doesn't settle a significant fraction of the possibilities, but if that's all there is, that's what you use. Potentially, thousands of such cases could combine to be a proof, and such efforts really are best done with computer assistance.
Brute force has its place. Don't discount it. Number Theory in particular is brim full of questions that are easy to ask and very hard to prove. Are there infinitely many twin primes? From the universe of Diophantine questions, Is there a perfect box? Brute force with computers can be employed to explore a larger space than we could ever hope to do by hand, and while if there are no perfect boxes it can't prove that, it could prove that there are perfect boxes by finding one.
(Score: 0) by Anonymous Coward on Wednesday March 24 2021, @05:35PM
> Verification is often trivial compared to discovery.
That's why professors grade the answers, they don't supply the answers. Their job is to tell you your work isn't good enough (unless it is then they get credit).
(Score: 3, Interesting) by hendrikboom on Wednesday March 24 2021, @02:04PM (1 child)
I was present at a presentation of the first computer proof of the four-colour theorem at the University of Waterloo. One of the professors attending that session said he had doubts about the result. The theoretical part was sound, but the computer computation was suspect. He said he just didn't believe that the proof could be that straightforward.
This caused immediate scrutiny of the program. He found a bug.
That bug, of course was fixed. It took months to rerun the program, and it eventually came up with a much more complicated proof.
This time that professor said he did now trust the result.
This created a general awareness that when programs are used to prove things that are not easily checked independently (like the expression of an integer as the sum of three cubes), it is essential to prove the program correct.
(Score: 0) by Anonymous Coward on Wednesday March 24 2021, @05:36PM
Proof by Professor, as it's known. I don't believe that + I don't understand that = the complete intellectual toolkit.
(Score: 2) by Mojibake Tengu on Tuesday March 23 2021, @11:59PM (2 children)
Anything a mathematician proves on paper I can prove on a computer by a Prolog program. Often lazily by letting the program to find a proof herself.
This has nothing to do with brute force numerical calculations. All I need is a proper formulation of a problem, in a relevant logical paradigm.
In Category Theory and Linear Logic, any abstract program is a proof of something and this was already proved long ago. This applies to all computer programs too.
I despise numerical calculations, actually. And all those current fake-AI tensor devilish monsters creeping on GPUs everywhere. Your professor was rightly afraid of those numerical devils coming to his lawn, but he did not see only truly logical AIPs could reach the final supremacy over humans.
The edge of 太玄 cannot be defined, for it is beyond every aspect of design
(Score: 0) by Anonymous Coward on Wednesday March 24 2021, @05:53AM
Have fun:
(Score: 3, Touché) by hendrikboom on Wednesday March 24 2021, @02:07PM
Actually, it turns out not to be that easy in practice.
It's not even that easy in theory -- Prolog has only a limited proof-theoretic strength.
-- hendrik