6 ms·

I actually somewhat sympathize with your view. But I think you overstate the problem: if someone discovers something with Mathematica, they can then formalize i

I actually somewhat sympathize with your view. But I think you overstate the problem: if someone discovers something with Mathematica, they can then formalize it with an open proof assistant like Coq before they publish, and modern journals in fact encourage this sort of thing. Really, it's not a zero-sum-game between open-source and commercial tools.

jordigh 13y ago
"Open source" and "commercial" are not antonyms, but people working on proprietary software think they are.
- Someone 13y ago
  Some people may think that, but I doubt that that applies here. Wolfram certainly knows that "proprietary" and "free" aren't antonyms. I do think there is a commercial side to this, too, however. This is a kind of a hook to catch future customers of the commercial package.
- comex 13y ago
  Only if you use an overly literal interpretation of "commercial" yet don't use the literal interpretation of "open source" (since it's also possible to make source code visible to the public without using a license that would be considered "open source").
  - jlgreco 13y ago
    You have just rediscovered the reason that some people talk about "free software", and some people talk about "open source". The sort of access to source code that is being expected here is really no more than the sort of access that you can get to Windows code. It really is not an unreasonable expectation.
    - comex 13y ago
      No - when most people use the term "open source", they mean something along the lines of the Open Source Definition (http://opensource.org/definition http://opensource.org/definition), rather than the literal meaning; this is independent from the distinctions between open source and free software, which are mostly about philosophy rather than the set of applicable licenses (http://www.gnu.org/philosophy/free-software-for-freedom.html http://www.gnu.org/philosophy/free-software-for-freedom.html) I suppose that you, however, do not, which makes what I was trying to say irrelevant.
- throwawaykf 13y ago
  And a lot of people using open source products think so too :-)
lutusp 13y ago
> Really, it's not a zero-sum-game between open-source and commercial tools. Yes, there are mathematical results that can be validated independently. But the problem is not so much pure mathematics as numerical results. In that arena, the method by which the results were acquired must be accessible in detail. And much of modern applied mathematics relies on numerical results. Imagine producing a result of some value and being unable to explain in detail how it was arrived at, because it emanated from a closed-source program. The four-color map problem I mentioned earlier was the first important case where this problem had to be dealt with, and it was resolved to everyone's satisfaction only because the full source was made available.
- taliesinb 13y ago
  You're jumping around a bit.. Did the four-color map problem use numerical results? I imagine it was just a pure combinatorial enumeration problem (I have not read the original paper, I may be wrong about that). If you're doing a finite element method to validate a bridge design, you're hardly publishing a paper based on the result (though of course you will do plenty of validation and then times everything by 2 for good measure!). What kinds of actual fields of mathematics are you thinking about, here? I know that error analysis is a deep and arcane subject, and personally I have no idea how well or badly we do in that department, but I'm struggling to think of where the details of how we get it wrong or right is crucial for the development of published academic mathematics. "Most" maths is totally abstract these days, categories and sheaves and topi and what not.
  - lutusp 13y ago
    > You're jumping around a bit. In that case, anyone who uses more than one example to make his point is jumping around. If allowed to prevail, this non-argument would cripple debate. > Did the four-color map problem use numerical results? Yes, emphatically so. There were a certain finite number of possible maps (1936 to be precise), and each of them had to be tested explicitly. The reason for the requirement for full disclosure was that the tested set needed to be examined to assure that nothing germane was excluded, nothing included on specious grounds, and the manner of testing had to be closely examined. None of this could be reduced to a simple equation, and none of it yielded to a formal, concise mathematical proof. > I imagine it was just a pure combinatorial enumeration problem (I have not read the original paper, I may be wrong about that). If that were true, there would have been no role for a computer program -- it would have been published as a pure and formal result, like Fermat's last theorem. No one would have cared about the role played by computers, because a formal and pure proof could be examined by anyone sufficiently versed in mathematics. > What kinds of actual fields of mathematics are you thinking about, here? Any field that would benefit from use of a computer. By recent count, that's nearly all mathematical fields for one reason or another, including areas we once might have thought would have no use for a computer. Computer mathematics has gotten to the point where computers, laboring independently, come up with new theorems that humans have overlooked. > I know that error analysis is a deep and arcane subject, and personally I have no idea how well or badly we do in that department, but I'm struggling to think of where the details of how we get it wrong or right is crucial for the development of published academic mathematics. Most struggle with that, and part of the struggle is being able to see the detail of the algorithms used to arrive at a result. No detail, no trust, no science. > "Most" maths is totally abstract these days ... Not relevant. Relevant would be whether that abstract mathematics is or is not fully revealed in its details. For science, it must be. This article -- http://www.newscientist.com/article/dn7286-computer-generates-verifiable-mathematics-proof.html#.Uo8YZkpDsrI http://www.newscientist.com/article/dn7286-computer-generate... -- discusses the role of theorem-proving software like Coq, but includes a misleading statement by someone at Microsoft: "Microsoft hopes to develop a similar system for checking the logic used in computer programs, which could pre-empt some unforeseen bugs that cause programs to crash." I hope this is an error on the part of the journalist who wrote the article, because it implies that Turing's halting problem, and Gödel's incompleteness theorems, which lie behind it, are potentially soluble. They aren't. All the more reason for full disclosure.

jordigh 13y ago

"Open source" and "commercial" are not antonyms, but people working on proprietary software think they are.

Someone 13y ago
Some people may think that, but I doubt that that applies here. Wolfram certainly knows that "proprietary" and "free" aren't antonyms. I do think there is a commercial side to this, too, however. This is a kind of a hook to catch future customers of the commercial package.
comex 13y ago
Only if you use an overly literal interpretation of "commercial" yet don't use the literal interpretation of "open source" (since it's also possible to make source code visible to the public without using a license that would be considered "open source").
- jlgreco 13y ago
  You have just rediscovered the reason that some people talk about "free software", and some people talk about "open source". The sort of access to source code that is being expected here is really no more than the sort of access that you can get to Windows code. It really is not an unreasonable expectation.
  - comex 13y ago
    No - when most people use the term "open source", they mean something along the lines of the Open Source Definition (http://opensource.org/definition http://opensource.org/definition), rather than the literal meaning; this is independent from the distinctions between open source and free software, which are mostly about philosophy rather than the set of applicable licenses (http://www.gnu.org/philosophy/free-software-for-freedom.html http://www.gnu.org/philosophy/free-software-for-freedom.html) I suppose that you, however, do not, which makes what I was trying to say irrelevant.
throwawaykf 13y ago
And a lot of people using open source products think so too :-)

lutusp 13y ago

> Really, it's not a zero-sum-game between open-source and commercial tools. Yes, there are mathematical results that can be validated independently. But the problem is not so much pure mathematics as numerical results. In that arena, the method by which the results were acquired must be accessible in detail. And much of modern applied mathematics relies on numerical results. Imagine producing a result of some value and being unable to explain in detail how it was arrived at, because it emanated from a closed-source program. The four-color map problem I mentioned earlier was the first important case where this problem had to be dealt with, and it was resolved to everyone's satisfaction only because the full source was made available.

taliesinb 13y ago
You're jumping around a bit.. Did the four-color map problem use numerical results? I imagine it was just a pure combinatorial enumeration problem (I have not read the original paper, I may be wrong about that). If you're doing a finite element method to validate a bridge design, you're hardly publishing a paper based on the result (though of course you will do plenty of validation and then times everything by 2 for good measure!). What kinds of actual fields of mathematics are you thinking about, here? I know that error analysis is a deep and arcane subject, and personally I have no idea how well or badly we do in that department, but I'm struggling to think of where the details of how we get it wrong or right is crucial for the development of published academic mathematics. "Most" maths is totally abstract these days, categories and sheaves and topi and what not.
- lutusp 13y ago
  > You're jumping around a bit. In that case, anyone who uses more than one example to make his point is jumping around. If allowed to prevail, this non-argument would cripple debate. > Did the four-color map problem use numerical results? Yes, emphatically so. There were a certain finite number of possible maps (1936 to be precise), and each of them had to be tested explicitly. The reason for the requirement for full disclosure was that the tested set needed to be examined to assure that nothing germane was excluded, nothing included on specious grounds, and the manner of testing had to be closely examined. None of this could be reduced to a simple equation, and none of it yielded to a formal, concise mathematical proof. > I imagine it was just a pure combinatorial enumeration problem (I have not read the original paper, I may be wrong about that). If that were true, there would have been no role for a computer program -- it would have been published as a pure and formal result, like Fermat's last theorem. No one would have cared about the role played by computers, because a formal and pure proof could be examined by anyone sufficiently versed in mathematics. > What kinds of actual fields of mathematics are you thinking about, here? Any field that would benefit from use of a computer. By recent count, that's nearly all mathematical fields for one reason or another, including areas we once might have thought would have no use for a computer. Computer mathematics has gotten to the point where computers, laboring independently, come up with new theorems that humans have overlooked. > I know that error analysis is a deep and arcane subject, and personally I have no idea how well or badly we do in that department, but I'm struggling to think of where the details of how we get it wrong or right is crucial for the development of published academic mathematics. Most struggle with that, and part of the struggle is being able to see the detail of the algorithms used to arrive at a result. No detail, no trust, no science. > "Most" maths is totally abstract these days ... Not relevant. Relevant would be whether that abstract mathematics is or is not fully revealed in its details. For science, it must be. This article -- http://www.newscientist.com/article/dn7286-computer-generates-verifiable-mathematics-proof.html#.Uo8YZkpDsrI http://www.newscientist.com/article/dn7286-computer-generate... -- discusses the role of theorem-proving software like Coq, but includes a misleading statement by someone at Microsoft: "Microsoft hopes to develop a similar system for checking the logic used in computer programs, which could pre-empt some unforeseen bugs that cause programs to crash." I hope this is an error on the part of the journalist who wrote the article, because it implies that Turing's halting problem, and Gödel's incompleteness theorems, which lie behind it, are potentially soluble. They aren't. All the more reason for full disclosure.