|A kind of counter-example to your claim is the following:
http://www.math.rutgers.edu/~zeilberg/GT.html
It is an automated reasoning system for Euclidean geometry. Starting from literally nothing, it derived all of the geometric propositions in Euclid’s Elements in a matter of seconds. Then it proceeded to produce a number of geometric theorems of human interest that were never noticed by any previous Euclidean geometers, classical or modern.
This is simply to point out that there are some fields of math that are classically very hard but computers find trivial. Another example is the verification of random algebraic identities by brute force.
On the other hand, large fields of mathematics have not yet come to be dominated by computers. For those I think this paper is a good introduction to some state-of-the-art, machine-learning based techniques: http://arxiv.org/abs/1108.3446
One can see from the paper that there is plenty of room for machine learning techniques to be ported from fields like speech and vision.
Progress in machine learning in vision and speech has recently been driven by the existence of huge training data-sets. It is only within the last few years that truly large databases of human-made proofs in things like set theory or group theory have been formalized. I think that future progress will come as these databases continue to grow.
A kind of counter-example to your claim is the following: http://www.math.rutgers.edu/~zeilberg/GT.html It is an automated reasoning system for Euclidean geometry. Starting from literally nothing, it derived all of the geometric propositions in Euclid’s Elements in a matter of seconds. Then it proceeded to produce a number of geometric theorems of human interest that were never noticed by any previous Euclidean geometers, classical or modern.
This is interesting.
It’s hard for me to assess it from the outside. In particular, I don’t have a good sense for the number of sequences of logical derivations one has to consider in order to arrive at the theorems that were proved if one were to proceed by brute force. I find it more interesting that it honed in on classical theorems on its own than that it was able to prove them (one can use coordinate geometry to reduce proofs to solving polynomial equations).
I think that it’s significant that Euclidean geometry fell out of fashion a long time ago: the fraction of modern mathematicians who think about Euclidean geometry is negligible, and this may reflect an accurate assessment of the field as mathematically shallow. I didn’t appreciate geometry until I learned about discrete groups of isometries acting on homogeneous Riemannian manifolds.
For those I think this paper is a good introduction to some state-of-the-art, machine-learning based techniques: http://arxiv.org/abs/1108.3446 One can see from the paper that there is plenty of room for machine learning techniques to be ported from fields like speech and vision.
Thanks for the reference
Progress in machine learning in vision and speech has recently been driven by the existence of huge training data-sets. It is only within the last few years that truly large databases of human-made proofs in things like set theory or group theory have been formalized. I think that future progress will come as these databases continue to grow.
Starting from literally nothing, it derived all of the geometric propositions in Euclid’s Elements in a matter of seconds. Then it proceeded to produce a number of geometric theorems of human interest that were never noticed by any previous Euclidean geometers, classical or modern.
Where do you get these detailed claims about the program? I don’t see anything like them in the book or here or here
Starting from literally nothing, it derived all of the geometric propositions in Euclid’s Elements in a matter of seconds.
Where do you get these detailed claims about the program?
Just to point out the obvious, your first link certainly does say that
Once you know the ansatz, you can have the machine, discover from scratch all the statements of any bounded complexity, and prove them at the same time, either rigorously (time permitting) or semi-rigorously (if a polynomial of degree 10^100 vanishes at 10^6 random values it is most likely identically zero, just like Rabin’s pseudo-primes). This is what Shalosh B. Ekhad, XIV, did in its 2050 PLANE GEOMETRY TEXTBOOK. What is so nice about it is that it is written in a precise, and hence completely formally correct programming language, Maple, but the names of the definitions are English based. Also each statement doubles as the proof, ready to be executed by Maple. So we have a text that is even more formally correct than any logocentric human proof (recall that Bill Thurston said that a computer program is much more formally correct than a human proof), yet just as much fun to read, and in which once you read the statement, you already have the proof (modulo running it on Maple, but I already did, so you can trust me and not run it again).
Oh, yeah, I missed that Zeilberger used the phrase “from scratch,” so that explains why JH says “from literally nothing” (though I disagree), but why did you quote the rest of the passage? Do you think it suggests any other of JH’s claims?
I quoted the rest so that it was clear that the key phrase ‘from scratch all the statements’ was referring to a computational, implemented, software package for Euclidean / plane geometry in particular.
|A kind of counter-example to your claim is the following: http://www.math.rutgers.edu/~zeilberg/GT.html It is an automated reasoning system for Euclidean geometry. Starting from literally nothing, it derived all of the geometric propositions in Euclid’s Elements in a matter of seconds. Then it proceeded to produce a number of geometric theorems of human interest that were never noticed by any previous Euclidean geometers, classical or modern.
This is simply to point out that there are some fields of math that are classically very hard but computers find trivial. Another example is the verification of random algebraic identities by brute force.
On the other hand, large fields of mathematics have not yet come to be dominated by computers. For those I think this paper is a good introduction to some state-of-the-art, machine-learning based techniques: http://arxiv.org/abs/1108.3446 One can see from the paper that there is plenty of room for machine learning techniques to be ported from fields like speech and vision.
Progress in machine learning in vision and speech has recently been driven by the existence of huge training data-sets. It is only within the last few years that truly large databases of human-made proofs in things like set theory or group theory have been formalized. I think that future progress will come as these databases continue to grow.
This is interesting.
It’s hard for me to assess it from the outside. In particular, I don’t have a good sense for the number of sequences of logical derivations one has to consider in order to arrive at the theorems that were proved if one were to proceed by brute force. I find it more interesting that it honed in on classical theorems on its own than that it was able to prove them (one can use coordinate geometry to reduce proofs to solving polynomial equations).
I think that it’s significant that Euclidean geometry fell out of fashion a long time ago: the fraction of modern mathematicians who think about Euclidean geometry is negligible, and this may reflect an accurate assessment of the field as mathematically shallow. I didn’t appreciate geometry until I learned about discrete groups of isometries acting on homogeneous Riemannian manifolds.
Thanks for the reference
How much future progress? :-)
Where do you get these detailed claims about the program? I don’t see anything like them in the book or here or here
Just to point out the obvious, your first link certainly does say that
Oh, yeah, I missed that Zeilberger used the phrase “from scratch,” so that explains why JH says “from literally nothing” (though I disagree), but why did you quote the rest of the passage? Do you think it suggests any other of JH’s claims?
I quoted the rest so that it was clear that the key phrase ‘from scratch all the statements’ was referring to a computational, implemented, software package for Euclidean / plane geometry in particular.