Could a computer do math? Well, you may think, of course it can – you only need to type “1 + 1” into the Google search bar for it to show the number two. Computers, in fact, were built to do math; the name comes from the root “compute”, and was formerly used to refer to actual people who do calculations by hand before we had computers. Indeed, by using Microsoft Excel or programming languages such as Python or C++, a computer can do plenty of difficult calculations far faster than a human being could. But mathematicians are far more interested in another type of math – proof writing. Consider the fol lowing problem: Star t with any number. If it is even, divide the number by two. If it is odd, multiply it by three, then add one. Does this sequence always get to 1 eventually? This innocentlooking problem is known as the Collatz conjecture, and remains unsolved to this day. A computer could check whether this is true for an arbitrarily large number (given enough time and computing power), but to prove that it goes to 1 for any number takes far more effort and new techniques; we do not know how to do it yet. Consider another problem that we can solve. Given the quadrilateral in Figure 1, how do you find the highlighted angle? Well, we apply the theorem “exterior angle of cyclic quadrilateral” to prove that the two are the same. Could a computer do the same thing? If we teach it the theorem, then yes. Can computers, then, prove things that we do not yet know? Well, maybe. We need to teach a computer how to do mathematics. The first task is to formalize the mathematics we know now. One recent contender for this is Lean, a software developed by Microsoft engineer Leonardo de Moura in 2013 [1]. Big swathes of basic universitylevel mathematics have been formalized (rewritten in a way a computer understands) since its foundation, and there are multiple ongoing efforts to build up a bigger mathematical library for Lean that it can draw on. To get a taste of how this is done, there is a game available online called The Natural Number Game [2]. There you can try teaching a computer to count and do basic addition and multiplication – even the most basic facts, like “the natural number after x is x + 1,” are things we need to tell the computer. Being able to count is, of course, a long way from what current research in mathematics looks like. But Lean can be fed more and more complex theorems which al low it to do far more: At the end of 2020, mathematician Peter Scholze had doubts about parts of a proof he wrote. Scholze, a Fields Medalist (footnote 1), works in arithmetic geometry, a field known for being extremely technical and abstract; he and Dustin Clausen had proved a fundamental statement to the field a few years ago, but there were parts of it he was unsure about – and who better to check it than a machine? Hence began the Liquid Tensor Experiment, an attempt to verify their proof using Lean [3]. Figure 1 Exterior angle of a cyclic quadrilateral. Will Mathematicians Be Replaced? – Computer s i n Mathemat ics 數學家會被取代嗎？— 電腦在數學中的角色 By Sonia Choy 蔡蒨珩
RkJQdWJsaXNoZXIy NDk5Njg=