Frustration with mathematics
in [Cryptography]
|
From: Simon Johnson on 30 Jan 2010 18:33 There are many people in this group that will defend, until death, the notion that dense mathematical notion in academic papers is not only required but _necessary_. However, I want to argue that it's the modern day equivelent of holding mass in Latin. To those who don't know Latin it's completely mysterious. To those that known Latin, most of what is stated is often uninteresting and obvious. We now understand that the grammars that (good) programming languages provide are unambigious and relatively easy to understand. Moreover, programming languages allow for powerful abstractions that can hide underlying complexity. These features are perfect for representing mathematics. So I ask, can we not translate the existing body of the mathematics in to such a language and show proofs of the relevant theorems using this grammar? This would make mathematics accessible to people like me. For example, if I wanted to understand the proof of the theorem that AES is resistant to differential cryptanalysis, I could recurse through the proof tree until such a point that the result is obvious. I suspect I will get a lot of replies saying this constitutes a "dumbing down" of mathematics. However, this is simply wrong. The proofs didn't become any easier by doing this. We just wrote them in a language that was machine verifiable. Each step is unambigious and un- bogged down in hundreds of years of notational evolution. It is simpler, purer, and more powerful. In my head, I see this as similiar to when the Arabs discovered the place value system. Overnight, arithmetic became much easier without losing expressivity. This innovation sped up the development of mathematics. Similarly, computers give us the power to formally express mathematics in a language that both humans and computers understand. If anyone can forsee the implications of this, it is the people in this group. The full force of the revolution computers will bring to mathematics has barely been felt. It is my view that the job of scentific papers isn't *just* to educate people within the field. It should also allow people relatively unfamiliar with the subject to at least know where they can go to find more information that provides the context of the paper. Maybe my deep frustration with the state of mathematics papers will not be in vein. There has been a similiar campaign [1] in the UK to clean up legal language so that the text represents legal concepts in an accessible way. For the most part, it has been successful. I want to establish a similar campaign in mathematics. Cheers, Simon [1]- http://www.plainenglish.co.uk/
From: Paul Rubin on 30 Jan 2010 19:01 Simon Johnson <simon.johnson(a)gmail.com> writes: > We now understand that the grammars that (good) programming languages > provide are unambigious and relatively easy to understand. ... > So I ask, can we not translate the existing body of the mathematics in > to such a language and show proofs of the relevant theorems using this > grammar? This would make mathematics accessible to people like me. That is called formalized mathematics and it's a lot harder than you seem to imagine. The most popular languages for the purpose are probably Mizar, Coq, ACL2, and HOL/HOL Light. You might also be interested in the Metamath Proof Explorer: http://us.metamath.org/mpegif/mmset.html In reality though, mathematics (as practiced by humans) doesn't work like that. It's all about the exercise and development of mathematical thought patterns, just like dancing is about the exercise and development of physical motion patterns. > I want to establish a similar campaign in mathematics. There was something like that called the QED Manifesto which didn't get much traction: http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/Extra/wiedijk_2.pdf Some history and critique can be found in the links from the wikipedia article: http://en.wikipedia.org/wiki/QED_manifesto
From: Simon Johnson on 30 Jan 2010 19:55 On Jan 31, 12:01 am, Paul Rubin <no.em...(a)nospam.invalid> wrote: > Simon Johnson <simon.john...(a)gmail.com> writes: > > > We now understand that the grammars that (good) programming languages > > provide are unambigious and relatively easy to understand. ... > > So I ask, can we not translate the existing body of the mathematics in > > to such a language and show proofs of the relevant theorems using this > > grammar? This would make mathematics accessible to people like me. First of all, thank you for the links. They were very interesting. > In reality though, mathematics (as practiced by humans) doesn't work > like that. It's all about the exercise and development of mathematical > thought patterns, just like dancing is about the exercise and > development of physical motion patterns. Having read the articles you linked to, I'm tempted to conclude that if you can't produce a machine verifiable proof what you have is not a proof; it's a conjecture. People objected to the four colour theorem because it was verified by computer and they totally and utterly missed the point. They asked how is it a real proof if a "computer" verified it? What they should have asked is: "hurray, what *else* can we now verify?" I suspect that once machine verification becomes mature, you'll find that there are serious but subtle errors in a large number of proofs. Once these are discovered you'll see a giant (overnight?) watershed on the use of this technology. Anyone who has developed software will be fully aware of the subtle bugs software contains. Formal inspection (which is the norm for mathematics) only removes 90% of bugs. There's going to be some real shockers out there. You might argue that the proving programs will contain errors. They will, that's for sure but it's like double entry book keeping. The fact that you want to prove X with said program reduces errors in both the proof and the program. Moreover, once you've proved that a theorem prover works, that proof extends to any theorem it verifies. Also, the theroem prover is going to be much, much smaller than the set of theorems it proves. This "compression" makes mathematics more robust. > There was something like that called the QED Manifesto which didn't > get much traction: > > http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/Extra/wiedijk_2.... > This work was ahead of its time. Machines were much too slow to realise this dream when this paper was published. I think we have a better shot of doing this today. Saying that " In reality though, mathematics (as practiced by humans) doesn't work" is silly. Mathematics will change to use this. A century ago "computers" were humans who made (many) mistakes producing log tables and the like. Today, they're nearly flawless circuits that compute results to unimaginable levels of accuracy. Tomorrow, most proofs will be submitted in computer verifiable form. I fully expect every single one of the modern mathematicans to have to die to make this happen (as was the case with calculus) but it *will* happen. The question is whether your one of the defeatist conservatives or one of the champions of the movement? Fortune rarely favours the conservative in mathematics. Cheers, Simon
From: Paul Rubin on 30 Jan 2010 20:22 Simon Johnson <simon.johnson(a)gmail.com> writes: > Saying that " In reality though, mathematics (as practiced by humans) > doesn't work" is silly. Mathematics will change to use this. ... > A century ago "computers" were humans who made (many) mistakes > producing log tables and the like. ... Sure, and ditches were dug by laborers with shovels. These days for economic reasons we dig ditches with machines instead. But dancing is still done mostly by humans, even if some people are doing technically and artistically interesting work on programming robots to dance. You might be on the right track if you are talking about machine checkability of certain types of software, including cryptography software, to make sure that the right stuff gets calculated. But more generally, mathematics is not software. Mathematics is about human understanding more than it is about calculation. In that way, it is more like dancing than like ditches, and formalized mathematics is along the same lines as programming robots to dance. Most dancers are simply more interested in how humans dance than in how robots dance. All in all I think you're taking too limited a view of what mathematics is and why people do it. You might like this article by Bill Thurston: http://www.ams.org/bull/1994-30-02/S0273-0979-1994-00502-6/S0273-0979-1994-00502-6.pdf Among other things, as the article describes, it is not exactly news that many mathematical proofs have errors.
From: unruh on 30 Jan 2010 23:11
On 2010-01-30, Simon Johnson <simon.johnson(a)gmail.com> wrote: > There are many people in this group that will defend, until death, the > notion that dense mathematical notion in academic papers is not only > required but _necessary_. > > However, I want to argue that it's the modern day equivelent of > holding mass in Latin. To those who don't know Latin it's completely > mysterious. To those that known Latin, most of what is stated is often > uninteresting and obvious. > > We now understand that the grammars that (good) programming languages > provide are unambigious and relatively easy to understand. Moreover, > programming languages allow for powerful abstractions that can hide > underlying complexity. These features are perfect for representing > mathematics. And you think APL is easier to understand than mathematical notiation? Or that C is an apprpriate language to express say differentiable manifolds in, or Homotopy theory? > > So I ask, can we not translate the existing body of the mathematics in > to such a language and show proofs of the relevant theorems using this > grammar? This would make mathematics accessible to people like me. Can you write a whole book in English never using the letter e. That would be an easy job compared to what you are asking for. > > For example, if I wanted to understand the proof of the theorem that > AES is resistant to differential cryptanalysis, I could recurse > through the proof tree until such a point that the result is obvious. > > I suspect I will get a lot of replies saying this constitutes a > "dumbing down" of mathematics. However, this is simply wrong. The No, it is a stupid exercise. the language of Fortran is just horrible for expressing the concepts required. > proofs didn't become any easier by doing this. We just wrote them in a > language that was machine verifiable. Each step is unambigious and un- they are no more machine verifiable than is English. > bogged down in hundreds of years of notational evolution. It is > simpler, purer, and more powerful. simpler maybe, purer-- you have never programmed anything in your life. More powerful-- hardly. How would you phrase an inductive proof in Basic? > > In my head, I see this as similiar to when the Arabs discovered the > place value system. Overnight, arithmetic became much easier without > losing expressivity. This innovation sped up the development of > mathematics. > > Similarly, computers give us the power to formally express mathematics > in a language that both humans and computers understand. If anyone can > forsee the implications of this, it is the people in this group. The > full force of the revolution computers will bring to mathematics has > barely been felt. That may be, but it sure will not come via trying to express things in Pascal. > > It is my view that the job of scentific papers isn't *just* to educate > people within the field. It should also allow people relatively > unfamiliar with the subject to at least know where they can go to find > more information that provides the context of the paper. And you think that writing it in say Forth would help in this? > > Maybe my deep frustration with the state of mathematics papers will > not be in vein. There has been a similiar campaign [1] in the UK to What are you shooting up here? > clean up legal language so that the text represents legal concepts in > an accessible way. For the most part, it has been successful. > > I want to establish a similar campaign in mathematics. > > Cheers, > > Simon > > [1]- http://www.plainenglish.co.uk/ > > > > > > > |