August 2014 - mathfun@mailman.xmission.com

Re: [math-fun] Game Theory/Chess strategy question
by Guy Haworth 16 Aug '14

16 Aug '14

All chess positions are intrinsically won, drawn or lost for the side to move [Zermelo (?), von Neumann] There may be more than one move which retains the value of the position and this seems to be usually the case. The set of moves SM that progress mate by only one ply may have more than one move in it but usually (so far, about 85% of the time) this appears not to be the case. The set of moves that progress mate to some other objective ('conversion' or 'end of phase') may be different from SM. The set of moves (probably one) that, in a draw situation, maximises the probability of a win against a fallible player may depend on the nature/degree of the opponent's fallibility. I would suggest that 'a strategy' is an algorithm for (successively) filtering down to the chosen move. Papers including the word 'fallible', 'skill', 'skilloscopy' in http://centaur.reading.ac.uk/view/creators/90000763.html may be relevant. A reasonably authority advises me that Lasker was the first to play the opponent as opposed to the ever-present Goddess of Chess, Kaissa. Today, with databases characterising the play of the top players, this is increasingly the case. Tal and Kasparov seem to be examples of players who particularly created 'opportunities to win against fallible players' by not necessarily choosing the best theoretical move. Guy

1 0

[math-fun] Game Theory/Chess strategy question
by Henry Baker 15 Aug '14

15 Aug '14

Everyone who's ever played games like chess quickly learns an opponent's style of play, whether it be aggressively offensive, or methodically defensive. I'm curious about the _types_ of games that encourage offensive strategies v. the types of games that encourage defensive strategies. Some evolutionary biologists have claimed that Darwinian evolution optimizes by using an almost purely offensive strategy. I don't have an opinion one way or another, but was curious about what sorts of environments might favor one strategy versus another.

6 6

[math-fun] Shalosh B. Ekhad: In Computers We Trust?
by Henry Baker 15 Aug '14

15 Aug '14

FYI -- http://www.simonsfoundation.org/quanta/20130222-in-computers-we-trust/ In Computers We Trust? As math grows ever more complex, will computers reign? By: Natalie Wolchover February 22, 2013 Shalosh B. Ekhad, the co-author of several papers in respected mathematics journals, has been known to prove with a single, succinct utterance theorems and identities that previously required pages of mathematical reasoning. Last year, when asked to evaluate a formula for the number of integer triangles with a given perimeter, Ekhad performed 37 calculations in less than a second and delivered the verdict: ÂTrue.Â Shalosh B. Ekhad is a computer. Or, rather, it is any of a rotating cast of computers used by the mathematician Doron Zeilberger, from the Dell in his New Jersey office to a supercomputer whose services he occasionally enlists in Austria. The name Â Hebrew for Âthree B oneÂ Â refers to the AT&T 3B1, EkhadÂs earliest incarnation. ÂThe soul is the software,Â said Zeilberger, who writes his own code using a popular math programming tool called Maple. A mustachioed, 62-year-old professor at Rutgers University, Zeilberger anchors one end of a spectrum of opinions about the role of computers in mathematics. He has been listing Ekhad as a co-author on papers since the late 1980s Âto make a statement that computers should get credit where credit is due.Â For decades, he has railed against Âhuman-centric bigotryÂ by mathematicians: a preference for pencil-and-paper proofs that Zeilberger claims has stymied progress in the field. ÂFor good reason,Â he said. ÂPeople feel they will be out of business.Â Anyone who relies on calculators or spreadsheets might be surprised to learn that mathematicians have not universally embraced computers. To many in the field, programming a machine to prove a triangle identity Â or to solve problems that have yet to be cracked by hand Â moves the goalposts of a beloved 3,000-year-old game. Deducing new truths about the mathematical universe has almost always required intuition, creativity and strokes of genius, not plugging-and-chugging. In fact, the need to avoid nasty calculations (for lack of a computer) has often driven discovery, leading mathematicians to find elegant symbolic techniques like calculus. To some, the process of unearthing the unexpected, winding paths of proofs, and discovering new mathematical objects along the way, is not a means to an end that a computer can replace, but the end itself. In other words, proofs, where computers are playing an increasingly prominent role, are not always the end goal of mathematics. ÂMany mathematicians think they are building theories with the ultimate goal of understanding the mathematical universe,Â said Minhyong Kim, a professor of mathematics at Oxford University and Pohang University of Science and Technology in South Korea. Mathematicians try to come up with conceptual frameworks that define new objects and state new conjectures as well as proving old ones. Even when a new theory yields an important proof, many mathematicians Âfeel itÂs actually the theory that is more intriguing than the proof itself,Â Kim said. Computers are now used extensively to discover new conjectures by finding patterns in data or equations, but they cannot conceptualize them within a larger theory, the way humans do. Computers also tend to bypass the theory-building process when proving theorems, said Constantin Teleman, a professor at the University of California at Berkeley who does not use computers in his work. In his opinion, thatÂs the problem. ÂPure mathematics is not just about knowing the answer; itÂs about understanding,Â Teleman said. ÂIf all you have come up with is Âthe computer checked a million cases,Â then thatÂs a failure of understanding.Â Zeilberger disagrees. If humans can understand a proof, he says, it must be a trivial one. In the never-ending pursuit of mathematical progress, Zeilberger thinks humanity is losing its edge. Intuitive leaps and an ability to think abstractly gave us an early lead, he argues, but ultimately, the unswerving logic of 1s and 0s Â guided by human programmers Â will far outstrip our conceptual understanding, just as it did in chess. (Computers now consistently beat grandmasters.) ÂMost of the things done by humans will be done easily by computers in 20 or 30 years,Â Zeilberger said. ÂItÂs already true in some parts of mathematics; a lot of papers published today done by humans are already obsolete and can be done using algorithms. Some of the problems we do today are completely uninteresting but are done because itÂs something that humans can do.Â Zeilberger and other pioneers of computational mathematics sense that their views have gone from radical to relatively common in the past five years. Traditional mathematicians are retiring, and a tech-savvy generation is taking the helm. Meanwhile, computers have grown millions of times more powerful than when they first appeared on the math scene in the 1970s, and countless new and smarter algorithms, as well as easier-to-use software, have emerged. Perhaps most significantly, experts say, contemporary mathematics is becoming increasingly complex. At the frontiers of some research areas, purely human proofs are an endangered species. ÂThe time when someone can do real, publishable mathematics completely without the aid of a computer is coming to a close,Â said David Bailey, a mathematician and computer scientist at Lawrence Berkeley National Laboratory and the author of several books on computational mathematics. ÂOr if you do, youÂre going to be increasingly restricted into some very specialized realms.Â Teleman studies algebraic geometry and topology Â areas in which most researchers probably now use computers, as with other subfields involving algebraic operations. He focuses on problems that can still be solved without one. ÂAm I doing the kind of math IÂm doing because I canÂt use a computer, or am I doing what IÂm doing because itÂs the best thing to do?Â he said. ÂItÂs a good question.Â Several times in his 20-year career, Teleman has wished he knew how to program so he could calculate the solution to a problem. Each time, he decided to spend the three months he estimated that it would take to learn to program tackling the calculation by hand instead. Sometimes, Teleman said, he will Âstay away from such questions or assign them to a student who can program.Â If doing math without a computer nowadays Âis like running a marathon with no shoes,Â as Sara Billey of the University of Washington put it, the mathematics community has splintered into two packs of runners. The use of computers is both widespread and underacknowledged. According to Bailey, researchers often de-emphasize the computational aspects of their work in papers submitted for publication, possibly to avoid encountering friction. And although computers have been yielding landmark results since 1976, undergraduate and graduate math students are still not required to learn computer programming as part of their core education. (Math faculties tend to be conservative when it comes to curriculum changes, researchers explained, and budget constraints can prevent the addition of new courses.) Instead, students often pick up programming skills on their own, which can sometimes result in byzantine and difficult-to-check code. But whatÂs even more troubling, researchers say, is the absence of clear rules governing the use of computers in mathematics. ÂMore and more mathematicians are learning to program; however, the standards of how you check a program and establish that itÂs doing the right thing Â well, there are no standards,Â said Jeremy Avigad, a philosopher and mathematician at Carnegie Mellon University. In December, Avigad, Bailey, Billey and dozens of other researchers met at the Institute for Computational and Experimental Research in Mathematics, a new research institute at Brown University, to discuss standards for reliability and reproducibility. From myriad issues, one underlying question emerged: In the search for ultimate truth, how much can we trust computers? Computerized Math Mathematicians use computers in a number of ways. One is proof-by-exhaustion: setting up a proof so that a statement is true as long as it holds for a huge but finite number of cases and then programming a computer to check all the cases. More often, computers help discover interesting patterns in data, about which mathematicians then formulate conjectures, or guesses. ÂIÂve gotten a tremendous amount out of looking for patterns in the data and then proving them,Â Billey said. Using computation to verify that a conjecture holds in every checkable case, and ultimately to become convinced of it, Âgives you the psychological strength you need to actually do the work necessary to prove it,Â said Jordan Ellenberg, a professor at the University of Wisconsin who uses computers for conjecture discovery and then builds proofs by hand. Increasingly, computers are helping not only to find conjectures but also to rigorously prove them. Theorem-proving packages such as MicrosoftÂs Z3 can verify certain types of statements or quickly find a counterexample that shows a statement is false. And algorithms like the Wilf-Zeilberger method (invented by Zeilberger and Herbert Wilf in 1990) can perform symbolic computations, manipulating variables instead of numbers to produce exact results free of rounding errors. With current computing power, such algorithms can solve problems whose answers are algebraic expressions tens of thousands of terms long. ÂThe computer can then simplify this to five or 10 terms,Â Bailey said. ÂNot only could a human not have done that, they certainly could not have done it without errors.Â But computer code is also fallible Â because humans write it. Coding errors (and the difficulty in detecting them) have occasionally forced mathematicians to backpedal. In the 1990s, Teleman recalled, theoretical physicists predicted Âa beautiful answerÂ to a question about higher-dimensional surfaces that were relevant to string theory. When mathematicians wrote a computer program to check the conjecture, they found it false. ÂBut the programmers had made a mistake, and the physicists were actually right,Â Teleman said. ÂThatÂs the biggest danger of using a computer proof: What if thereÂs a bug?Â This question preoccupies Jon Hanke. A number theorist and proficient programmer, Hanke thinks mathematicians have grown too trusting of tools that not long ago they frowned upon. He argues that software should never be trusted; it should be checked. But most of the software currently used by mathematicians canÂt be verified. The best-selling commercial math programming tools Â Mathematica, Maple and Magma (each costing about $1,000 per professional license) Â are closed source, and bugs have been found in all of them. ÂWhen Magma tells me the answer is 3.765, how do I know thatÂs really the answer?Â Hanke asked. ÂI donÂt. I have to trust Magma.Â If mathematicians want to maintain the longstanding tradition that it be possible to check every detail of a proof, Hanke says, they canÂt use closed-source software. There is a free, open-source alternative named Sage, but it is less powerful for most applications. Sage could catch up if more mathematicians spent time developing it, Wikipedia-style, Hanke says, but there is little academic incentive to do so. ÂI wrote a whole bunch of open-source quadratic form software in C++ and Sage and used it to prove a theorem,Â Hanke said. In a pre-tenure review of his achievements, Âall that open-source work received no credit.Â After being denied the opportunity for tenure at the University of Georgia in 2011, Hanke left academia to work in finance. Although many mathematicians see an urgent need for new standards, there is one problem that standards canÂt address. Double-checking another mathematicianÂs code is time-consuming, and people might not do it. ÂItÂs like finding a bug in the code that runs your iPad,Â Teleman said. ÂWhoÂs going to find that? How many iPad users are hacking in and looking at the details?Â Some mathematicians see only one way forward: using computers to prove theorems step by step, with cold, hard, unadulterated logic. Proving the Proof In 1998, Thomas Hales astounded the world when he used a computer to solve a 400-year-old problem called the Kepler conjecture. The conjecture states that the densest way to pack spheres is the usual way oranges are stacked in a crate Â an arrangement called face-centered cubic packing. Every street vendor knows it, but no mathematician could prove it. Hales solved the puzzle by treating spheres as the vertices of networks (Âgraphs,Â in math-speak) and connecting neighboring vertices with lines (or ÂedgesÂ). He reduced the infinite possibilities to a list of the few thousand densest graphs, setting up a proof-by-exhaustion. ÂWe then used a method called linear programming to show that none of the possibilities are a counterexample,Â said Hales, now a mathematician at the University of Pittsburgh. In other words, none of the graphs was denser than the one corresponding to oranges in a crate. The proof consisted of about 300 written pages and an estimated 50,000 lines of comp uter code. Hales submitted his proof to the Annals of Mathematics, the fieldÂs most prestigious journal, only to have the referees report four years later that they had not been able to verify the correctness of his computer code. In 2005, the Annals published an abridged version of HalesÂ proof, based on their confidence about the written part. According to Peter Sarnak, a mathematician at the Institute for Advanced Study who until January was an editor of the Annals, the issues broached by HalesÂ proof have arisen repeatedly in the past 10 years. Knowing that important computer-assisted proofs would only become more common in the future, the editorial board has decided to be receptive of such proofs. ÂHowever, in cases where the code is very difficult to check by an ordinary single referee, we will make no claim about the code being correct,Â Sarnak said by email. ÂOur hope in such a case is that the result being proved is sufficiently significant that others might write a similar but independent computer code verifying the assertions.Â HalesÂ response to the refereeing dilemma could change the future of mathematics, according to his colleagues. ÂTom is a remarkable person. He knows no fear,Â Avigad said. ÂGiven that people had raised concern about his proof, he said, ÂOK, the next project is to come up with a formally verified version.Â With no background in the area, he started talking to computer scientists and learning how to do that. Now that project is within a few months of completion.Â To show that his proof was unimpeachable, Hales believed he had to reconstruct it with the most basic building blocks in mathematics: logic itself, and the mathematical axioms. These self-evident truths Â such as Âx=xÂ Â serve as the rule book of mathematics, similar to the way grammar governs the English language. Hales set out to use a technique called formal proof verification in which a computer program uses logic and the axioms to assess each baby step of a proof. The process can be slow and painstaking, but the reward is virtual certainty. The computer ÂdoesnÂt let you get away with anything,Â said Avigad, who formally verified the prime number theorem in 2004. ÂIt keeps track of what youÂve done. It reminds you thereÂs this other case you have to worry about.Â By subjecting his Kepler proof to this ultimate test, Hales hopes to remove all doubt about its veracity. ÂItÂs looking very promising at this point,Â he said. But that isnÂt his only mission. He is also carrying the flag for formal proof technology. With the proliferation of computer-assisted proofs that are all but impossible to check by hand, Hales thinks computers must become the judge. ÂI think formal proofs are absolutely essential for the future development of mathematics,Â he said. Alternative Logic Three years ago, Vladimir Voevodsky, one of the organizers of a new program on the foundations of mathematics at the Institute for Advanced Study in Princeton, N.J., discovered that a formal logic system that was developed by computer scientists, called Âtype theory,Â could be used to re-create the entire mathematical universe from scratch. Type theory is consistent with the mathematical axioms, but couched in the language of computers. Voevodsky believes this alternative way to formalize mathematics, which he has renamed the univalent foundations of mathematics, will streamline the process of formal theorem proving. Voevodsky and his team are adapting a program named Coq, which was designed to formally verify computer algorithms, for use in abstract mathematics. The user suggests which tactic, or logically airtight operation, the computer should employ to check whether a step in the proof is valid. If the tactic confirms the step, then the user suggests another tactic for assessing the next step. ÂSo the proof is a sequence of names of tactics,Â Voevodsky said. As the technology improves and the tactics become smarter, similar programs may someday perform higher-order reasoning on par with or beyond that of humans. Some researchers say this is the only solution to mathÂs growing complexity problem. ÂVerifying a paper is becoming just as hard as writing a paper,Â Voevodsky said. ÂFor writing, you get some reward Â a promotion, perhaps Â but to verify someone elseÂs paper, no one gets a reward. So the dream here is that the paper will come to a journal together with a file in this formal language, and referees simply verify the statement of the theorem and verify that it is interesting.Â Formal theorem proving is still relatively rare in mathematics, but that will change as programs like VoevodskyÂs adaptation of Coq improve, some researchers say. Hales envisions a future in which computers are so adept at higher-order reasoning that they will be able to prove huge chunks of a theorem at a time with little Â or no Â human guidance. ÂMaybe heÂs right; maybe heÂs not,Â Ellenberg said of HalesÂ prediction. ÂCertainly heÂs the most thoughtful and knowledgeable person making that case.Â Ellenberg, like many of his colleagues, sees a more significant role for humans in the future of his field: ÂWe are very good at figuring out things that computers canÂt do. If we were to imagine a future in which all the theorems we currently know about could be proven on a computer, we would just figure out other things that a computer canÂt solve, and that would become Âmathematics.Â Â Teleman doesnÂt know what the future holds, but he knows what kind of math he likes best. Solving a problem the human way, with its elegance, abstraction and element of surprise, is more satisfying to him. ÂThereÂs an element of a notion of failure, I think, when you resort to a computer proof,Â he said. ÂItÂs saying: ÂWe canÂt really do it, so we have to just let the machine run.Â Â Even the most ardent computer fan in mathematics acknowledges a certain tragedy in surrendering to the superior logic of Shalosh B. Ekhad and accepting a supporting role in the pursuit of mathematical truth. After all, itÂs only human. ÂI also get satisfaction from understanding everything in a proof from beginning to end,Â Zeilberger said. ÂBut on the other hand, thatÂs life. Life is complicated.Â Note: This article was updated on March 1, 2013, to provide additional background information about the debate over the role of computers in pure mathematics. http://www.simonsfoundation.org/quanta/20130222-in-computers-we-trust/ In Computers We Trust? As math grows ever more complex, will computers reign? By: Natalie Wolchover February 22, 2013 Shalosh B. Ekhad, the co-author of several papers in respected mathematics journals, has been known to prove with a single, succinct utterance theorems and identities that previously required pages of mathematical reasoning. Last year, when asked to evaluate a formula for the number of integer triangles with a given perimeter, Ekhad performed 37 calculations in less than a second and delivered the verdict: ÂTrue.Â Shalosh B. Ekhad is a computer. Or, rather, it is any of a rotating cast of computers used by the mathematician Doron Zeilberger, from the Dell in his New Jersey office to a supercomputer whose services he occasionally enlists in Austria. The name Â Hebrew for Âthree B oneÂ Â refers to the AT&T 3B1, EkhadÂs earliest incarnation. ÂThe soul is the software,Â said Zeilberger, who writes his own code using a popular math programming tool called Maple. A mustachioed, 62-year-old professor at Rutgers University, Zeilberger anchors one end of a spectrum of opinions about the role of computers in mathematics. He has been listing Ekhad as a co-author on papers since the late 1980s Âto make a statement that computers should get credit where credit is due.Â For decades, he has railed against Âhuman-centric bigotryÂ by mathematicians: a preference for pencil-and-paper proofs that Zeilberger claims has stymied progress in the field. ÂFor good reason,Â he said. ÂPeople feel they will be out of business.Â Anyone who relies on calculators or spreadsheets might be surprised to learn that mathematicians have not universally embraced computers. To many in the field, programming a machine to prove a triangle identity Â or to solve problems that have yet to be cracked by hand Â moves the goalposts of a beloved 3,000-year-old game. Deducing new truths about the mathematical universe has almost always required intuition, creativity and strokes of genius, not plugging-and-chugging. In fact, the need to avoid nasty calculations (for lack of a computer) has often driven discovery, leading mathematicians to find elegant symbolic techniques like calculus. To some, the process of unearthing the unexpected, winding paths of proofs, and discovering new mathematical objects along the way, is not a means to an end that a computer can replace, but the end itself. In other words, proofs, where computers are playing an increasingly prominent role, are not always the end goal of mathematics. ÂMany mathematicians think they are building theories with the ultimate goal of understanding the mathematical universe,Â said Minhyong Kim, a professor of mathematics at Oxford University and Pohang University of Science and Technology in South Korea. Mathematicians try to come up with conceptual frameworks that define new objects and state new conjectures as well as proving old ones. Even when a new theory yields an important proof, many mathematicians Âfeel itÂs actually the theory that is more intriguing than the proof itself,Â Kim said. Computers are now used extensively to discover new conjectures by finding patterns in data or equations, but they cannot conceptualize them within a larger theory, the way humans do. Computers also tend to bypass the theory-building process when proving theorems, said Constantin Teleman, a professor at the University of California at Berkeley who does not use computers in his work. In his opinion, thatÂs the problem. ÂPure mathematics is not just about knowing the answer; itÂs about understanding,Â Teleman said. ÂIf all you have come up with is Âthe computer checked a million cases,Â then thatÂs a failure of understanding.Â Zeilberger disagrees. If humans can understand a proof, he says, it must be a trivial one. In the never-ending pursuit of mathematical progress, Zeilberger thinks humanity is losing its edge. Intuitive leaps and an ability to think abstractly gave us an early lead, he argues, but ultimately, the unswerving logic of 1s and 0s Â guided by human programmers Â will far outstrip our conceptual understanding, just as it did in chess. (Computers now consistently beat grandmasters.) ÂMost of the things done by humans will be done easily by computers in 20 or 30 years,Â Zeilberger said. ÂItÂs already true in some parts of mathematics; a lot of papers published today done by humans are already obsolete and can be done using algorithms. Some of the problems we do today are completely uninteresting but are done because itÂs something that humans can do.Â Zeilberger and other pioneers of computational mathematics sense that their views have gone from radical to relatively common in the past five years. Traditional mathematicians are retiring, and a tech-savvy generation is taking the helm. Meanwhile, computers have grown millions of times more powerful than when they first appeared on the math scene in the 1970s, and countless new and smarter algorithms, as well as easier-to-use software, have emerged. Perhaps most significantly, experts say, contemporary mathematics is becoming increasingly complex. At the frontiers of some research areas, purely human proofs are an endangered species. ÂThe time when someone can do real, publishable mathematics completely without the aid of a computer is coming to a close,Â said David Bailey, a mathematician and computer scientist at Lawrence Berkeley National Laboratory and the author of several books on computational mathematics. ÂOr if you do, youÂre going to be increasingly restricted into some very specialized realms.Â Constantin Teleman, a professor at the University of California at Berkeley, thinks proofs that rely heavily on computation tend not to deepen our understanding of the mathematical universe. (Photo: George Bergman) Teleman studies algebraic geometry and topology Â areas in which most researchers probably now use computers, as with other subfields involving algebraic operations. He focuses on problems that can still be solved without one. ÂAm I doing the kind of math IÂm doing because I canÂt use a computer, or am I doing what IÂm doing because itÂs the best thing to do?Â he said. ÂItÂs a good question.Â Several times in his 20-year career, Teleman has wished he knew how to program so he could calculate the solution to a problem. Each time, he decided to spend the three months he estimated that it would take to learn to program tackling the calculation by hand instead. Sometimes, Teleman said, he will Âstay away from such questions or assign them to a student who can program.Â If doing math without a computer nowadays Âis like running a marathon with no shoes,Â as Sara Billey of the University of Washington put it, the mathematics community has splintered into two packs of runners. The use of computers is both widespread and underacknowledged. According to Bailey, researchers often de-emphasize the computational aspects of their work in papers submitted for publication, possibly to avoid encountering friction. And although computers have been yielding landmark results since 1976, undergraduate and graduate math students are still not required to learn computer programming as part of their core education. (Math faculties tend to be conservative when it comes to curriculum changes, researchers explained, and budget constraints can prevent the addition of new courses.) Instead, students often pick up programming skills on their own, which can sometimes result in byzantine and difficult-to-check code. But whatÂs even more troubling, researchers say, is the absence of clear rules governing the use of computers in mathematics. ÂMore and more mathematicians are learning to program; however, the standards of how you check a program and establish that itÂs doing the right thing Â well, there are no standards,Â said Jeremy Avigad, a philosopher and mathematician at Carnegie Mellon University. In December, Avigad, Bailey, Billey and dozens of other researchers met at the Institute for Computational and Experimental Research in Mathematics, a new research institute at Brown University, to discuss standards for reliability and reproducibility. From myriad issues, one underlying question emerged: In the search for ultimate truth, how much can we trust computers? Computerized Math Mathematicians use computers in a number of ways. One is proof-by-exhaustion: setting up a proof so that a statement is true as long as it holds for a huge but finite number of cases and then programming a computer to check all the cases. More often, computers help discover interesting patterns in data, about which mathematicians then formulate conjectures, or guesses. ÂIÂve gotten a tremendous amount out of looking for patterns in the data and then proving them,Â Billey said. Using computation to verify that a conjecture holds in every checkable case, and ultimately to become convinced of it, Âgives you the psychological strength you need to actually do the work necessary to prove it,Â said Jordan Ellenberg, a professor at the University of Wisconsin who uses computers for conjecture discovery and then builds proofs by hand. Increasingly, computers are helping not only to find conjectures but also to rigorously prove them. Theorem-proving packages such as MicrosoftÂs Z3 can verify certain types of statements or quickly find a counterexample that shows a statement is false. And algorithms like the Wilf-Zeilberger method (invented by Zeilberger and Herbert Wilf in 1990) can perform symbolic computations, manipulating variables instead of numbers to produce exact results free of rounding errors. With current computing power, such algorithms can solve problems whose answers are algebraic expressions tens of thousands of terms long. ÂThe computer can then simplify this to five or 10 terms,Â Bailey said. ÂNot only could a human not have done that, they certainly could not have done it without errors.Â But computer code is also fallible Â because humans write it. Coding errors (and the difficulty in detecting them) have occasionally forced mathematicians to backpedal. In the 1990s, Teleman recalled, theoretical physicists predicted Âa beautiful answerÂ to a question about higher-dimensional surfaces that were relevant to string theory. When mathematicians wrote a computer program to check the conjecture, they found it false. ÂBut the programmers had made a mistake, and the physicists were actually right,Â Teleman said. ÂThatÂs the biggest danger of using a computer proof: What if thereÂs a bug?Â This question preoccupies Jon Hanke. A number theorist and proficient programmer, Hanke thinks mathematicians have grown too trusting of tools that not long ago they frowned upon. He argues that software should never be trusted; it should be checked. But most of the software currently used by mathematicians canÂt be verified. The best-selling commercial math programming tools Â Mathematica, Maple and Magma (each costing about $1,000 per professional license) Â are closed source, and bugs have been found in all of them. ÂWhen Magma tells me the answer is 3.765, how do I know thatÂs really the answer?Â Hanke asked. ÂI donÂt. I have to trust Magma.Â If mathematicians want to maintain the longstanding tradition that it be possible to check every detail of a proof, Hanke says, they canÂt use closed-source software. There is a free, open-source alternative named Sage, but it is less powerful for most applications. Sage could catch up if more mathematicians spent time developing it, Wikipedia-style, Hanke says, but there is little academic incentive to do so. ÂI wrote a whole bunch of open-source quadratic form software in C++ and Sage and used it to prove a theorem,Â Hanke said. In a pre-tenure review of his achievements, Âall that open-source work received no credit.Â After being denied the opportunity for tenure at the University of Georgia in 2011, Hanke left academia to work in finance. Although many mathematicians see an urgent need for new standards, there is one problem that standards canÂt address. Double-checking another mathematicianÂs code is time-consuming, and people might not do it. ÂItÂs like finding a bug in the code that runs your iPad,Â Teleman said. ÂWhoÂs going to find that? How many iPad users are hacking in and looking at the details?Â Some mathematicians see only one way forward: using computers to prove theorems step by step, with cold, hard, unadulterated logic. Proving the Proof In 1998, Thomas Hales astounded the world when he used a computer to solve a 400-year-old problem called the Kepler conjecture. The conjecture states that the densest way to pack spheres is the usual way oranges are stacked in a crate Â an arrangement called face-centered cubic packing. Every street vendor knows it, but no mathematician could prove it. Hales solved the puzzle by treating spheres as the vertices of networks (Âgraphs,Â in math-speak) and connecting neighboring vertices with lines (or ÂedgesÂ). He reduced the infinite possibilities to a list of the few thousand densest graphs, setting up a proof-by-exhaustion. ÂWe then used a method called linear programming to show that none of the possibilities are a counterexample,Â said Hales, now a mathematician at the University of Pittsburgh. In other words, none of the graphs was denser than the one corresponding to oranges in a crate. The proof consisted of about 300 written pages and an estimated 50,000 lines of computer co de. Hales submitted his proof to the Annals of Mathematics, the fieldÂs most prestigious journal, only to have the referees report four years later that they had not been able to verify the correctness of his computer code. In 2005, the Annals published an abridged version of HalesÂ proof, based on their confidence about the written part. According to Peter Sarnak, a mathematician at the Institute for Advanced Study who until January was an editor of the Annals, the issues broached by HalesÂ proof have arisen repeatedly in the past 10 years. Knowing that important computer-assisted proofs would only become more common in the future, the editorial board has decided to be receptive of such proofs. ÂHowever, in cases where the code is very difficult to check by an ordinary single referee, we will make no claim about the code being correct,Â Sarnak said by email. ÂOur hope in such a case is that the result being proved is sufficiently significant that others might write a similar but independent computer code verifying the assertions.Â HalesÂ response to the refereeing dilemma could change the future of mathematics, according to his colleagues. ÂTom is a remarkable person. He knows no fear,Â Avigad said. ÂGiven that people had raised concern about his proof, he said, ÂOK, the next project is to come up with a formally verified version.Â With no background in the area, he started talking to computer scientists and learning how to do that. Now that project is within a few months of completion.Â To show that his proof was unimpeachable, Hales believed he had to reconstruct it with the most basic building blocks in mathematics: logic itself, and the mathematical axioms. These self-evident truths Â such as Âx=xÂ Â serve as the rule book of mathematics, similar to the way grammar governs the English language. Hales set out to use a technique called formal proof verification in which a computer program uses logic and the axioms to assess each baby step of a proof. The process can be slow and painstaking, but the reward is virtual certainty. The computer ÂdoesnÂt let you get away with anything,Â said Avigad, who formally verified the prime number theorem in 2004. ÂIt keeps track of what youÂve done. It reminds you thereÂs this other case you have to worry about.Â By subjecting his Kepler proof to this ultimate test, Hales hopes to remove all doubt about its veracity. ÂItÂs looking very promising at this point,Â he said. But that isnÂt his only mission. He is also carrying the flag for formal proof technology. With the proliferation of computer-assisted proofs that are all but impossible to check by hand, Hales thinks computers must become the judge. ÂI think formal proofs are absolutely essential for the future development of mathematics,Â he said. Alternative Logic Three years ago, Vladimir Voevodsky, one of the organizers of a new program on the foundations of mathematics at the Institute for Advanced Study in Princeton, N.J., discovered that a formal logic system that was developed by computer scientists, called Âtype theory,Â could be used to re-create the entire mathematical universe from scratch. Type theory is consistent with the mathematical axioms, but couched in the language of computers. Voevodsky believes this alternative way to formalize mathematics, which he has renamed the univalent foundations of mathematics, will streamline the process of formal theorem proving. Voevodsky and his team are adapting a program named Coq, which was designed to formally verify computer algorithms, for use in abstract mathematics. The user suggests which tactic, or logically airtight operation, the computer should employ to check whether a step in the proof is valid. If the tactic confirms the step, then the user suggests another tactic for assessing the next step. ÂSo the proof is a sequence of names of tactics,Â Voevodsky said. As the technology improves and the tactics become smarter, similar programs may someday perform higher-order reasoning on par with or beyond that of humans. Some researchers say this is the only solution to mathÂs growing complexity problem. ÂVerifying a paper is becoming just as hard as writing a paper,Â Voevodsky said. ÂFor writing, you get some reward Â a promotion, perhaps Â but to verify someone elseÂs paper, no one gets a reward. So the dream here is that the paper will come to a journal together with a file in this formal language, and referees simply verify the statement of the theorem and verify that it is interesting.Â Formal theorem proving is still relatively rare in mathematics, but that will change as programs like VoevodskyÂs adaptation of Coq improve, some researchers say. Hales envisions a future in which computers are so adept at higher-order reasoning that they will be able to prove huge chunks of a theorem at a time with little Â or no Â human guidance. ÂMaybe heÂs right; maybe heÂs not,Â Ellenberg said of HalesÂ prediction. ÂCertainly heÂs the most thoughtful and knowledgeable person making that case.Â Ellenberg, like many of his colleagues, sees a more significant role for humans in the future of his field: ÂWe are very good at figuring out things that computers canÂt do. If we were to imagine a future in which all the theorems we currently know about could be proven on a computer, we would just figure out other things that a computer canÂt solve, and that would become Âmathematics.Â Â Teleman doesnÂt know what the future holds, but he knows what kind of math he likes best. Solving a problem the human way, with its elegance, abstraction and element of surprise, is more satisfying to him. ÂThereÂs an element of a notion of failure, I think, when you resort to a computer proof,Â he said. ÂItÂs saying: ÂWe canÂt really do it, so we have to just let the machine run.Â Â Even the most ardent computer fan in mathematics acknowledges a certain tragedy in surrendering to the superior logic of Shalosh B. Ekhad and accepting a supporting role in the pursuit of mathematical truth. After all, itÂs only human. ÂI also get satisfaction from understanding everything in a proof from beginning to end,Â Zeilberger said. ÂBut on the other hand, thatÂs life. Life is complicated.Â Note: This article was updated on March 1, 2013, to provide additional background information about the debate over the role of computers in pure mathematics.

1 0

[math-fun] Mathematica
by Bill Gosper 15 Aug '14

15 Aug '14

S.Plouffe>or worst : ImplicitRungeKuttaLobattoIIIBCoefficients < Several versions back, NeilB found the longest name to be MultivariateHypergeometricDistribution But the Predictive Interface will save you typing this. Thane> For example something like this subsets[list_] := Distribute[Map[{{},{#}}&,list], List, List, List, Union] gives me a headache to even look at. < That's unacceptably transpicuous! subsets[list_] := Distribute[{{},{#}}&/@list, List, List, List, Union] Of course, the installed function Subsets offers this, plus a bewilderment of bells and whistles. Looking in my toolbox, e.g., Brill2sqs[p_Integer] := NestWhile[{#[[2]], Mod @@ #} &, {p, #}, #1[[1]]^2 > p &] & /@ Select[#[[1, 2]] & /@ Solve[z^2 == -1, Modulus -> p], # < p/2 &] But what I *always* get wrong is the semantics of Sequence, e.g. st0[{f_, n_, M_?MatrixQ, cf___}] := Block[{xy = Divide @@ M, t}, If[Floor@xy[[1]] == (t = Floor@xy[[2]]), Join[{f, Sow[n]}, {{{0, 1}, {1, -t}}.M, Sequence @@ {cf, t}}], xy = M.f[n]; {f, n + 1, xy/GCD @@ Join @@ xy, cf}]] And nearly always get wrong: Hold, ReleaseHold, HoldPattern, Verbatim, Unevaluated, plus the rules for the spontaneous disappearance of wrappers, e.g. MatrixForm. It's a baroque language, at once too terse and too verbose. Perhaps unavoidable consequences of an *enormity* of functionality. One of the kids tells me "Version 10 is great!" Despite having grown only 800 functions since Version 9. --rwg

1 0

[math-fun] (no subject)
by Eugene Salamin 15 Aug '14

15 Aug '14

I'm reading a book on general relativity, and the author makes a statement giving a proof that I don't find convincing. Suppose we wish to construct a scalar R (i.e. R(x') = R(x) under coordinate transformations) from the metric tensor and two powers of differentiation. That is, R must consist of terms of the form (∂∂g) and (∂g)(∂g). The claim is that R must be the scalar curvature, except for a multiplicative constant. Can someone point me to a proof? The importance of this result is that the Einstein-Hilbert action for the dynamics of spacetime is then uniquely determined. Well, unique in the absence of the cosmological constant. -- Gene

7 8

Re: [math-fun] Mathematica
by Henry Baker 14 Aug '14

14 Aug '14

I've been using Macsyma/Maxima pretty much since Joel Moses developed it. It has had a very rocky career, and had the extreme misfortune to be developed prior to the open source movement. Even though I love Lisp, I have lots of complaints about Macsyma/Maxima, most of which stem from the fact that it is probably the least mathematical thing that a mathematician will ever have to deal with. For example, one is never quite sure what ring or field one is working in -- e.g., whether (x-a)/(x-a)=1 or not. A truly mathematical algebraic manipulation system would force the user to be very precise about all of these things, but this level of precision might range from being merely scolding to being unusably anal. An analogy with precise type-checking in computer languages is in order here; without some form of type inference, dealing with some strongly typed languages would be unbearable. Macsyma/Maxima never really got any kind of formal semantics, and Joel Moses's own discussions about "what is a variable" are quite hand-wavey. Nevertheless, Macsyma/Maxima remains an incredibly flexible tool in the right hands. I would personally like to see a mathematical algebra tool that could be tightened up (when desired) into a proof-checker for automatically verifying proofs. I have personally used Maxima to algebraically verify a number of proofs normally done with geometric reasoning, and it was painful, but very educational. At 03:53 PM 8/14/2014, Eugene Salamin via math-fun wrote: >Mathematica is unreadable. I simply ignore Mathematica code in the math-fun posts. I'll use Sage as far as possible, and would consider buying the student version of Maple. Now, Macsyma was a complete winner. But due to a very bad decision, it is now being held hostage, and no reasonable person would pay the ransom for its release. > > -- Gene >>________________________________ >> From: Dan Asimov <dasimov(a)earthlink.net> >>To: Eugene Salamin <gene_salamin(a)yahoo.com>; math-fun <math-fun(a)mailman.xmission.com> >>Sent: Thursday, August 14, 2014 3:14 PM >>Subject: Mathematica >> >>Is it just my imagination, or is Mathematica syntax between 5 and 100 times as clunky as it needs to be? >> >>Sometimes I feel it's like programming with Cobol^Cobol. >> >>--Dan

1 0

Re: [math-fun] Mathematica
by Warren D Smith 14 Aug '14

14 Aug '14

I'm now using "maxima," a freeware and not very good version of macsyma, and it's quite bad.

1 0

[math-fun] Maryam Mirzakhani first female Fields Medal winner (Tehran-Iran born prof. at Stanford)
by Warren D Smith 14 Aug '14

14 Aug '14

and what did she actually do? http://en.wikipedia.org/wiki/Maryam_Mirzakhani says some stuff, but basically I did not understand a word of this. http://www.mathunion.org/fileadmin/IMU/Prizes/2014/news_release_mirzakhani.… contains a few actually comprehensible claims. Despite Iran culture and education system allegedly being anti-female, unlike the enlightened West, you'll notice the first female Fields medalist came from Iran.

5 4

[math-fun] fields medals, randomness, women
by Warren D Smith 14 Aug '14

14 Aug '14

Well, in at least some parts of Afghanistan, girls trying to be educated caused disasters where they were brutalized, raped, or it was considered some kind of horrible religious offense that they should even be allowed to be educated. In Maryam Mirzakhani's case, though, she was educated in schools and undergraduate college in Iran and apparently was quite pro-active and non-shy about it, requesting and getting special education. Apparently she had a sympathetic headmaster in her school who wanted to help her. ------------ This Guardian piece S.Anderson pointed me to re the field medalists seems quite excellent... but that is since they just copied it from the IMU: http://www.theguardian.com/science/alexs-adventures-in-numberland/2014/aug/… "Another outstanding result of Avila is his work, with Giovanni Forni, on weak mixing. If one attempts to shuffle a deck of cards by only cutting the deck - that is, taking a small stack off the top of the deck and putting the stack on the bottom - then the deck will not be truly mixed. ... but if a closed interval is cut into several subintervals... e.g. cut into four pieces, ABCD, and then one defines a map on the interval by exchanging the positions of the subintervals so that, say, ABCD goes to DCBA. (Always apply a "derangement" permutation.) By iterating the map, one obtains a dynamical system called an 'interval exchange transformation'. Avila and Forni showed that almost every interval exchange transformation is weakly mixing; in other words, if one chooses at random an interval exchange transformation, the overwhelmingly likelihood is that, when iterated, it will produce a dynamical system that is weakly mixing." --that could be used to make a pseudo-random number generator, by iterating a 4 piece bijective map, each piece of the form x --> x+a. However, this would be fairly poor since it will require a large number of iterations (at least comparable to the number of bits in a machine word) before it becomes likely that adjacent integer x are no longer. Also, it seems to need "if" statements, which are somewhat slow. Still, it might be a useful ingredient in a combination generator... http://w3.impa.br/~avila/qmath.pdf considers a certain linear "Schrodinger" operator arising in a 1-dimensional physics model, the "wave function" being defined only at integer locations. This is just an infinite matrix. Avila & Jitomirskaya prove the eigenvalue spectrum of this matrix, is a Cantor set. My mind is somewhat boggled. I mean, the matrix is countably-infinite-dimensional. A Cantor set, although 'discrete', has the same cardinality as the real numbers. How can the number of eigenvalues exceed the number of dimensions of the matrix??? http://en.wikipedia.org/wiki/Cantor_set#Cardinality "Bhargava asked, what can be said about the rational points on a typical curve? In joint work with Arul Shankar and also with Christopher Skinner, Bhargava came to the surprising conclusion that a positive proportion of elliptic curves have only one rational point and a positive proportion have infinitely many. Analogously, in the case of hyperelliptic curves of degree 4, Bhargava showed that a positive proportion of such curves have no rational points and a positive proportion have infinitely many rational points. For higher degree hyperelliptic curves... the typical hyperelliptic curve has no rational points at all." --this is useful for generating conjectures... Martin Hairer: his work sounds potentially very important for trying to rigorize physics. "Mirzakhani... closed geodesics on a hyperbolic surface. These are closed curves whose length cannot be shortened by deforming them. A now-classic theorem proved more than 50 years ago gives a precise way of estimating the number of closed geodesics whose length is less than some bound L. The number of closed geodesics grows exponentially with L; specifically, it is asymptotic to exp(L)/L for large L... Mirzakhani looked at what happens to this 'prime number theorem for geodesics' when one considers only the closed geodesics that are simple, meaning that they do not intersect themselves. The behavior is very different in this case: the growth of the number of geodesics of length at most L is no longer exponential in L but asymptotic to c*L^(6g - 6) for large L (going to infinity), where the constant c depends on the hyperbolic structure and g is the genus of the surface." She apparently knows all about "moduli space", whatever that is. "Mirzakhani, showed the system known as the 'earthquake flow,' which was introduced by William Thurston (a 1982 Fields Medalist), is chaotic." --what the hell did that mean? I think, not sure, that the "earthquake map" means this. If you have a hyperbolic surface (i.e. closed 2-manifoldl with constant negative curvature) and it has some simple closed geodesics then cut it along the geodesic then glue it back together shifted circularly. One could also do this for, say, a sphere (cut along a great circle and glue back one half rotated), or a flat torus. Is that right? What is the meaning of what it is claimed she proved? -- Warren D. Smith http://RangeVoting.org <-- add your endorsement (by clicking "endorse" as 1st step)

1 0

[math-fun] OEIS-50 conference in October
by Neil Sloane 14 Aug '14

14 Aug '14

Announcement: A conference on Challenges of Identifying Integer Sequences will be hold at DIMACS (Rutgers) on October 9 and 10 2014. This will celebrate 50 years of the OEIS, 250,000 sequences, and my 75th birthday. See http://dimacs.rutgers.edu/Workshops/OEIS/announcement.html. Invited speakers include Jörg Arndt, Sara Billey, John Conway, Russ Cox, Edinah Gnang, Doug Hofstadter, Jeff C. Lagarias, Lara Pudwell, Jeffrey Shallit, Neil Sloane, Michael Somos, Richard Stanley, Bridget Tenner, Space is limited but there is still room. Young people, teachers, etc. may qualify for reduced registration. Travel funds may also be available for young people. Hope to see you in October. Neil -- Dear Friends, I have now retired from AT&T. New coordinates: Neil J. A. Sloane, President, OEIS Foundation 11 South Adelaide Avenue, Highland Park, NJ 08904, USA. Also Visiting Scientist, Math. Dept., Rutgers University, Piscataway, NJ. Phone: 732 828 6098; home page: http://NeilSloane.com Email: njasloane(a)gmail.com

1 0