SoylentNews is people
SoylentNews
QuantaMagazine.org has a very long and interesting article on computers redefining the roots of Math.
On a recent train trip from Lyon to Paris, Vladimir Voevodsky sat next to Steve Awodey and tried to convince him to change the way he does mathematics.
Voevodsky, 48, is a permanent faculty member at the Institute for Advanced Study (IAS) in Princeton, N.J. He was born in Moscow but speaks nearly flawless English, and he has the confident bearing of someone who has no need to prove himself to anyone. In 2002 he won the Fields Medal, which is often considered the most prestigious award in mathematics.
[...] The idea of doing mathematics in a program like Coq has a long history. The appeal is simple: Rather than relying on fallible human beings to check proofs, you can turn the job over to computers, which can tell whether a proof is correct with complete certainty. Despite this advantage, computer proof assistants haven't been widely adopted in mainstream mathematics. This is partly because translating everyday math into terms a computer can understand is cumbersome and, in the eyes of many mathematicians, not worth the effort.
For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people.
"The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes," Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error.
This is something Voevodsky has learned through personal experience. In 1999 he discovered an error in a paper he had written seven years earlier. Voevodsky eventually found a way to salvage the result, but in an article last summer in the IAS newsletter, he wrote that the experience scared him. He began to worry that unless he formalized his work on the computer, he wouldn't have complete confidence that it was correct.
But taking that step required him to rethink the very basics of mathematics. The accepted foundation of mathematics is set theory. Like any foundational system, set theory provides a collection of basic concepts and rules, which can be used to construct the rest of mathematics. Set theory has sufficed as a foundation for more than a century, but it can't readily be translated into a form that computers can use to check proofs. So with his decision to start formalizing mathematics on the computer, Voevodsky set in motion a process of discovery that ultimately led to something far more ambitious: a recasting of the underpinnings of mathematics.
Geometry and classic algebra are not really isomorphic. Boolean logic and number theory were proved incompatible by Bertrand Russell
(Score: 1) by Tara Li on Wednesday October 04 2017, @04:16PM (5 children)
If this system can take a proof and verify it - could it then be used to genetically create new proofs and verify them as a measure of "fitness", and would this likely lead to useful new mathematical understandings, or just random factoids thrown out? And could this be applied to the mathematics used in the Standard Model of physics, to let us get a handle on WTF is going on with it?
(Score: 0) by Anonymous Coward on Wednesday October 04 2017, @05:00PM (2 children)
That was actually the original impetus for developing automated theorem proving. It just turned out that proving theorems is actually fairly difficult, so generating theorems isn't really possible Maybe it will be in the future with better theorem proving technology / more computing power.
(Score: 3, Interesting) by HiThere on Wednesday October 04 2017, @05:04PM (1 child)
Actually, what's really difficult is generating interesting proofs. Proofs are easy to generate if you don't care what is being proven.
Because of this you probably aren't going to get a automated theorem prover before you get a full scale AI.
Javascript is what you use to allow unknown third parties to run software you have no idea about on your computer.
(Score: 3, Funny) by captain normal on Wednesday October 04 2017, @08:14PM
But if you get full scale Artificial Intelligence, wouldn't you wind up with artificial theorem and artificial proofs?
Everyone is entitled to his own opinion, but not to his own facts"- --Daniel Patrick Moynihan--
(Score: 0) by Anonymous Coward on Thursday October 05 2017, @09:39AM
If you're asking about how to generate proofs then maybe this is useful. Here's what I understand about the "set of support" strategy for automated theorem proving:
To start off you have two things. A goal statement that want to prove/disprove, and a "set of support" which starts out as _the set of all of the math statements that you assume are true to begin with_. These would include things like the axioms of the math system that you are using, plus other statements representing theorems that you'd want to use without having to re-prove from the ground up, and would also include statements which set up the problem you're trying to solve.
As an example: Say my problem was that I had a triangle where I knew that two of the angles were 60 degrees and 90 degrees, and my goal was to automatically prove/disprove that the third angle was 30 degrees. The set of statements that I began with would need to include which math system I was working with, because there are some systems where the angles in a triangle add up to 180 degrees, and others where they don't (e.g. https://en.wikipedia.org/wiki/Spherical_geometry). [wikipedia.org] If I didn't include this kind of basic stuff, then an automated theorem prover would never be able to prove/disprove the goal statement, because it wasn't given enough information to figure out if the angles in a triangle add up 180 degrees or not. On top of that I would probably want to include other statements ( some theorems about triangles maybe ) if I wanted to do problems with triangles and not have to prove those things from the ground up. The last thing I'd have to provide would be statements about the actual problem I have ("There is a triangle and one angle is 60 degrees and another is 90 degrees.").
So that describes how you start out. From there, you follow [some procedure] to derive a new statement from the existing set of support. This new statement must be true, since you derived it from the things you began with, and we're assuming that all those things are true. So you include the new statement into the set of support, and now you can use it going forward. You keep doing this in a loop until you either prove/disprove the goal statement or give up.
So, the kind of set-up that's described here really doesn't say how to do any problem-solving. The "[some procedure]" part is where all the problem solving would go (how do you actually choose what stuff to generate so that you get to the answer?) and people don't have a way to do that efficiently. There are competitions to build the best tools for this stuff ( http://www.cs.miami.edu/~tptp/CASC/ [miami.edu] http://smtcomp.sourceforge.net/2017/ [sourceforge.net] http://www.satcompetition.org/ [satcompetition.org] )
Also there are "SMT solvers" and "SAT solvers" which solve smaller classes of problems, and they work differently and actually are used. e.g. https://github.com/Z3Prover/z3 [github.com] could be good to look at.
(Score: 2) by TheRaven on Thursday October 05 2017, @10:42AM
sudo mod me up