Mathematicians Welcome Computer-Assisted Proof in 'Grand Unification' Theory (nature.com) 36
Proof-assistant software handles an abstract concept at the cutting edge of research, revealing a bigger role for software in mathematics. From a report: Mathematicians have long used computers to do numerical calculations or manipulate complex formulas. In some cases, they have proved major results by making computers do massive amounts of repetitive work -- the most famous being a proof in the 1970s that any map can be coloured with just four different colours, and without filling any two adjacent countries with the same colour. But systems known as proof assistants go deeper. The user enters statements into the system to teach it the definition of a mathematical concept -- an object -- based on simpler objects that the machine already knows about.
A statement can also just refer to known objects, and the proof assistant will answer whether the fact is 'obviously' true or false based on its current knowledge. If the answer is not obvious, the user has to enter more details. Proof assistants thus force the user to lay out the logic of their arguments in a rigorous way, and they fill in simpler steps that human mathematicians had consciously or unconsciously skipped. Once researchers have done the hard work of translating a set of mathematical concepts into a proof assistant, the program generates a library of computer code that can be built on by other researchers and used to define higher-level mathematical objects. In this way, proof assistants can help to verify mathematical proofs that would otherwise be time-consuming and difficult, perhaps even practically impossible, for a human to check. Proof assistants have long had their fans, but this is the first time that they had a major role at the cutting edge of a field, says Kevin Buzzard, a mathematician at Imperial College London who was part of a collaboration that checked Scholze and Clausen's result. "The big remaining question was: can they handle complex mathematics?" says Buzzard. "We showed that they can."
A statement can also just refer to known objects, and the proof assistant will answer whether the fact is 'obviously' true or false based on its current knowledge. If the answer is not obvious, the user has to enter more details. Proof assistants thus force the user to lay out the logic of their arguments in a rigorous way, and they fill in simpler steps that human mathematicians had consciously or unconsciously skipped. Once researchers have done the hard work of translating a set of mathematical concepts into a proof assistant, the program generates a library of computer code that can be built on by other researchers and used to define higher-level mathematical objects. In this way, proof assistants can help to verify mathematical proofs that would otherwise be time-consuming and difficult, perhaps even practically impossible, for a human to check. Proof assistants have long had their fans, but this is the first time that they had a major role at the cutting edge of a field, says Kevin Buzzard, a mathematician at Imperial College London who was part of a collaboration that checked Scholze and Clausen's result. "The big remaining question was: can they handle complex mathematics?" says Buzzard. "We showed that they can."
The Last Question IRL (Score:3)
Source [wikipedia.org]
Re: (Score:2)
Re: (Score:3)
Re: (Score:2)
Re: (Score:3)
Depends on what you mean by ages. I took a course on machine proofs in 1998. The four-colour theorem was proved by machine in 1976. That last bit is in TFS.
They're a pain in the ass for sure, and it's much more fun proving things the old fashioned way, but the power of them is pretty undeniable.
A very valid objection is that machine proofs are often so complicated that they practically amount to a simple true or false output. Landmark human proofs tend to contribute new methods and understanding that are ap
Re: (Score:3)
Its not so simple to get to the point of practical iteration. Chess isnt anywhere close to being solved, for example, even though a solving algorithm is trivial to construct.
Re: (Score:3)
I'm not sure exactly what you're trying to say. If you mean simple iteration, machine proof systems don't do that. The four colour theorem wasn't proved by generating all possible maps and finding ways to colour them with four colours, for example.
Machine proof systems take definitions, principles of logic, and generate logical deductions. This is how human proofs work too. The difference is really only in how humans and machines choose what direction in which to proceed.
Re: (Score:2)
.If you mean simple iteration, machine proof systems don't do that.
The computer generated 4-color theorem proof most certainly iterates over a subset of all possible graphs, and the subset was large enough that the proof was therefore still enormous, in spite of only needing to iterate over a subset of all the graphs. This is for a lucky problem where the search space was reduced to a small enough N, and it still wasnt all that small. For fuck sakes you dishonest or always wrong fuck, time for you to shut the
Re: (Score:2)
Think about your claim: the search space for *all possible graphs* was reduced to a small enough N to check each one.
You clearly have access to the Internet. Why don't you use it to do some research? And why does this topic anger you so much?
Re: (Score:3)
Re: (Score:2)
Re: (Score:2)
That's why my first sentence was "depends...."
From the perspective of the history of mathematics, automated proof systems popped into existence yesterday. From the perspective of electronic computing, as soon as we had some spare time away from reading Nazi mail we started thinking about how to use our new toys to do this kind of logical symbol manipulation. Some dudes even named it "artificial intelligence."
Re: (Score:2)
we started thinking about how to use our new toys to do this kind of logical symbol manipulation. Some dudes even named it "artificial intelligence." Flag as Inappropriate
Oh, I'm fully aware of the Dartmouth workshop and how the Logic Theorist presentation went completely under the radar of most participants of the workshop. It's a famous cautionary tale, I believe.
Re: (Score:3)
Actually, theoretical computer scientists have been using this for ages in proofs. Mathematicians are a little slow to adopt new things.
Re: (Score:2)
Re: (Score:2)
True. And while there are CS types doing theoretical CS research, calling them "mathematicians" is not so far off the mark.
Re: (Score:2)
Very unclear abstract (Score:4, Informative)
The abstract just discusses proof assistants, which while interesting is not new. The result they are used to show, that geometry, functional analysis and p-adic numbers can be unified (hence the title) is not in the abstract at all, but is interesting as well.
Re: (Score:2)
not "more fundamental than observed reality"
This is absolutely wrong. I've said before that mathematics is that part of science that doesn't require a universe. In a universe with different values for the fundamental physical constants, mathematics would be exactly the same.
2+2=4 not because of the properties of space and time, matter and energy, but rather the other way around.
The same is true for unique factorization of the integers, the fundamental theorem of algebra, the completeness of a compact metric space, Hilbert's Nullstellensatz, and any o
Re: (Score:2)
That's cute, but no one takes seriously the hypothesis that you don't know what the thorem "2+2=4" is.
Re: (Score:2)
This isn't really true either. Mathematics (the system, not the subject) is a self-consistent system based on a small (maybe minimal) set of axioms. We choose the axioms that give us a useful system, but you could choose others.
If you look historically, we sort of fluffed around with mathematics, inventing bits that were useful (i.e. consistent with observation of reality), then we decided to actually formalize the thing and agree on the axioms that make it all work. And we're still working on that part.
So
Re: When mathematicians talk about "proof"... (Score:1)
Mathematics is unlike reality by design. It's all based on infinities when reality is very much discrete.
Re: (Score:2)
The foundation of modern math is set theory so....
Bad joke alert (Score:3)
Grothendieck begs to differ.
Re: (Score:2)
Because really, everything in mathematics *also* just relies on it being a theory with a very high likeliness of making the correct predictions, that can be overthrown by a conflicting observation.
This statement isn't true in the usual sense of the word "observation". Mathematics (and yes Godel's theorem is part of mathematics) derives things from axioms. There are no predictions, no observations, no probabilities, etc.
The statement is true in a kind of way. Mathematical proofs are not proofs until a large enough body of mathematicians have read the proof and concurred that it is correct -- that there is no logical flaw in the structure and reasoning of the proof. This fact has a profound conseque
Re:When mathematicians talk about "proof"... (Score:4, Informative)
Professor Hilbert? (Score:2)
Re: (Score:2)
I have a "Kurt Godel" on line 1.
Fun fact - While he’s on hold, we both know and don’t know some true statements have no proof.
Re: (Score:2)
Were you going to finish that comment?
I have discovered a truly marvelous proof of this. (Score:4, Funny)
What the primary result was that was proven (Score:5, Informative)
Since the summary doesn't really explain things much, it might help to note part of what they proved. (Disclaimer: I am am mathematician but I don't understand the details of their work but only an approximation. Also, one of the two authors, Dustin Clausen, is a friend of mine I've known since we were roomates in the same summer math program in high school many years ago, so I may have some biases here.) Roughly speaking, Peter Scholze and Dustin Clausen noticed that there were close analogies between a whole bunch of different fields, p-adic analysis, analytic geometry, and some other stuff. But the idea that the results were analogous didn't quite work under a standard framework. They realized that one could make these make sense all together if one had a different approach to how topology worked, the major details of which are here https://www.math.uni-bonn.de/people/scholze/Condensed.pdf [uni-bonn.de].
However, their new framework for topology relies on a set of ideas about the regular old real numbers which worked as a sort of base case for everything. But the proof that Scholze and Clausen came up for this base case is fantastically complicated, so complicated that they weren't really sure that all the moving parts hung together. What happened then is that a group of people using computer assisted proof systems turned that proof into a computer-checkable proof, and in the process they also made a bunch of parts substantially easier for a human to follow and see what was going on.
An introduction to a proof assistant (Lean) (Score:1)
For those possessing limited knowledge of proof assistants, I recommend this article in Quanta Magazine as an approachable introduction. https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001