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.'""
Thanks for the article, now some crazed company is going to try to copyright math.
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"
This problem goes beyond mathematics, and reaches into many of the sciences. Mathematicians and scientists often place undue trust in complex software systems, simply as a matter of getting the work done faster rather than producing higher quality research. Sometimes it is a case of handling large volumes of data, in which case human intelligence and discretion is a bottleneck. Sometimes it is a matter of finding numerical solutions where analytic ones are difficult (if not impossible) to find at present. And, in the case of mathematics, I'm guessing that they are using it as a shortcut for those difficult analytic solutions.
Then again, I must really ask if the mathematician in question understands what they are doing if they are using software as a shortcut for difficult analytic solutions. After all, if they don't understand the algorithms well enough to do the work themselves, who is going to say that they understand the limitations of the rules that they are asking the computer to apply.
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.
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.
There is one special feature of Ruby, that I miss in every single programming language I used since: iterator methods. Any time I want to iterate over elements of an array or hash I just do: That's it, instant "anonymous function" given as a parameter in estetically pleasing syntax. In fact, "for" loop in Ruby is just obfuscated way of calling method #each on an object. But the madness doesn't stop here: It's a pity that so many people disregard Ruby as a "platform for Rails". It is a feature complete countepart to Python, and as my company high volume systems can attest, can handle anything other languages can handle.
Robert
Bastard Operator From 193.219.28.162
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.
We may also mention Coq, a proof assistant wich is available under LGPL and runs on OCaml (which in turn is also open sourced and available on Linux).
/. (article about machine assisted proofs).
This is a tool that can help mathematician prove their theorems.
It was notably being used in the proof of the four color theorem, as mentioned on
"Sufficiently advanced satire is indistinguishable from reality." - [Tips: 1DrYakQDKCQ6y52z6QbnkxHXAocMZJE61o ]
Look around you. Look around you!
That's how I learned maths in high school.
I am defenseless. Use your button. Mod me down with all of your hatred.
http://metamath.org/ has been around for 15 years or so; it has a very nice text-based proof expression, a huge library of existing proofs and a graphical visualization tool
The AMS did not write that article. I wrote the article as an opinion piece and the AMS published it. They do not necessarily agree with the points made in the article.
... and (using [Mathematica|Magma|...]) we deduce that [...].
..." this gets very very frustrating, since one just hits a brick wall. And, in practice, reimplementing -- with enough optimization to make it useful for research -- just one or two key functions from Mathematica or Magma, can take literally years of work (in fact, that's exactly what I've been doing the last few years with http://sagemath.org/). And sometimes exactly that is necessary to go beyond what has already been done, i.e., to do research.
By the way, the article is not about formal automated proofs. It is about what is now standard procedure in mathematical research, namely proofs that look like this:
[Formal mathematical argument]
It's incredibly common right now when reading published mathematical papers to see random citations to using closed source software to do key steps of calculations. Usually even the code used to get the closed source program to yield the result isn't given.
The way many mathematicians read proofs is that they often basically skim the argument to get a general idea of what it is about. Then they decide they want to prove something similar or related, and they "dive" into the most refined details of some key part of the argument. When a part of the argument is "... using Mathematica we deduce
-- William Stein
I'm too lazy to see if that's the IEEE 754 result or not (but I suspect it is). But three things in Python's defense:
Dewey, what part of this looks like authorities should be involved?
Sage( http://www.sagemath.org/ ) is currently the most full=featured open-source computer algebra system. It is being developed by the two authors of the AMS opinion piece (and many others including myself). Our goal is to provide a free, viable, open-source alternative to Mathematica, Maple, MATLAB, and Magma. Some nice features of Sage include:
* It uses Python as its programming language so that you can use any existing Python modules with your Sage programs.
* Sage also includes Cython ( http://www.cython.org/ ) which is based on Pyrex and allows one to easily compile Python code down to C for speed.
* Sage's notebook interface with also interface with pretty much every existing computer algebra system, open-source or not.
* Sage includes Maxima, GAP, Scipy, Numpy, and many other open source math packages.
* A very active developer community. If there is something that you need Sage to do, chances are that there will be a number of developers willing to help you out.
For some screenshots, see http://www.sagemath.org/screen_shots/ .
One of the things that Sage needs most now is more users. So, if you have an interest in open source math software, definitely check out Sage.
Python calculated exactly what its documentation says it will do: ((1 minus the IEEE-754 double closest to 1/100) rounded to the nearest IEEE-754 double). It's not Python's fault if you don't know the basics of floating-point arithmetic. Mathematicians who use or write numerical software do.
I recommend reading What Every Computer Scientist Should Know About Floating-Point Arithmetic.
1. The only reason you would need a "PDF warning" is that you use an operating system with poor support for the format (i.e. Windows). Switching to a real OS, among other benefits, will make reading math papers (which are almost always in PDF format) a pleasure.
2. PDF is an open standard, which has been implemented by many different parties: Adobe and Apple have closed-source implementations; freedesktop.org's poppler and cairo libraries are Free software.
3. The fontface chosen by AMS is orthogonal to the content of the paper - you can easily copy-paste the text and use Computer Modern, Dejavu, Liberation or any other open-source font of your choice. Why would a proprietary font embedded in a PDF file bother you any more than the proprietary fontface of a book?
4. First of all, PDF is editable. And second, why would you want to edit this particular document? Remember, it's copyrighted by AMS - if you can't prove fair use, you do not have the right to distribute a modified version.
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
These guys are advocating setting up a peer-review process for open source software in machine learning. The idea is that this would encourage researchers to spend more time on the software component of the publication, and perhaps produce something that others can use aswell.
The article is in the Journal of Machine Learning Research.
Would these be the same kind of good-for-nothing, lazy, worthless asses who brought us Special Relativity while working in a lowly position in the Patent Office in Bern? You know, the kind who got together with friends to peruse and discuss the latest freely available scientific texts, the same texts that led him to revolutionise science more than anyone since Newton?
The books in the Princeton Library are free, thanks to the generousity of far-seeing individuals who realised that their money was better spent on a library than a new yacht. They, at least, saw the benefit of sharing knowledge with everyone, regardless of their means. I can only hope that, somewhere in that misanthropic little husk you call a heart, you will some day find room for a similar spirit of openness and sharing.
Crumb's Corollary: Never bring a knife to a bun fight.
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
It's called Math You Can't Use - by Ben Klemens. Makes a bunch of great points in favor of open source, too.
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.