6 ms·

Are there practical applications for proving theorems? It seems like it's the full employment act for pencil pushers. edit: downvoters downvote instead of prov

Are there practical applications for proving theorems? It seems like it's the full employment act for pencil pushers. edit: downvoters downvote instead of providing refutation. A lot in common with fundamental religionists.

klodolph 14y ago
If you can't prove a theorem, then it's not a theorem, it's a conjecture. Conjectures are not as useful. For example, the Shannon-Hartley theorem tells us under what circumstances it is possible to decode a radio signal. That theorem lets us design, e.g., cell phone networks. Theorems are useful in all sorts of unexpected ways. At the turn of the 20th century group theory was considered a worthless corner of mathematics, but understanding group theory allows modern chemical instrumentation to work. edit: > It seems like it's the full employment act for pencil pushers > downvoters downvote instead of providing refutation. A lot in common with fundamental religionists You've proven the downvoters right by piling one ad hominem attack upon another.
- marshallp 14y ago
  The example you've described (radio signals) is just a method of winning an argument. It doesn't actually help you, you practically do it by writing a computer program that tries out different parameters to get the right one.
  - klodolph 14y ago
    I'll explain in more detail. Let's say you need a communications channel with a 300 Mbit/s capacity. Shannon's theorem lets you know what kind of parameters make that possible -- namely, bandwidth and signal-to-noise ratio. From there, I can make an informed decision about the entire signal chain. Once I choose the bandwidth, the theorem tells me the SNR so I can assign a noise budget to each of the components. If we assume that the noise is Gaussian, we can calculate total noise level as the root sum of squares of the noise levels of the individual components (don't forget to multiply by the gain). I can look at an amplifier IC's spec sheet and immediately say, "that's too noisy" or "that's overdesigned, I think I can get something cheaper". And thanks to theorems we got from the field of real analysis and statistics, we know that the sum of Gaussians is itself Gaussian. So rather than sticking two components together and measuring the noise, or running a computer simulation, I can simply square, sum, and square root. Each of these theorems reduces the amount of work necessary -- whether by pen and paper or by computer -- by an enormous factor. But if you can describe in similar detail how the computer program would work, I'll acknowledge your greatness.
    - marshallp 14y ago
      That's just a few parameters that you avoided having to tune, a few milliseconds of computer time. I'm not great, just questioning basic assumptions that have been handed down from a time before computers were around.
      - klodolph 14y ago
        You keep on asserting that the task -- without domain knowledge of Shannon's theorem -- is solvable by computer. Can you describe how such a computer program would work? I'm unconvinced that the computer program would get a reasonable result before you run out of money paying for it.
        marshallp 14y ago
        The Shannon theorem is basically voided by compressive sensing. But all of this (shannon+compressive) was a waste of practical people's time anyway. It's justification for pencil pushers who don't want to do real work.
        karategeek6 14y ago
        http://www.youtube.com/watch?v=1orMXD_Ijbs&feature=related http://www.youtube.com/watch?v=1orMXD_Ijbs&feature=relat...
      - darkarmani 14y ago
        > That's just a few parameters that you avoided having to tune, a few milliseconds of computer time. Really? What happens when you need to do a similar calculation across hundreds of millions of data points?
  - geoka9 14y ago
    How about solving differential equations numerically. Such programs are used all over the place in mathematical modeling, with applications ranging from economics to electronics. And you can't just "write a computer program that tries different parameters". You have to prove that your numerical method solves a certain class of equations first, otherwise your rocket will fly sideways, if at all.
    - marshallp 14y ago
      The intelligent way to do that nowadays is to use automatic differentiation followed by optimization "plugins". And that has little to with proving theorems unless you consider all computer programs as proofs and all computer programmers as mathematicians.
      - geoka9 14y ago
        I'm not sure what automatic differentiation has to do with solving diff. equations but... I assume that all those automatic methods you mention are passed down from above in some sort of holy scriptures that we're supposed to blindly believe and use? Or maybe some "pencil pushing" mathematician came up with them first and _proved_ that they actually work?
        marshallp 14y ago
        If you're solving DE's by hand you were probably just in a class taught by members of the Mathematician-Teaching Complex (allusion to Military-Industrial Complex).
Evbn 14y ago
You might be interested in the up and coming fields of 3D video games, flight simulators, CG movies, machine learning, supply logistics, autonomous navivations, colonization of Mars, and your personal favorite algorithmic trading, all brought to you by "theorems" of linear algebra.
- marshallp 14y ago
  None of those require theorems, they require computers.
  - gizmo686 14y ago
    Great news, I finally wrote a sorting algorithm that worked for 10/10 of my test cases. Now, I can just plug that number into my unproven statisticle test, and found out how likely it is that my algorithm will work for all inputs. It does not seem to run extra slow for any input, so it probably won't run slowly on any input in actual use. Besides, even if it did I would have no way of proving what types of inputs it failed on, or if another algorithm would do better.
    - marshallp 14y ago
      http://ertos.nicta.com.au/research/l4.verified/proof.pml http://ertos.nicta.com.au/research/l4.verified/proof.pml Keeping the above in mind, does it actually justify the billions of man hours spent on mathematics.
  - saraid216 14y ago
    The notion of a computer was a theorem. http://en.wikipedia.org/wiki/Turing_completeness http://en.wikipedia.org/wiki/Turing_completeness
    - marshallp 14y ago
      The computer industry wasn't built on Turing completeness. It's an evolution of practical technology starting with the invention of textile machinery (but you can also kind of argue it started with abacuses or even lines drawn in sand).
saurabh 14y ago
Proving theorems has theoretical applications. And the knowledge gained by doing so may have practical applications.
plinkplonk 14y ago
Exhibit 1: you say "Are there practical applications for proving theorems?" Exhibit 2: In your profile, you describe yourself as "Machine Learning Expert" Hmm.
- marshallp 14y ago
  Yeah, there's pencil pushing frauds (mathemagicians) in machine learning too.
  - mreid 14y ago
    I see that you use VW for machine learning. You should ask the lead developer (John Langford) what he thinks of the efficacy of mathematics for machine learning given most of the algorithms it uses were derived from theoretical considerations (e.g., SGD, LDA, reductions, etc.) Would you describe him as a "pencil pushing fraud" too?
    - marshallp 14y ago
      Yes, he's a pencil pushing fraud for the most part (he might even admit it in private). I don't know how old he is but assuming he's been professional for 10 years, his big contribution is the few hundred/thousand lines of VW (he's probably done other work, but let's assume this is a significant fraction). Where did the rest of his time go? If he just decided to bang VW out a decade ago he'd be at it's current state within a month of starting. VW is only useful because it's fast and it works (and that's not due to any theory). It's theoretical considerations are useful only for essentially drawing that 1 month out to years/decades.
      - mreid 14y ago
        I'll ask him whether he considers himself mostly a pencil pushing fraud when I see him in December. I'll also see what he thinks of the claim that VW's usefulness is "not due to any theory". I'll think you'll be surprised given he's written a blog post on this topic titled "Use of Learning Theory" http://hunch.net/?p=496 http://hunch.net/?p=496 at his blog which, by the way, is called "Machine Learning (Theory)". It's easy to dismiss what you don't understand but you should consider the possibility that it is significantly more difficult develop algorithms like those in VW and "bang out" implementations of them that are fast and correct.
ColinWright 14y ago
I'm curious - you seem to be saying that theorems are useless, and instead, all we ever need to do is write programs to twiddle the numbers and work things out that way. So what would you need me to do to show that proving theorems is important? What would convince you? What is your criterion for a successful response?
- marshallp 14y ago
  What is the criterion you would give an astrologer? I'm not equating them with astrology, but simply pointing out the countless billions wasted on mathematics that narrows to the rarefied "breed" of pure mathematician earning a salary is as much of a waste as if billions were spent on buggy whip boys. Some things are just meant to fade into museums and history books.
  - mreid 14y ago
    There is no argument that fundamental research (including, but not limited to pure mathematics) is a high-risk investment with a small chance of a large pay-off. But, like most good, high-risk investments the potential pay-offs can be massive and, importantly, not always well-understood in advance. Would we have GPS without relativity which in turn depends on non-Euclidean geometry, initially considered a curiosity? What about public key encryption, built upon number theory, proudly described as "useless" by the pure mathematician G.W. Hardy? There are so many examples like these. Be careful of committing the fallacy in assuming that because a clear line of ideas can be traced back from the present day that finding that line was as easy as recounting it. Out of interest, what is your position of the spending on sport, the arts, and other cultural endeavours?
    - marshallp 14y ago
      People are tired of me criticizing maths on here so I'll stop with it. My opinion on sports, arts etc. is the same. Publicly funded stuff is basically for the elite anyway, it's their way of cleverly siphoning tax-payer money (for there boring outdated interests which they partake in to show the illusion of sophistication). The masses pay to see their interests (and usually heavily taxed for it to boot).
regularfry 14y ago
We can't have provably correct software without theorem proofs. Provably correct software is a good thing.
thedigitalengel 14y ago
Would you feel secure about using a cryptographic system without a proof?
Cogito 14y ago
'Proving Theorems' is a grand sounding statement, but the reality need not be so glamorous! A Theorem as a thing is an encapsulation of a granule of knowledge or, even less precisely, something learnt which is known to be true[1]. To prove a Theorem is to show that the knowledge it encapsulates is correct. Why is this good? Most theory I have read[2] on AI, machine learning, and knowledge deals in depth with the concept of symbols and symbol manipulation. Some would claim (correctly!) that computers are in essence simply symbol manipulation machines. The thing is, these symbols are really just ways of encapsulating a piece of information. Often, symbols are described as being 'made-up' of other symbols; symbols are used to describe other symbols. As a simple and obvious example: - bits (low level 'axiomatic' symbols) are organised into groups to create bytes (still low level, not much meaning here yet) - bytes are associated with letters (in an isomorphic relation which imparts meaning[3]) - letters are organised into groups to form words (a significant amount of meaning has now appeared) - words are strung together in sentences - sentences are woven into paragraphs/chapters/themes/poems/stories/epics If I was to claim that a poem or story has no meaning simply because I can craft it from simple bits I would be missing something very important about symbol manipulation. When I take a collection of ideas, snippets of information and learning, and am able to label them with a name I can transcend my current level of understanding and deal with ideas which are invisible on the lower level. For a programmer, this hierarchy of symbols presents itself as a hierarchy of low, medium and high level languages. Writing a python program in assembly would be absurd!(although perhaps appropriate in some cases) Theorems (and Axioms) are the symbols of mathematics, and proving Theorems is symbolic manipulation in one of its purest forms. In fact, proving Theorems is the main way in which new 'meaningful'[4] symbols are created. So why is proving Theorems useful? In short, because it is how new knowledge is created! (in this context, mathematical knowledge) Is mathematical knowledge useful? I think anyone living in this modern world of ours (and I think that phrase applies to most people in most of humanity's history) can see that at least some mathematics is useful. Many have here argued about the different merits of developing mathematical knowledge (ie proving Theorems) before an application is well known, so I won't labour that point. Instead, I think I'll direct the interested reader to G.H. Hardy's 'A Mathematician's Apology'[5] for a great essay on the many merits a joy of mathematics can bring the suitably inclined soul. If knowledge is a good thing, and proving Theorems increases knowledge, than proving Theorems is a good thing. To say it is better than other ways of spending our efforts is hard, but I think we can definitely agree that it is useful. [1] My own definition! [2] Which is tragically less than I would like [3] Douglas Hofstadter in Gödel, Escher, Bach explains this idea so much better than I can - see https://en.wikipedia.org/wiki/Gödel,_Escher,_Bach https://en.wikipedia.org/wiki/Gödel,_Escher,_Bach [4] An idea again borrowed from Hofstadter. We can string any string of words together that we want, doesn't mean that they mean anything to us. Formal system such as mathematics give us a way to combine symbols to give us new meaningful symbols. My claim that it is the main way they are created is founded on wild speculation and heavily biased historical observation. [5] http://www.math.ualberta.ca/~mss/misc/A%20Mathematicians%20Apology.pdf http://www.math.ualberta.ca/~mss/misc/A%20Mathematicians%20A...

klodolph 14y ago

If you can't prove a theorem, then it's not a theorem, it's a conjecture. Conjectures are not as useful. For example, the Shannon-Hartley theorem tells us under what circumstances it is possible to decode a radio signal. That theorem lets us design, e.g., cell phone networks. Theorems are useful in all sorts of unexpected ways. At the turn of the 20th century group theory was considered a worthless corner of mathematics, but understanding group theory allows modern chemical instrumentation to work. edit: > It seems like it's the full employment act for pencil pushers > downvoters downvote instead of providing refutation. A lot in common with fundamental religionists You've proven the downvoters right by piling one ad hominem attack upon another.

marshallp 14y ago
The example you've described (radio signals) is just a method of winning an argument. It doesn't actually help you, you practically do it by writing a computer program that tries out different parameters to get the right one.
- klodolph 14y ago
  I'll explain in more detail. Let's say you need a communications channel with a 300 Mbit/s capacity. Shannon's theorem lets you know what kind of parameters make that possible -- namely, bandwidth and signal-to-noise ratio. From there, I can make an informed decision about the entire signal chain. Once I choose the bandwidth, the theorem tells me the SNR so I can assign a noise budget to each of the components. If we assume that the noise is Gaussian, we can calculate total noise level as the root sum of squares of the noise levels of the individual components (don't forget to multiply by the gain). I can look at an amplifier IC's spec sheet and immediately say, "that's too noisy" or "that's overdesigned, I think I can get something cheaper". And thanks to theorems we got from the field of real analysis and statistics, we know that the sum of Gaussians is itself Gaussian. So rather than sticking two components together and measuring the noise, or running a computer simulation, I can simply square, sum, and square root. Each of these theorems reduces the amount of work necessary -- whether by pen and paper or by computer -- by an enormous factor. But if you can describe in similar detail how the computer program would work, I'll acknowledge your greatness.
  - marshallp 14y ago
    That's just a few parameters that you avoided having to tune, a few milliseconds of computer time. I'm not great, just questioning basic assumptions that have been handed down from a time before computers were around.
    - klodolph 14y ago
      You keep on asserting that the task -- without domain knowledge of Shannon's theorem -- is solvable by computer. Can you describe how such a computer program would work? I'm unconvinced that the computer program would get a reasonable result before you run out of money paying for it.
      - marshallp 14y ago
        The Shannon theorem is basically voided by compressive sensing. But all of this (shannon+compressive) was a waste of practical people's time anyway. It's justification for pencil pushers who don't want to do real work.
        karategeek6 14y ago
        http://www.youtube.com/watch?v=1orMXD_Ijbs&feature=related http://www.youtube.com/watch?v=1orMXD_Ijbs&feature=relat...
    - darkarmani 14y ago
      > That's just a few parameters that you avoided having to tune, a few milliseconds of computer time. Really? What happens when you need to do a similar calculation across hundreds of millions of data points?
- geoka9 14y ago
  How about solving differential equations numerically. Such programs are used all over the place in mathematical modeling, with applications ranging from economics to electronics. And you can't just "write a computer program that tries different parameters". You have to prove that your numerical method solves a certain class of equations first, otherwise your rocket will fly sideways, if at all.
  - marshallp 14y ago
    The intelligent way to do that nowadays is to use automatic differentiation followed by optimization "plugins". And that has little to with proving theorems unless you consider all computer programs as proofs and all computer programmers as mathematicians.
    - geoka9 14y ago
      I'm not sure what automatic differentiation has to do with solving diff. equations but... I assume that all those automatic methods you mention are passed down from above in some sort of holy scriptures that we're supposed to blindly believe and use? Or maybe some "pencil pushing" mathematician came up with them first and _proved_ that they actually work?
      - marshallp 14y ago
        If you're solving DE's by hand you were probably just in a class taught by members of the Mathematician-Teaching Complex (allusion to Military-Industrial Complex).

Evbn 14y ago

You might be interested in the up and coming fields of 3D video games, flight simulators, CG movies, machine learning, supply logistics, autonomous navivations, colonization of Mars, and your personal favorite algorithmic trading, all brought to you by "theorems" of linear algebra.

marshallp 14y ago
None of those require theorems, they require computers.
- gizmo686 14y ago
  Great news, I finally wrote a sorting algorithm that worked for 10/10 of my test cases. Now, I can just plug that number into my unproven statisticle test, and found out how likely it is that my algorithm will work for all inputs. It does not seem to run extra slow for any input, so it probably won't run slowly on any input in actual use. Besides, even if it did I would have no way of proving what types of inputs it failed on, or if another algorithm would do better.
  - marshallp 14y ago
    http://ertos.nicta.com.au/research/l4.verified/proof.pml http://ertos.nicta.com.au/research/l4.verified/proof.pml Keeping the above in mind, does it actually justify the billions of man hours spent on mathematics.
- saraid216 14y ago
  The notion of a computer was a theorem. http://en.wikipedia.org/wiki/Turing_completeness http://en.wikipedia.org/wiki/Turing_completeness
  - marshallp 14y ago
    The computer industry wasn't built on Turing completeness. It's an evolution of practical technology starting with the invention of textile machinery (but you can also kind of argue it started with abacuses or even lines drawn in sand).

saurabh 14y ago

Proving theorems has theoretical applications. And the knowledge gained by doing so may have practical applications.

plinkplonk 14y ago

Exhibit 1: you say "Are there practical applications for proving theorems?" Exhibit 2: In your profile, you describe yourself as "Machine Learning Expert" Hmm.

marshallp 14y ago
Yeah, there's pencil pushing frauds (mathemagicians) in machine learning too.
- mreid 14y ago
  I see that you use VW for machine learning. You should ask the lead developer (John Langford) what he thinks of the efficacy of mathematics for machine learning given most of the algorithms it uses were derived from theoretical considerations (e.g., SGD, LDA, reductions, etc.) Would you describe him as a "pencil pushing fraud" too?
  - marshallp 14y ago
    Yes, he's a pencil pushing fraud for the most part (he might even admit it in private). I don't know how old he is but assuming he's been professional for 10 years, his big contribution is the few hundred/thousand lines of VW (he's probably done other work, but let's assume this is a significant fraction). Where did the rest of his time go? If he just decided to bang VW out a decade ago he'd be at it's current state within a month of starting. VW is only useful because it's fast and it works (and that's not due to any theory). It's theoretical considerations are useful only for essentially drawing that 1 month out to years/decades.
    - mreid 14y ago
      I'll ask him whether he considers himself mostly a pencil pushing fraud when I see him in December. I'll also see what he thinks of the claim that VW's usefulness is "not due to any theory". I'll think you'll be surprised given he's written a blog post on this topic titled "Use of Learning Theory" http://hunch.net/?p=496 http://hunch.net/?p=496 at his blog which, by the way, is called "Machine Learning (Theory)". It's easy to dismiss what you don't understand but you should consider the possibility that it is significantly more difficult develop algorithms like those in VW and "bang out" implementations of them that are fast and correct.

ColinWright 14y ago

I'm curious - you seem to be saying that theorems are useless, and instead, all we ever need to do is write programs to twiddle the numbers and work things out that way. So what would you need me to do to show that proving theorems is important? What would convince you? What is your criterion for a successful response?

marshallp 14y ago
What is the criterion you would give an astrologer? I'm not equating them with astrology, but simply pointing out the countless billions wasted on mathematics that narrows to the rarefied "breed" of pure mathematician earning a salary is as much of a waste as if billions were spent on buggy whip boys. Some things are just meant to fade into museums and history books.
- mreid 14y ago
  There is no argument that fundamental research (including, but not limited to pure mathematics) is a high-risk investment with a small chance of a large pay-off. But, like most good, high-risk investments the potential pay-offs can be massive and, importantly, not always well-understood in advance. Would we have GPS without relativity which in turn depends on non-Euclidean geometry, initially considered a curiosity? What about public key encryption, built upon number theory, proudly described as "useless" by the pure mathematician G.W. Hardy? There are so many examples like these. Be careful of committing the fallacy in assuming that because a clear line of ideas can be traced back from the present day that finding that line was as easy as recounting it. Out of interest, what is your position of the spending on sport, the arts, and other cultural endeavours?
  - marshallp 14y ago
    People are tired of me criticizing maths on here so I'll stop with it. My opinion on sports, arts etc. is the same. Publicly funded stuff is basically for the elite anyway, it's their way of cleverly siphoning tax-payer money (for there boring outdated interests which they partake in to show the illusion of sophistication). The masses pay to see their interests (and usually heavily taxed for it to boot).

regularfry 14y ago

We can't have provably correct software without theorem proofs. Provably correct software is a good thing.

thedigitalengel 14y ago

Would you feel secure about using a cryptographic system without a proof?

Cogito 14y ago

'Proving Theorems' is a grand sounding statement, but the reality need not be so glamorous! A Theorem as a thing is an encapsulation of a granule of knowledge or, even less precisely, something learnt which is known to be true[1]. To prove a Theorem is to show that the knowledge it encapsulates is correct. Why is this good? Most theory I have read[2] on AI, machine learning, and knowledge deals in depth with the concept of symbols and symbol manipulation. Some would claim (correctly!) that computers are in essence simply symbol manipulation machines. The thing is, these symbols are really just ways of encapsulating a piece of information. Often, symbols are described as being 'made-up' of other symbols; symbols are used to describe other symbols. As a simple and obvious example: - bits (low level 'axiomatic' symbols) are organised into groups to create bytes (still low level, not much meaning here yet) - bytes are associated with letters (in an isomorphic relation which imparts meaning[3]) - letters are organised into groups to form words (a significant amount of meaning has now appeared) - words are strung together in sentences - sentences are woven into paragraphs/chapters/themes/poems/stories/epics If I was to claim that a poem or story has no meaning simply because I can craft it from simple bits I would be missing something very important about symbol manipulation. When I take a collection of ideas, snippets of information and learning, and am able to label them with a name I can transcend my current level of understanding and deal with ideas which are invisible on the lower level. For a programmer, this hierarchy of symbols presents itself as a hierarchy of low, medium and high level languages. Writing a python program in assembly would be absurd!(although perhaps appropriate in some cases) Theorems (and Axioms) are the symbols of mathematics, and proving Theorems is symbolic manipulation in one of its purest forms. In fact, proving Theorems is the main way in which new 'meaningful'[4] symbols are created. So why is proving Theorems useful? In short, because it is how new knowledge is created! (in this context, mathematical knowledge) Is mathematical knowledge useful? I think anyone living in this modern world of ours (and I think that phrase applies to most people in most of humanity's history) can see that at least some mathematics is useful. Many have here argued about the different merits of developing mathematical knowledge (ie proving Theorems) before an application is well known, so I won't labour that point. Instead, I think I'll direct the interested reader to G.H. Hardy's 'A Mathematician's Apology'[5] for a great essay on the many merits a joy of mathematics can bring the suitably inclined soul. If knowledge is a good thing, and proving Theorems increases knowledge, than proving Theorems is a good thing. To say it is better than other ways of spending our efforts is hard, but I think we can definitely agree that it is useful. [1] My own definition! [2] Which is tragically less than I would like [3] Douglas Hofstadter in Gödel, Escher, Bach explains this idea so much better than I can - see https://en.wikipedia.org/wiki/Gödel,_Escher,_Bach https://en.wikipedia.org/wiki/Gödel,_Escher,_Bach [4] An idea again borrowed from Hofstadter. We can string any string of words together that we want, doesn't mean that they mean anything to us. Formal system such as mathematics give us a way to combine symbols to give us new meaningful symbols. My claim that it is the main way they are created is founded on wild speculation and heavily biased historical observation. [5] http://www.math.ualberta.ca/~mss/misc/A%20Mathematicians%20Apology.pdf http://www.math.ualberta.ca/~mss/misc/A%20Mathematicians%20A...