Six months later, the results were positive – their proof was correct, albeit with a few slight imprecisions. A group of mathematicians, with the vast majority of work done by Johan Commelin, were able to follow their written out proof and “teach” it to a computer, hence verifying their proof [4]. So it is actual ly possible that a computer could actively participate in research-level mathematics – with a slight catch. Here Lean is a proof assistant, not a proof generator; the computer’s checking of the proof relies on the human effort of formalizing the proof, since it cannot read and digest human prose by itself. It also certainly cannot come up with a proof of this very technical statement all on its own; while Lean can make simplifications that might not come as completely obvious to humans, it still follows the skeleton of the argument given by Scholze and Clausen and merely checks whether it is logically correct. There is also another dimension to this problem; research in mathematics is largely about proving statements, but par t of it i s al so about choosing and proving the “r ight” statements. Of ten when mathematicians cannot prove a certain statement, they go about proving a simpler version that is sti l l “interesting”. These words, however, are much more difficult to define than absolute concepts like true and false; for example, while we might not yet have enough machinery to prove the Twin Prime Conjecture (i.e. “there are infinitely many pairs of primes that have a difference of two”), we are able to prove a weaker version of this statement, that there are infinitely many pairs of primes with a difference less than or equal to 246 [5], and notably this weaker version is still of interest to us. To look for ways to simplify a given conjecture into the right statement is straightforward to a human being, but not necessar i ly easy to a computer. There are ongoing efforts to study the difference between “easy” and “hard” problems by using machine learning, such as a recent effort began by Timothy Gowers [6]; once this barrier is cleared, we might have more progress in getting computers to prove “not-too-hard” statements that are “useful” to mathematicians. We are, also, still a long way away from solving problems that need some sort of “cheat” or “hint”, or involve constructing certain examples; these problems are often extremely difficult by brute force searching but are almost trivial once you know what method you need. Without a human feeding the hint to the prover, at present it is impossible for a computer to come up with the “hint” itself, and even for a mathematician, it takes years of training to be able to spot the best way to attack a problem. But recently, AIs have also been able to solve harder problems independently – it is now possible for cer tain engines (ROBOT [6], Lean [7]) to solve “routine” undergraduate- level math problems, as well as problems from the International Mathematical Olympiad, a worldwide competition for high schoolers often called the Olympics of Mathematics. So it is only natural to expect that computers will be able to solve harder and harder problems in the future – perhaps, at some point, even surpassing human capabilities. So what role will computers play in research-level mathematics in the future? The honest answer is that nobody knows; AI-optimists will claim that computers will eventually replace mathematicians, in the time frame of ten years to a century; those less optimistic will claim that mathematicians are irreplaceable. As an aspiring research mathematician, I surely hope that we will not be replaced in the near future (very unlikely). But it is also exciting to see progress both in improving the knowledge base which software can draw from, and in computers’ ability to solve problems hands-on. Perhaps one day they will replace mathematicians – who knows? But first there will surely be a time when computers will aid mathematicians greatly in their research, when they gain the ability to prove tedious statements that nobody wanted to do. 1 Fields Medal: Regarded as the “Nobel Prize in mathematics” (which does not exist), it is one of the most prestigious prizes in mathematics, which is awarded to two to four outstanding mathematicians under the age of 40 every four years. 23
RkJQdWJsaXNoZXIy NDk5Njg=