What does Stacking Spheres have to do with Writing Proofs?
Ever since 1611, Johannes Kepler had suggested that the most efficient way to stack unit spheres is to arrange them in a pyramid formation. Thomas Hale managed to come up with a 300 page proof in 1998, but reviewers were only 99% certain that the proof is correct even after spending 4 years on it.
As such, in 2003, Hales began to create a computational tool that could formally verify the proofs by relying on small, easily validated series of logical statements, to bootstrap their way to long tedious proofs. Finally, in August 2014, Hales announced that he was able to computationally verify that the pyramid offered the densest packing.
"This technology cuts the mathematical referees out of the verification process," says Hales. "Their opinion about the correctness of the proof no longer matters." This would also allow us to verify the dense mathematical proofs written up in specialized fields, which few other mathematicians would be able to follow.
Imagine if one day a computer could come along and grade your solutions on Brilliant, and tell you if it's right or wrong! The community will no longer need to point out errors or flaws, and will just appreciate the proofs and echo "Well Done!"
Note by
Calvin Lin
6 years, 10 months ago
Easy Math Editor
This discussion board is a place to discuss our Daily Challenges and the math and science related to those challenges. Explanations are more than just a solution — they should explain the steps and thinking strategies that you used to obtain the solution. Comments should further the discussion of math and science.
When posting on Brilliant:
*italics*or_italics_**bold**or__bold__paragraph 1
paragraph 2
[example link](https://brilliant.org)> This is a quote# I indented these lines # 4 spaces, and now they show # up as a code block. print "hello world"\(...\)or\[...\]to ensure proper formatting.2 \times 32^{34}a_{i-1}\frac{2}{3}\sqrt{2}\sum_{i=1}^3\sin \theta\boxed{123}Comments
But I think we should not let machines take over us.
Thank you for this article. I agree with Anuj Shikarkhane. We should not let machines take over us. I would like to see you here, rather than a machine. There is much more in relation between human and human rather than human and machine. Machine can do our tedious work our dangerous work or time consuming work, they could help, not eliminate humans.
The whole story is really fantastic!
Oh that would be wonderful. Then we wouldn't spend so much time on problems like this
The hardest integral ever!!
thinking that this has an exact answer, but doesn't (the "correct answer" here is but only an excellent approximation). Wouldn't it be great if we just asked Siri (or something like her), "is this answer really correct?"
But, seriously, though, mathematics continues to evolve, and new technologies bring in, as always, blessings and curses. We are already accustomed to using math software to carry out the most complex arithmetical computations, why not the same for "long tedious proofs"? "But how can we trust computers to give us the truth?" Well, didn't Godel already comment on that, on the entire foundation of mathematics?
Ach! And just today I find out that one of my own posted problems had a flawed "correct answer". Oh well.
But, personally, I welcome "mechanized proofs" for another reason. A lot of pure mathematics involves definitions and reasoning that seems to defy implementation by computer. Much of it sounds too much like philosophical discourse, and I often wonder how "real" some of it is. How does it affects or impacts the rest of mathematics, or even physics? So, I've eventually adopted the view that if a branch of pure mathematics can be implemented on a computer, i.e., can be made understandable by a computer, then it passes a kind of a test of "real-ness" to me. It than has utility, a practical value. I would thus divide mathematics into two parts, one that is implementable by computer, and one that remains part of philosophical discourse. An immediate candidate I would propose for this test would be certain topics in real analysis, which seems to me indistinguishable from philosophical speculation that have no practical consequences for anything else, mathematics or physics. One of the things Alan Turing is famous for is the "Turing Test", in which it proposes that if a machine can fool people into thinking that it can think, it does think after all. I'd like to propose something similar, which is that if a computer can do and prove certain mathematical theorems with repeatable results, then that part of mathematics is proven to be more than philosophical speculation. In other words, if you can explain it to a computer, then it is at least not gibberish.