Slashdot Mirror
Open Source Math
An anonymous reader writes "The American Mathematical society has an opinion piece about open source software vs propietary software used in mathematics. From the article : "Increasingly, proprietary software and the algorithms used are an essential part of mathematical proofs. To quote J. Neubüser, 'with this situation two of the most basic rules of conduct in mathematics are violated: In mathematics information is passed on free of charge and everything is laid open for checking.'""
about the money.
I am no a mathematician but surely if you're going to submit a computer aided proof you must submit a full copy of the program. The are all manor of subtle mistakes that can be made in a program that could cause serious problems with a proof.
Suppose you inspect the source and find it to be faultless, how can you trust the compiler. And if you hand compile the compiler, how can you trust the CPU? Surely it's turtles all the way down.
In many ways, establishing the correctness of a computer-aided proof is very much like security engineering. You want to verify that the whole software stack is operating correctly before you can trust the result. Having the source-code is a pre-requisite to this exercise.
Changing to topic slightly, I was particularly heartened to see that the open-source mathematics framework being developed one of the authors of the article involves the use of Python.
My immediate thought when seeing the title to the article was "Python is the answer." When some problem or algorithm intrigues me the first thing that happens is that I reach for the Python interpreter.
Python seems to deftly marry precision with looseness. When code is laid out in Python I find it is easier to see what it's trying to do than other languages. It's aesthetic qualities aside, it supports a number of features out of the box which I imagine would be ideal of mathematicians. To list a few, it's treating of lists and tuples as first class objects, support for large integers, complex numbers, it's ability to integrate with C for high-performance work.
I often think of Python as "basic done right" and it's ideal for mathematicians (or anybody) who don't want to think about programming but the problem at hand.
Simon
The article (which is actually a PDF, thanks for the warning) uses proprietary fonts (LucidaBright). While it was typeset with TeX (open), only the PDF (closed and uneditable) is provided.
Do you even lift?
These aren't the 'roids you're looking for.
Algorithms cannot be protected by copyright, only by patents and trade secrets. If the algorithm is a trade secret, it has no place in a mathematical proof because it cannot be shared with the world and verified or refuted by anyone interested in doing so.
If the algorithm is part of a patented device or piece of software, its use in a mathematical proof is not subject to the patent on the grounds that pure math cannot be patented.
If journals and academic societies refused to publish proofs based on trade secrets and insisted on a covenant not to enforce the patent against researchers doing purely mathematical research or those who publish the research, the problem would mostly go away. An alternative to the covenant is congressional action or a court ruling that says with absolute clarity that mathematical research is exempt from math-related patents directly related to the research.
--
Personally, I'm against all such patents but I'm not holding out hope that Congress or the Courts will agree with me.
Knowledge is how to play a game, intelligence is how to win, wisdom is knowing what game to play.
TWW
"Encyclopedia" is to "Wikipedia" what "Library" is to "Some people at a bus stop"
I thought the same thing... shouldn't mathematic proofs be independent of outside influence, shouldn't they stand on their own and make as few assumptions as possible. I figured that a proof, properly done, would be a large step by step solution to the problem.
Then I realized that many proofs aren't concerned with single-input single-output situations, but instead may require thousands of iterations based upon large sets of inputs. You can't do that by hand.
I am certain, that because computers/software are being used we will eventually find an accepted proof that is scrapped because it exploited (inadvertently) a bug/limitation of the software used to test it. Unfortunately there is nothing to be done!
Sometimes the best solution is to stop wasting time looking for an easy solution.
Why does this keep coming up on ./? What is wrong with PDF? It's undeitable, sure, that's kind of the point. However, the spec is accessible, and there are plenty of open readers, e.g. xpdf and ghostscript.
Really, what is wrong with PDFs and why should they require a warning?
By the way, all scientific papers are disseminated by PDF.
SJW n. One who posts facts.
Proprietary math software is not a problem as long as the end result can be exported into a fully documented format and can be then verified by open software, including human mathematicians.
In other cases, like the proof of the four color theorem, it seems like the source code is important to see, but not essential. Pseudocode should suffice. Providing pseudocode is akin to saying things like "Simplifying expression (1) yields..."; we don't have to provide EVERY step, but with pseudocode you have enough to determine whether the algorithm itself will work. Checking the source code beyond that is akin to checking someone's algebra.
Just because we don't know how the program arrived at the steps it did doesn't mean that we shouldn't use it; we can usually check the steps. After all, the human brain has been a closed-source proof machine for thousands of years, and no one has complained about that :) Just require pseudocode in computer aided proofs, and it should be sufficient.
I would think that hardware errors would be an even worse problem, like the old Pentium bug, since they are so insidious.
Well, don't get your panties in a big bunch over this. Humans make mistakes in proofs all the time, many of which are not caught before publication (and many not even for some time afterward).
Also, although it's not in the field of theorem-proving, the mathematical package I use the most -- MATLAB -- is a million times better than the open source equivalent, Octave. I'm not going to use Octave simply because I can inspect the code, because who does that? An error in a software proof would be pretty obvious if it were checked with another independently written piece of software. With MATLAB, I can write my own alternative algorithm using C if I need to, though with significantly more effort and annoyance.
Furthermore, mathematicians are smart people who are fully aware of the implications of their assumptions, probably moreso than any other group of people I have encountered. Reading the set of comments accompanying this article, saying what mathematicians should and should not consider a proof, is like watching monkeys trying to use a can opener.
Toronto-area transit rider? Rate your ride.
A recall a few recent incidents in which papers had to be retracted because the machine did not do what the researchers thought it did. I have personal experience in which the spectroscopy generated by the computer did not reflect reality. If the researcher does not know how to use a tool, then he or she does not know when that tool is being misused.
I am not sure something like mathematica is the issue. Wolfram seems to use standard standard well known algorithm. Almost every academic institution has a license, so, given the data, any number of people can rerun the analysis. Likewise the algorithms can be tested with simpler data sets to understand how they work and breakdown. I would be more worried about homegrown software.
"She's a scientist and a lesbian. She's not going to let it slide." Orphan Black
Suppose the only known way to prove something is to check all cases. Suppose the cases number about 1.000.000. It would take any human practically an eternity to check them all. Suppose checking each case is somewhat trivial, even though each case takes some considerable time and the results of each case is not generalizable to the other ones (so that we absolutlely HAVE to check the all). The mathematician working on the problem creates an algorithm for this work. It can be proven that the algorithm works. But the algorithm IS the proof. If the theorem is true, running the program produces YES or TRUE or whatever and if it's false the algorithm produces NO or FALSE or something similar.
If we don't know that the algorithm works (it is proven to do so) and that the software also works (THAT is furthermore proven to do so) we have no way of knowing whether that YES or NO our program produced actually proves the theorem. Now assume that the program found a counterexample somewhere between case #50.000 and case #55.000. What if it was a precision error? If we don't have access to whatever it was that could have produced such an error - if we don't have ALL the source and ALL other information about the software, the results are useless.
I'm not going to disagree with the "laid open" part, but the "free of charge" nonsense is just typical marxist university professor hypocrisy.
Let's price some math texts:
Or try a few titles which might be a little more familiar to Slashdotters:
Princeton, which has the finest mathematics department in the world [or at least had the finest mathematics department in the world, before Harold Shapiro & Shirley Tilghman decided they wanted to turn the
The issue is not whether software companies should make their source code open - the real issue is should mathematicians accept proprietary applications as proof of theorums?
As pointed out in the editorial, software developers make mistakes, and this is true regardless of whether that developer is a proprietary software vendor, or a free/open source software project. There is one key difference however, the validity of any given proof can be determined independently when using free/open source code by the very nature of the product (availability of source code). There is no validation for proprietary software beyond the assurances of the company involved.
When mathematic theory becomes applied mathematics (such as the creation of buildings, bridges, aircraft, or thermonuclear devices), which proof would you prefer to hang your life upon - Microsoft's guarantee, or independent verification and peer review? This becomes ever more critical as we create more complex systems that can not be easily verified by hand, yet rushed into applied use by the expediency/efficiencies they deem to provide.
Lodragan Draoidh
The more you explain it, the more I don't understand it. - Mark Twain
Luckily for you, you haven't the foggiest idea how mathematics is developed. As it happens, I am a trained mathematician, and I work in finance, so I think I'm relatively qualified to comment. Your naive analysis makes a great deal of sense when you're dealing with procedures that are simple enough for a few smart people to come up with, but modern mathematics has become so complex that we only advance by standing on each others shoulders.
At my firm we use a lot of "proprietary mathematics", but guess what: none of it is stuff that wasn't discovered by some academic, we just combine their results in innovative ways. We depend completely — and it's not just us, it's everyone in the industry — on the results of academics.
Firms like Renaissance hire a bunch of PhDs who then apply their years of research in academia to generate the returns they do. Derivatives pricing in particular is so complex that it's not that the math isn't freely available for anyone to peruse, it's that it takes years of study to properly understand how it even works. So when a firm hires one of these guys, they aren't hiring them hoping that they'll come up with the next Black-Scholes-Merton pricing theory on company time. They're hoping that they understand the theory that already exists well enough to be able to apply it to real-world data and tweak it as necessary. That's what all those proprietary processes really are: not new, exciting theory, but old theory, properly combined and tested and written up into algorithmic trading or security selection algorithms.
Now, cryptography is not my thing, that's not the field I studied or what I have an interest in, but it may be that the NSA has a bunch of tech that no one else has. However, the NSA is not a private firm, and they'll be funded no matter what happens, so they can afford to employ thousands of brilliant cryptography researchers (in the same way a university does) and sit on the results. A private company can't do that. You can point to them as an example of how "it makes sense to keep results closed" if you want, but understand: they are the exception, not the rule. No one else works the way they do.
Universities, many of the best of which are private, depend on their professors publishing new and innovative stuff nearly non-stop. It's not altruistic; they make their money on tuition and they can justify charging 40k a year for an education only if they employ the best and the brightest. The measure of the best and the brightest is in their scholarly output. It's no coincidence that Harvard, Princeton, Stanford, MIT, and Yale have so many Nobel Prize and Fields Medal winners in their employ. Reputation is what makes or breaks a school; without it, they have no income, because the best students want to study at a university with pedigree.
So while your (cynical) view of the world may "feel" right if you don't know what you're talking about, thankfully for all of us, open mathematical and scientific development will always trump private proprietary systems. That may not be true of software, I don't know. But when it comes to research, academia wins.
On the subject of open source math, Axiom is an interesting 30 years-and-running project started (I believe) at IBM research that recently became open source. A new branch of the project started recently: http://www.open-axiom.org/ and has several people actively working on it. It differs perhaps most significantly from Maple and Mathematica in its use of strong static type checking. This allows its library creation language to be compiled into C, which gets compiled and loaded back into the interactive top-level. Altogether, a very neat system and a gigantic resource.
Mathomatic is a quick and handy package to use for your more everyday math problems. It celebrates 20 years since its first release this year and is still updated with its latest release, version 12.8.0, just three days ago.
For programmers, its 'code' command converts your math problem to source code in your choice of several programming languages.
For more info see http://www.mathomatic.org/math/adv.html
Many thanks for writing it, George Gesslein II.
Trusted Computing FAQ | Free Dawit Isaak!