Google AI system proves over 1200 mathematical theorems
A new and remarkable development here is that several researchers at Google'used in Hales research center in Mountain View, California have now developed an AI theorem-proving program. Their program works with the HOL-Light theorem prover, which was used in Hales' proof of the Kepler conjecture, and can prove, essentially unaided by humans, many basic theorems of mathematics. What's more, they have provided their tool in an open-source release, so that other mathematicians and computer scientists can experiment with it.
The Google AI system was "trained" on a set of 10,200 theorems that the researchers had gleaned from several sources, including many sub-theorems of Hales' proof of the Kepler conjecture. Most of these theorems were in the area of linear algebra, real analysis and complex analysis, but the Google researchers emphasize that their approach is very broadly applicable.
In the initial release, their software was able to prove 5919, or 58% of the training set. When they applied their software to a set of 3217 new theorems that it had not yet seen, it succeeded in proving 1251, or 38.9%. Not bad for a brand-new piece of software.
Mathematicians are already envisioning how this software can be used in day-to-day research. Jeremy Avigad of Carnegie Mellon University sees it this way:
You get the maximum of precision and correctness all really spelled out, but you don't have to do the work of filling in the details. Maybe offloading some things that we used to do by hand frees us up for looking for new concepts and asking new questions.
For additional details see the authors' technical paper, or this New Scientist article by Leah Crane.
[link]
AlphaGo is a computer program that plays the board game Go.[1] It was developed by Alphabet Inc.'s Google DeepMind in London. AlphaGo had three far more powerful successors, called AlphaGo Master, AlphaGo Zero [2] and AlphaZero.
In October 2015, the original AlphaGo became the first computer Go program to beat a human professional Go player without handicaps on a full-sized 19×19 board.[3][4] In March 2016, it beat Lee Sedol in a five-game match, the first time a computer Go program has beaten a 9-dan professional without handicaps.[5] Although it lost to Lee Sedol in the fourth game, Lee resigned in the final game, giving a final score of 4 games to 1 in favour of AlphaGo. In recognition of the victory, AlphaGo was awarded an honorary 9-dan by the Korea Baduk Association.[6] The lead up and the challenge match with Lee Sedol were documented in a documentary film also titled AlphaGo,[7] directed by Greg Kohs. It was chosen by Science as one of the Breakthrough of the Year runners-up on 22 December 2016.[8]
At the 2017 Future of Go Summit, its successor AlphaGo Master beat Ke Jie, the world No.1 ranked player at the time, in a three-game match (the even more powerful AlphaGo Zero already existed but was not yet announced). After this, AlphaGo was awarded professional 9-dan by the Chinese Weiqi Association.[9]
AlphaGo and its successors use a Monte Carlo tree search algorithm to find its moves based on knowledge previously "learned" by machine learning, specifically by an artificial neural network (a deep learning method) by extensive training, both from human and computer play.[10] A neural network is trained to predict AlphaGo's own move selections and also the winner's games. This neural net improves the strength of tree search, resulting in higher quality of move selection and stronger self-play in the next iteration.
After the match between AlphaGo and Ke Jie, DeepMind retired AlphaGo, while continuing AI research in other areas.[11] Starting from a 'blank page', with only a short training period, AlphaGo Zero achieved a 100-0 victory against the champion-defeating AlphaGo, while its successor, the self-taught AlphaZero, is currently perceived as the world's top player in Go as well as possibly in chess.
[link]