Open Source Math 352
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.'""
It's all... (Score:2, Insightful)
Python is part of the answer (Score:5, Insightful)
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 [cryptome.org] the compiler. And if you hand compile the compiler, how can you trust the CPU [wikipedia.org]? 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
speaking of proprietary (Score:3, Insightful)
Should journals reject such proofs? (Score:3, Insightful)
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.
Not Proven (Score:4, Insightful)
TWW
Re:Welcome to the world of modern research ... (Score:3, Insightful)
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!
PDF rant. (Score:5, Insightful)
Really, what is wrong with PDFs and why should they require a warning?
By the way, all scientific papers are disseminated by PDF.
Open Formats (Score:3, Insightful)
Re:Python is part of the answer (Score:4, Insightful)
No mistakes. After all, the Ultimate Answer really is 42. My program proves it!
#define MYANSWER "42"
int main()
{
printf("The result is: %s.", MYANSWER);
}
No, you CAN'T have the source code... but look, my program proves it! LOOK AT THE PROGRAM!
Not necessarily bad in all cases... (Score:5, Insightful)
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.
Re:Python is part of the answer (Score:4, Insightful)
I am a mathematician. Your referees might ask to inspect the source code. This is akin to a biologist being asked to produce her raw data. But it's pointless anyway. Because...
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.
The AMS isn't worried about the correctness of these "proofs." They aren't proofs. It is logically possible for one of these programs to return the wrong answer, even if the program is correctly implemented. Ergo, it is not a proof.
Computing, in mathematics, is a source of fresh problems and a vehicle to explore and gain insight about mathematical structures. The AMS is far more concerned about good exploratory algorithms getting swept up by Wolfram Inc., and Mathworks, and the like, and never being seen by mathematicians again.
Regarding which language is approriate for mathematics, the answer is whichever clearly expresses the idea you're trying to write. Lexical scoping is familiar to us. I know I prefer it, since it lessens my cognitive load. I prefer dynamically typed languages. I need the ability to construct anonymous functions efficiently. And I would prefer automatic memoization. Development time is always an issue. Most languages don't come with extensive mathematical algorithm libraries. So you'll either have to write them yourself (time consuming; boring, unless you're into that stuff) or find some. I've used Perl, Ruby, Scheme, and C.
What about hardware? (Score:4, Insightful)
Re:Openness is Fundamental to Mathematics (Score:4, Insightful)
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.
Re:Not necessarily bad in all cases... (Score:3, Insightful)
Perhaps I'm being too pessimistic, but shouldn't the source code have to be provided alongside the pseudocode? If the pseudocode is 100% spot-on, then there would really be no need for the computer-assisted proof in the first place --- you will have provided a proof in the form of verifiable instructions. But the FCT was proved by some amount of brute-force, IIRC. Who is to say that the coder who translated from pseudocode to source code didn't mess something up? I mean, if my pseudocode reads
INCREMENT current value by ONE...
OUTPUT result of long computations
and my source code is entered as
value += value++;...
printf("%d",result);
then even if the pseudocode is verified, the program may still be producing an erroneous result. In other words, you're assuming that IF the pseudocode is correct THEN the program itself is also correct, which may not be the case.
bad analysis, bad results (Score:3, Insightful)
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.
Re:Python is part of the answer (Score:3, Insightful)
I disagree, it is certainly possible to prove to a reasonable certainty what a black box is doing. It may be easier, or more though to prove looking into the box.
As you say, for all practicality no one is going to be able to confirm the entire software stack, by looking at the code for any proof. unless your running the final step on a basic stamp.
But if you re-run the program multiple times with the same result, and you run multiple iterations of very similar problems that you know the results of, and they all agree, you can build a reasonable proof.
Re:But the proof steps are known, right? (Score:2, Insightful)
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.
Re:Python is part of the answer (Score:3, Insightful)
Math is "Free", MY LILY-WHITE ASS. (Score:5, Insightful)
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
Re:Not Proven (Score:2, Insightful)
If a "proof" is published with some steps or information excluded then it's not a proof, it's just an assertion.
I don't agree with this, because by that argument nothing is a proof. Every proof has steps left out, unless you reduce everything to axioms, which is plainly silly.
A proof is a proof if and only if it is enough to convince the person that is reading it. Of course this makes a proof a function of both the reader and the writer, but this is the only way it can be. If the person reading your proof is not convinced by any of the steps and wishes clarification, then you must be able to provide it. If however everbody is happy that the missing steps are okay, then the proof is good.
Re:Math is "Free", MY LILY-WHITE ASS. (Score:5, Insightful)
> I'm not going to disagree with the "laid open" part, but the "free of charge" nonsense
> is just typical marxist university professor hypocrisy.
Taken out of context the quote might not make sense to you. The full quote from Neubuser is:
When Neubuser says that mathematics is "free of charge" he means that
one can use theorems one reads without having to pay to use those theorems.
He is of course not at all claiming that publishers do not charge for
books and papers that contain mathematics. Put simply, if I want to use
the "FactorN" function in Mathematica, I have to pay for the privilege
every time I use it. If I want to use the theorem that every integer
factors uniquely as a product of primes, then I never have to pay, even if
I am using that theorem in a published proof.
-- William
Re:I'm not the hypocrite here. (Score:5, Insightful)
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.
Re:not really true (Score:3, Insightful)
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.
OpenAxiom (Score:3, Insightful)
another useful package: Mathomatic (Score:3, Insightful)
Mathomatic [mathomatic.org] 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 [mathomatic.org]
Many thanks for writing it, George Gesslein II [mathomatic.org].