×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

Open Source Math

CmdrTaco posted more than 6 years ago | from the wouldn't-it-be-nice dept.

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.'""

cancel ×
This is a preview of your comment

No Comment Title Entered

Anonymous Coward 1 minute ago

No Comment Entered

352 comments

Lol (5, Funny)

Matt867 (1184557) | more than 6 years ago | (#21398025)

Thanks for the article, now some crazed company is going to try to copyright math.

Re:Lol (1)

Roager (1188827) | more than 6 years ago | (#21398077)

10 bucks on Microsoft!

Those fucking porpriartaryers can learn from riaa (-1, Troll)

Anonymous Coward | more than 6 years ago | (#21398295)

That data wants to be free including binaryies. It obivous to me and I am a expert all around this feilds

Re:Those fucking porpriartaryers can learn from ri (0)

Anonymous Coward | more than 6 years ago | (#21398319)



How is it I can tell you're a Linux user?

Re:Lol (5, Funny)

Anonymous Coward | more than 6 years ago | (#21398181)

I am going to copyright 0 = 1.
Any software that contains i = i+1 must license my math.

Re:Lol (4, Funny)

Dunbal (464142) | more than 6 years ago | (#21398441)

Sorry, but I've already patented the systematic use and manipulation of abstract symbols representing real world quantities in order to derive relationships.

Re:Lol (4, Funny)

Plutonite (999141) | more than 6 years ago | (#21398957)

Sorry, but I've already patented the systematic use and manipulation of abstract symbols representing real world quantities in order to derive relationships.
And I've copyrighted proverbial hand-waving. Together, we hold the scientific community hostage!

Python is part of the answer (5, Insightful)

Ckwop (707653) | more than 6 years ago | (#21398061)

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

Re:Python is part of the answer (5, Interesting)

snarkh (118018) | more than 6 years ago | (#21398313)

I have seen from personal experience, how a compiler error (some sort of incorrect optimization) led to a subtle difference in the results of a simple classification task.

The insidious thing about that particular result was that it looked very similar to the correct. In fact the difference would not have been found if two people did not run different versions of code independently (and more or less coincidentally) arriving to slightly different error rates.

Re:Python is part of the answer (3, Informative)

jelle (14827) | more than 6 years ago | (#21398737)

From your description, it sound as if you found that the code returned different results at different optimization settings for the compiler, but did not pinpoint what instruction sequence exactly caused the difference.

Unless you were using an experimental compiler, that usually means a bug in the code, not a bug in the compiler. Run the code with valgrind, you'll probably find out-of-bound addressing, or uninitialized reads (the signs of the problem being in the code, not the compiler)... Or if you use threads, it can also be in your locks...

The reason for that is that such code bugs often result in different code execution at different compiler optimization settings.

Re:Python is part of the answer (5, Informative)

nwbvt (768631) | more than 6 years ago | (#21398323)

I used Python fairly extensively in my number theory course back in college, it did the job fairly well. Its support for large integers was especially important for that class. And the fact that it was very familiar to me (I was a double major in CS and math), it was very easy for me to crank out an algorithm in it. However, most of the book's examples were in Mathematica, which I ended up getting as well. It was a neat tool, but now that my student license has expired and I don't feel like spending a few grand on another license, everything I wrote in that is useless. However I can still pull out my old Python programs and see what it was I was doing.

Re:Python is part of the answer (1)

argiedot (1035754) | more than 6 years ago | (#21398789)

With a little work you may be able to do something with Octave, it's partly compatible with Mathematica code.

Re:Python is part of the answer (0)

noidentity (188756) | more than 6 years ago | (#21398365)

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.

I never thought about it until now, but I'd say that math "proofs" done by a computer shouldn't be given as solid a status as those done by humans. It's too easy for the computer to have a glaring bug. Maybe if more than one independently developed proof checking program were run over it (simulating more than one fallible human going over a proof), but how will that happen with patented, proprietary math programs?

Re:Python is part of the answer (3, Insightful)

Dunbal (464142) | more than 6 years ago | (#21398415)

The are all manor of subtle mistakes that can be made in a program that could cause serious problems with a proof.

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!

Re:Python is part of the answer (1)

otomo_1001 (22925) | more than 6 years ago | (#21398423)

Not to troll or anything, but every one of your reasons for using Python is why I use Ruby.

Some *very* recent others that make me like it:
* I can now use versions of Ruby that work with dtrace on Leopard and Solaris/Opensolaris (haven't tried FreeBSD yet).
* Ruby on Rails, yes despite the hype I like it. Though there are annoyances.
* I can also build Ruby (and Python) programs in osx without Coacoa/Objective C. Supported too, yay.
* (Not recent, but the reason I prefer Ruby to Python) Whitespace is optional, as are parentheses. I am looking at Perl right now.

Faults in 1.8 I don't like:
* longjmp/setjmp threading versus native threads in the interpreter. Sort of annoying to have to restrict certain things to the main "thread".
* Some functional aspects end up using insane amounts of memory if used.

In either case use what works for you, I use Ruby since it lets me work on the solution to the problem. If Python does that more power to you.

Back to the topic, shouldn't the math community be promoting a specific language then if they want to develop proofs with computers? Something like Haskell version XYZ should be used for all submitted proofs to verify everything? If we distrust every component of the computing stack we might as well throw them away as being useless. Although if we have a test framework/harness to verify proper operation we can leave most of this up to the interpreter/compiler.

I am sure I will get proven wrong on all this so be gentle!

Re:Python is part of the answer (1)

aldheorte (162967) | more than 6 years ago | (#21398531)

Second that on Ruby. I think Ruby is where the brain share and community is going, nothing against Python per se.

You have to be careful with Python and Ruby though. For example, I wrote a symbolic math interpreter for simplifying algebraic equations in Ruby. I then realized that I had reinvented LISP.

I do not actually program LISP, but in the end, LISP rules all as a programming language, especially when pure math is considered.

Re:Python is part of the answer (4, Insightful)

poopdeville (841677) | more than 6 years ago | (#21398495)

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.

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.

Re:Python is part of the answer (2, Interesting)

Anonymous Brave Guy (457657) | more than 6 years ago | (#21398605)

I fear you and/or the AMS are giving too much credit to the big names in mathematical software. Sure, they have some bright people and they do some useful research in their own right, but they're still only human. They make mistakes, their software has bugs, and they don't know lots of deep secrets that the rest of academia don't. In fact, the development practices at certain high profile mathematical software companies leave a lot to be desired; they tend to hire PhD types, who know a lot about mathematics but may or may not know jack about how to write good software. I rather doubt they're about to kidnap all the leading edge research and make it disappear from everyone not working for them.

Disclosure: I work for a mathematical software firm well known in its industry, and I've encountered some of the others in a professional context. I am speaking personally and not on behalf of anyone else here.

Re:Python is part of the answer (2, Interesting)

poopdeville (841677) | more than 6 years ago | (#21398881)

I fear you and/or the AMS are giving too much credit to the big names in mathematical software.

I can see why you might think that, but my point had little to do with commercial software houses. My main point was that computer-assisted "proofs" are not proofs in the mathematical sense. They're "results" that rest "scientifically" on the software and hardware and real world. It really doesn't matter whether I use my implementation of Newton's Method or Mathematica's. Neither should be trusted in a proof.

I forget who it was (Wiles maybe?), but a famous mathematician once described doing mathematical research as groping around a dark cave, trying to find an exit. A computer program is like a flashlight. Not an exit, but a helpful tool for finding it.

Re:Python is part of the answer (1)

rucs_hack (784150) | more than 6 years ago | (#21398719)

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.

I might be wrong, but it occurs to me that a program which 'proves' a mathematical hypothesis can only, on inspection, be shown to be a proof of the program itself, not the initial hypothesis.

The problem with software is that it can be made to do anything. Want to model colliding galaxies that mimic observed or hypothesised behaviour? Easy, jut twealk till you get the right result.
The result however will not be a 'proof' of the true mechanisms underlying the event in the real universe. The issue then is what you are trying to prove. If it's something that is outside of the domain of the computer, then you can't use it as a proof, since you almost certainly cannot reproduce enough of the influencing factors, in most cases you need to simplify to model in silico. If, on the other hand you aim is solely to produce a model that looks the same, but is not said to be trying to prove the mechanism of galaxy collision, then you can say the software is the 'proof' of your simulation being able to poduce something that looks the same.

If the problem being demonstrated is itself solely in the domain of software, then the software can be the proof, in way, albeit not the conventional meaning of the word proof as used in mathematics.

Consider machine learning as applied to pattern recognition. You design your classification data structure/algorithm, then construct software that optimises it to perform that pattern recognition as well as can be cheived.
In that case the result of the software can be considered the the evidence that supports the hypothesised performance, and the souce code would, in effect, be the 'proof' in loose terms, as it would be the means by which the aproach is shown to be valid.

In most cases, it would just be the result that mattered, but unless you can provide a description of the software, or the software itself, so the method can be independantly implemented and verified as producing the results you show, you wouldn't get taken seriously. In that way the software performs the same function as a mathematical proof. It can be independantly checked.

Re:Python is part of the answer (1, Funny)

Anonymous Coward | more than 6 years ago | (#21398973)

I am a mathematician.
Yeah right. I don't see any publications by you on MathSciNet, Mr. poopdeville.

Ruby could be the answer as well (4, Interesting)

Gadzinka (256729) | more than 6 years ago | (#21398547)

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.
I could also recommend Ruby for the job. It has all the features you recommend, and more. If you could forget for a moment about the monstrosity that is Rails (I don't know, lobotomy might do the trick), the language in itself is quite beautiful.

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:

myhash.each_pair do |key,val|
  puts "#{key}: #{val}"
end
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:

File::open("somefile.txt") do |fh|
  fh.each do |line|
      puts line
  end
end
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

Re:Python is part of the answer (0)

Anonymous Coward | more than 6 years ago | (#21398575)

"The are all manor of subtle mistakes"


Or not so subtle spelling mistakes. A manor is a large house. Manner. The word you want is manner.

Coq is another interesting tool (3, Informative)

DrYak (748999) | more than 6 years ago | (#21398637)

We may also mention Coq [wikipedia.org], a proof assistant wich is available under LGPL and runs on OCaml (which in turn is also open sourced and available on Linux).

This is a tool that can help mathematician prove their theorems.
It was notably being used in the proof of the four color theorem [wikipedia.org], as mentioned on /. [slashdot.org] (article about machine assisted proofs).

Re:Python is part of the answer (1)

Have Brain Will Rent (1031664) | more than 6 years ago | (#21398923)

It seems to me that if you were looking for a language for mathematicians that it would be something that is syntactically very close to mathematical notation... APL was/is such a language, and with all the interactiveness of Basic... but mathematicians aren't using it in any significant number and never really did.

Re:Python is part of the answer (2, Insightful)

Dare nMc (468959) | more than 6 years ago | (#21398937)

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.


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:Python is part of the answer (1)

Bert64 (520050) | more than 6 years ago | (#21398965)

Well, you're only really responsible for the correctness of your own code.
As to the compiler and CPU, so long as you use a combination that have been verified as correct by other mathematicians you should be fine.

speaking of proprietary (3, Insightful)

larry bagina (561269) | more than 6 years ago | (#21398069)

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.

Re:speaking of proprietary (5, Funny)

Main Gauche (881147) | more than 6 years ago | (#21398289)

"While it was typeset with TeX (open), only the PDF (closed and uneditable) is provided."

Indeed. Now we are left wondering whether the TeX code is buggy. Like maybe an extra character accidentally slipped into the file.

therefore mathematics software should %not
be open source!

Now we'll never know.

PDF rant. (4, Insightful)

serviscope_minor (664417) | more than 6 years ago | (#21398347)

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.

Re:PDF rant. (1)

Tango42 (662363) | more than 6 years ago | (#21398405)

"By the way, all scientific papers are disseminated by PDF."

Actually, most scientific papers I see are disseminated as PostScript (often with a PDF option for people without ghostscript or similar installed - basically, non-academics).

Re:PDF rant. (1)

serviscope_minor (664417) | more than 6 years ago | (#21398445)

Actually, most scientific papers I see are disseminated as PostScript (often with a PDF option for people without ghostscript or similar installed - basically, non-academics).

Not in my experience. PS is opten an option, but not always. LNCS (Springer?) for instance only offer as PDF. I think Elsevier and the IEEE are like that as well.

Re:PDF rant. (1)

saforrest (184929) | more than 6 years ago | (#21398497)

Actually, most scientific papers I see are disseminated as PostScript (often with a PDF option for people without ghostscript or similar installed - basically, non-academics).

Perhaps it depends on the field. In my experience, in computer science all recent papers are provided either as PDF alone or PDF + PostScript, and in my (very limited) experience with refereed publications, PDF is the accepted standard.

PDF has a lot of advantages over PostScript, the most obvious of which is internal hyperlinks.

Re:PDF rant. (1)

Tango42 (662363) | more than 6 years ago | (#21398657)

It may well depend on the field - my experience is with Maths papers. Also, I'm thinking of pre-prints rather than papers from journals - journals are more commonly PDF, now I think about it. But my point stands - PDF is far from universal.

Re:PDF rant. (1)

lahvak (69490) | more than 6 years ago | (#21398977)

I think lot of preprints used to be postscript because people simply ran TeX and dvips. With pdftex becoming more popular, I expect that is probably soon going to change.

Re:PDF rant. (2)

visualight (468005) | more than 6 years ago | (#21398561)

I would like a warning because I usually don't click on links to PDFs unless I really need the info. Not because it's proprietary or whatever, they just take a long time to load, and if it's a big one, my browser hangs while it's rendering.

Re:PDF rant. (2, Informative)

serviscope_minor (664417) | more than 6 years ago | (#21398649)

I would like a warning because I usually don't click on links to PDFs unless I really need the info. Not because it's proprietary or whatever, they just take a long time to load, and if it's a big one, my browser hangs while it's rendering.

Then get a better PDF reader. Even on a very slow computer, xpdf or ghostview have subsecond load times. If you use mozilla related browsers, then plugger will let you "embed" decent PDF readers. In fact if you install mozplugger under Ubuntu, it uses evince by default. If you don't use mozilla, then set it up to use $viewer as an external helper application.

My guess is that your bias against PDF comes from the awful Adobe viewer.

Re:PDF rant. (1)

Eivind Eklund (5161) | more than 6 years ago | (#21398857)

PDFs sucks in the default reader, and it often requires external shitty setup. This makes the format suck (on the web) for many/most people. Thus, it is courteous to give a warning. Whether a warning is unnecessary for YOU doesn't matter - it's courteous because the format is annoying for a large enough fraction to matter.

For me, I find it particularly annoying because the default Adobe PDF plugin on Windows sometimes crash my browser. I think that's true for many others, too, though I don't know that for sure.

Eivind.

Re:PDF rant. (1)

serviscope_minor (664417) | more than 6 years ago | (#21398969)

PDFs sucks in the default reader, and it often requires external shitty setup. This makes the format suck (on the web) for many/most people. Thus, it is courteous to give a warning. Whether a warning is unnecessary for YOU doesn't matter - it's courteous because the format is annoying for a large enough fraction to matter.

For me, I find it particularly annoying because the default Adobe PDF plugin on Windows sometimes crash my browser. I think that's true for many others, too, though I don't know that for sure.

Eivind.


Really? The default reader under Ubuntu seems OK. It sounds like you're using Windows, where there isn't a default reader. Sounds like you chose to install a bad reader. An interesting choice given that you don't like it and it crashes your browser. Do you think that a website aimed at techs should give a warning because some of its users are unable to install software that they like?

Perhaps slashdot should stop using HTML, since many people use internet explorer which is a sucky browser.

Or perhaps you should try browsing under a good Linux distro. It sounds like a much more pleasant experience.

Re:PDF rant. (1)

mfnickster (182520) | more than 6 years ago | (#21398673)

> Really, what is wrong with PDFs and why should they require a warning?

Well, for one thing, if you use unusual fonts or special symbols, you can never be 100% sure that the reader on the other end will see them properly.

PDF should include an option for graphically rendering fonts which the user doesn't have installed. After all, I've never taken a piece of paper to another location and suddenly seen the writing on it turn to gobbledygook - something I can't say for PDF.

Re:speaking of proprietary (0)

Anonymous Coward | more than 6 years ago | (#21398381)

The PDF from the 1srt version is a proprietary but open format at the same time and only the DRM part is closed, even if it have patents they are royalty free and only used for preventing incompatible implementation, for their history visit: http://www.acrobatusers.com/blogs/leonardr/history-of-pdf-openness/ [acrobatusers.com]

Re:speaking of proprietary (3, Informative)

StormReaver (59959) | more than 6 years ago | (#21398401)

"While it was typeset with TeX (open), only the PDF (closed and uneditable) is provided."

PDF is neither closed nor uneditable. Adobe publishes the complete PDF format for anyone to use free of charge. It may not be FSF Free (since Adobe requires that implementers adhere to certain rules that violate the principle of Free), but it's definitely not closed. Also, KWord will import it for further editing, text and images, so it's not uneditable (even if it's not ideal).

I agree with your main point, but let's cut PDF some slack.

Re:speaking of proprietary (2, Informative)

1u3hr (530656) | more than 6 years ago | (#21398507)

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.

I think (hope) you're joking, but several people who responded seem to be taking this at face value. It's wrong in several ways. PDF is an open format, and if you look at the file info, you see that this particular PDF was generated with Ghostscript. And it's quite simple to edit PDFs. Not as easy as, say HTML, but much easier than if it were, say, a TIFF file. I personally use Adobe Acrobat, but a great many free and commercial apps can read, write, and manipulate PDF files. That's why the format was created, for use in DTP, not a locked document format as some business people seem to imagine.

seriously, wtf? (4, Informative)

tetromino (807969) | more than 6 years ago | (#21398929)

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.
Oh, where to begin...
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 [adobe.com], 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 [petricek.net]. 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.

quote is out of context (1)

mr.Peabody (56428) | more than 6 years ago | (#21398083)

The J.Neubuser quote is in reference to using proprietary, closed source software for proofs. The point being that without seeing the guts of the software it is hard to tell if the proof is correct, or dependent on a flaw in the software.

Re:quote is out of context (0)

Anonymous Coward | more than 6 years ago | (#21398725)

This is highly misleading. A proof can be checked without knowing how it was obtained. (As a matter of fact, in some sense that's the whole point of a proof.) Proof checking is far easier than generating a proof in the first place. If a proof is generated by closed-source software, it can still be checked for errors quite easily. Access to the proof generator itself is not necessary.

The idea of "proof carrying code" (PCC) is fundamentally based on this observation.

Of course, a result of the form "software XYZ says it is true" is not a proof in the above sense.

Openness is Fundamental to Mathematics (2, Interesting)

aproposofwhat (1019098) | more than 6 years ago | (#21398087)

The article is a very well argued opinion piece, and is correct in that only open-source software should ever be used in a proof.

It is fundamental to mathematics that other mathematicians in the same field can check a proof, and the use of closed source software makes that logically impossible, for without access to the source of the application, it is not possible to guarantee that any particular operation has been implemented correctly.

He's also plugging his own open source project, SAGE [sagemath.org] - I might have to download it and see if the rusty old brain cells can figure out how to play with it ;)

Re:Openness is Fundamental to Mathematics (1)

tcgroat (666085) | more than 6 years ago | (#21398335)

If software is used in a formal mathmetical proof, then the software itself must be subjected to rigorous mathematical proof. Every step must be justified based on accepted postulates and previously proven theorems, or else the work isn't rigorous and doesn't qualify as mathemetically "proven". As I repeatedly tell my daughter about her alegbra, you must show your work: it isn't just coming up with the "right answer", it's about how you know it's the right answer. Opaque software isn't mathematic proof, it's saying "Trust me!". That line doesn't relieve the doubt, it only confirms suspicion that the proof is incomplete.

Re:Openness is Fundamental to Mathematics (0)

Anonymous Coward | more than 6 years ago | (#21398623)

If software is used in a formal mathmetical proof, then the software itself must be subjected to rigorous mathematical proof.

You phrased that awkwardly, almost as if you know what all the words mean. I doubt you know what you're talking about, though I hope I'm not insulting you as I say it.

A program cannot ever be verified for correctness enough to make results returned from it "proved." For example, consider the four-color theorem. It was "proved" in the 70s by enumerating all possible 5 element graph colorings and verifying that they could be turned into 4 color graphs. The source code has been poured over many times. And yet, it is not a proof. It is logically possible that the program produced an error despite having been implemented correctly. Proofs do not share this property.

Re:Openness is Fundamental to Mathematics (0)

Anonymous Coward | more than 6 years ago | (#21398843)

The four-color-theorem has meanwhile be re-proved using the Coq theorem proving assistant. While I agree that the 70s program was not a proof, the Coq proof certainly is.

Re:Openness is Fundamental to Mathematics (3, Insightful)

s20451 (410424) | more than 6 years ago | (#21398571)

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.

Re:Openness is Fundamental to Mathematics (0)

Anonymous Coward | more than 6 years ago | (#21398811)

I don't have MATLAB. If you showed me a proof that included "proof by MATLAB", I wouldn't believe you. You can't get away with that shit in most mathematics journals I read.

Re:Openness is Fundamental to Mathematics (1)

moosesocks (264553) | more than 6 years ago | (#21398909)

I'm not 100% sure, but I'm pretty sure that the source for many of MATLAB's functions (albeit copywrighted) is available for inspection.

Should journals reject such proofs? (3, Insightful)

davidwr (791652) | more than 6 years ago | (#21398107)

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.

Re:Should journals reject such proofs? (1, Informative)

Anonymous Coward | more than 6 years ago | (#21398435)

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.

Research is already exempt [wikipedia.org] from patent infringement. The "OMG, yuo cant do research because of teh patents!!!!" stuff you read here is pure fearmongering.

Not Proven (3, Insightful)

nagora (177841) | more than 6 years ago | (#21398141)

If a "proof" is published with some steps or information excluded then it's not a proof, it's just an assertion.

TWW

Re:Not Proven (4, Informative)

ciaohound (118419) | more than 6 years ago | (#21398251)

As a high school math teacher, I am familiar with some of the details of Thomas Hales' proof of Kepler's "Cannonball" Conjecture, concerning the most efficient way to stack spheres. When he first published his proof in 1996, he included the source code for the programs that were used to do the calculations for the thousands of possible sphere configurations. I think most of the code was actually written by his graduate assistant. At first that struck me as cheating -- "... and then this program runs. Q.E.D." -- but then I realized that if anyone else was to verify his results, they would need the programs. There are just too many calculations to perform without software, which is why the conjecture went unproven for four hundred years. But without the source code, it would smack of charlatanism.

Propriatary Software (4, Funny)

calebt3 (1098475) | more than 6 years ago | (#21398185)

Increasingly, proprietary software and the algorithms used are an essential part of mathematical proofs
Like Excel's 65,535-equals-100,000 formula?

file under self-serving nonsense (0)

Anonymous Coward | more than 6 years ago | (#21398187)

One of the authors acknowledges being the founder of an OSS project that provides... guess what... a comprehensive toolkit for mathematical research! So if research journals require computationally based proofs to use OSS, guess who's company will be the big beneficiary? And guess who personally will be in big demand to travel to conferences around the world explaining the concepts and methods of this suddenly necessary piece of software.

Bottom line is that computational techniques should be explained so that they can be duplicated or refuted using any software of the colleague's choosing. The aim should not be to turn pure mathematicians into maintenance programmers, having to gain proficiency with the 10 or so different languages and platforms listed by the authors at the piece.

Proof exchange format (2, Interesting)

David Deharbe (1150399) | more than 6 years ago | (#21398301)

IMHO, it would be an important contribution to establish an open proof exchange format that make it possible to... exchange proofs between different tools: theorem prover, proof checker, etc. Possibly this format would have a translator to a human-readable format (e.g. based on TeX) that would also make it possible for humans to review the proof process.

Re:file under self-serving nonsense (0)

Anonymous Coward | more than 6 years ago | (#21398659)

Why couldn't the author be right even though he stands to benefit from being so? If you perceive a need for more use of OSS in a field, isn't it natural to make it more feasible by founding an OSS project to make a readily available comprehensive toolkit?
Why would using open source instead of closed source products magically turn 'pure mathematicians' into maintenance programmers? Most matematicians I know are bright people, and have learned some pretty arcane computer stuff to use in their work, e.g. TeX/LaTeX and Fortran.

Welcome to the world of modern research ... (4, Interesting)

MacTO (1161105) | more than 6 years ago | (#21398209)

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.

Re:Welcome to the world of modern research ... (2, Insightful)

jhfry (829244) | more than 6 years ago | (#21398321)

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!

Re:Welcome to the world of modern research ... (2, Interesting)

mathcam (937122) | more than 6 years ago | (#21398835)

And, in the case of mathematics, I'm guessing that they are using it as a shortcut for those difficult analytic solutions.
This is certainly one application, but the use of computers in the more "pure" aspects of mathematics is nothing to sneeze at either. Programs like GAP for group theory, PARI for number theory, and Macaulay for commutative algebra and algebraic geometry play a significant role in the development of their respective subjects. For example, there's very little you can say about the Monster group [wikipedia.org] without the aid of computer calculations -- it's not that researchers don't understand the algorithms involved, it's that it's physically impossible (given reasonable time constraints) to say anything non-trivial without computer aid. To address the other concerns, unlike the numerical solutions, there are frequently completely independent algorithms for checking the results of your first algorithm, so that trusting the original algorithm is less of an issue.

From the flip side... (1)

3seas (184403) | more than 6 years ago | (#21398231)

...is this saying the American Mathematical Society is accepting proprietary software used in proofs?

Seems the only problem here is one of the position of the AMS regarding what is acceptable.

Re:From the flip side... (1)

poopdeville (841677) | more than 6 years ago | (#21398687)

No, they aren't. Computer-assisted "proofs" are not proofs. They're "results". Subtly different. Proofs have the force of logic behind them. "Results" aren't guaranteed to. A computer-assisted proof cannot be a mathematical proof because it is logically possible for a correctly implemented program to return a false result. This is true whether the source is available or not.

But the proof steps are known, right? (1)

DrEasy (559739) | more than 6 years ago | (#21398305)

I don't understand: don't these automatic theorem provers provide the steps they took to prove the theorem? As long as those steps are provided and can be verified, I don't see why we care how the proof was obtained. We don't always know how proofs obtained by humans were obtained either; they don't tell us what they had for breakfast that day or what inspired them.

There's probably not much insight that can be obtained by the source code of the theorem prover, you can always just assume that it was brute force with some optimization tweaks.

As long as you don't just take the proof at face value and that you verify the proof you should be fine, no? And if you used another software tool to do the verification itself, then verify the verification manually. And so on. Verifying the proof of a theorem should always be easier than coming up with the proof, so this is not a hopeless process.

Re:But the proof steps are known, right? (2, Informative)

flajann (658201) | more than 6 years ago | (#21398509)

The advantage of having the source code is that, in a lengthy proof that involves thousands of steps that may be hard to follow, one may have an easier go at proving that the software did the steps correctly. At least, if a bug were found that would save you many hours over sweating over the actual proof!!!

Open Formats (2, Insightful)

iamacat (583406) | more than 6 years ago | (#21398357)

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.

openmodelica.... (2, Interesting)

dohmp (13306) | more than 6 years ago | (#21398409)

not entirely on-topic, but i figured the slashdot community might be interested in this tool.

OpenModelica [ida.liu.se]

a very nice modelling package that can help you with practical mathematics issues like mathematica might.

cheers.

Peter

Not necessarily bad in all cases... (4, Insightful)

Ardeaem (625311) | more than 6 years ago | (#21398459)

There are some programs which can aid proofs that are closed source. This doesn't HAVE to mean that steps of the proof are omitted. Take, for example, Mathematica for the Web [calc101.com]. It can spit out a result, including all the steps (try a derivative). Or check out a sample Otter proof [anl.gov]. Mathematica is closed source, Otter is open source. However, even if both of these were closed source, all the steps would be laid bare for all to see.

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:Not necessarily bad in all cases... (2, Insightful)

mopslik (688435) | more than 6 years ago | (#21398683)

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.

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.

Re:Not necessarily bad in all cases... (1)

Ardeaem (625311) | more than 6 years ago | (#21398887)

But with the pseudocode, you can write your own program in whatever language you like to verify the results. In my opinion, proving something doesn't obligate you to show every single step. We all omit things in proofs, especially steps which can be verified easily by others, like algebraic simplification, etc. The pseudocode is the minimum acceptable transparency in a computer-aided proof.

Re:Not necessarily bad in all cases... (1)

HiThere (15173) | more than 6 years ago | (#21398975)

I've encountered too many programs where the source code doesn't match the documentation. For some of your arguments, that's not fatal. If the entire proofs are made explicit, then you can argue that it's like not being able to peer inside the skull of the mathematician. In the cases, however, where you are depending on the results of computational steps (as in the four color proof), those steps need to be made open and explicit.

Pseudocode is not sufficient. You don't know that it actually reflects the code that was used.

first: prove the correctness of your software (1)

petes_PoV (912422) | more than 6 years ago | (#21398515)

If you are using a software tool/package, then it must have been subject to mathematically rigourous tests to demonstrate it's own correctness. If not, then the foundation of any proofs that use it must be in doubt.

So, if you use a closed product, how can that have been proved corect (independently of the supplier, of course) without recourse to the source code?

What about hardware? (3, Insightful)

LM741N (258038) | more than 6 years ago | (#21398525)

I would think that hardware errors would be an even worse problem, like the old Pentium bug, since they are so insidious.

Why I don't trust Python (1)

Nuwdle (1190721) | more than 6 years ago | (#21398679)

Python 2.5.1 (current)...

Command Line:
>>> 1.00 - 0.01
0.98999999999999999

I hope I'm not the only one that thought of this one.

Re:Why I don't trust Python (1)

William Stein (259724) | more than 6 years ago | (#21398753)

The program Sage http://sagemath.org/ [sagemath.org] mentioned in the article uses Python extensively, but with a few changes when used interactively. In particular, all floating point literals are created as Python objects that wrap MPFR C-library objects http://www.mpfr.org/ [mpfr.org] which have better semantics. In particular, your example above in Sage becomes:

sage: 1.00 - 0.01
0.990000000000000

Likewise, in Python one has the confusing (to a mathematician):

>>> 1/3
0

In Sage integer literals wrap GMP integers http://gmplib.org/ [gmplib.org] (which are vastly faster than Python's large integers), and one has:

sage: 1/3
1/3

  -- William, http://wstein.org/ [wstein.org] (author of the article being discussed)

Re:Why I don't trust Python (3, Informative)

Just Some Guy (3352) | more than 6 years ago | (#21398841)

>>> 1.00 - 0.01
0.98999999999999999

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:

  1. Floats can only store exact values for the fractional part when the denominator is a power of 2. The "100" in "1/100" isn't a power of two, so IEEE 754 cannot represent it perfectly.
  2. .999999999... == 1, so the answer is still correct.
  3. If you must have exact answers, use the Decimal type:

    >>> 1 - decimal.Decimal(".01")
    Decimal("0.99")

Re:Why I don't trust Python (4, Informative)

fredrikj (629833) | more than 6 years ago | (#21398895)

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 [sun.com].

bad analysis, bad results (2, Insightful)

fermion (181285) | more than 6 years ago | (#21398699)

This seems to fall under the realm of researchers using tools they do not understand. Black box science does not work. As has been mentioned, the results cannot be shown to be valid.

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:bad analysis, bad results (-1, Offtopic)

Anonymous Coward | more than 6 years ago | (#21398949)

Blacks do not work.

And neither will Mexicans once they president Hillary and the democrats make them eligible for welfare.

look at who's speaking... (2, Interesting)

legrimpeur (594896) | more than 6 years ago | (#21398705)

... try to read a paper from their journal (JAMS http://www.ams.org/jams/2003-16-03/S0894-0347-03-00422-3/S0894-0347-03-00422-3.pdf [ams.org]) and you will be asked for... money. Well that's their interpretation of "... In mathematics information is passed on free of charge..." cheers

Re:look at who's speaking... (3, Informative)

William Stein (259724) | more than 6 years ago | (#21398837)

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.

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] ... and (using [Mathematica|Magma|...]) we deduce that [...].

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 ..." 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/ [sagemath.org]). And sometimes exactly that is necessary to go beyond what has already been done, i.e., to do research.

  -- William Stein

Norman Megill's Meta-Math for proof verification (3, Informative)

ClarkEvans (102211) | more than 6 years ago | (#21398745)

http://metamath.org/ [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

greed rears its ugly head (-1, Offtopic)

Anonymous Coward | more than 6 years ago | (#21398803)

what the 'fck' is it about the privileged that enough is never enough

even when others suffer death from deprivation

imho, affluent people are evil

Sage (3, Informative)

Anonymous Coward | more than 6 years ago | (#21398859)

Sage( http://www.sagemath.org/ [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/ [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/ [sagemath.org] .

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.

not really true (1)

superwiz (655733) | more than 6 years ago | (#21398871)

Mathematics goes in an out of the phases of being secretive and open.

Pythagoreans were very secretive. So were statisticians in the 19th century. I am pretty sure investment bankers do a great deal of math that they don't want anyone to ever see because it gives them an edge in the market.

It's sort of like gun powder. When first discovered, the secret is tightly controlled because it would gives advantage over the competition. Then the competition realizes that it is being consistently beaten and tries to emulate/steal the results. After a while, everyone knows what the results are.

And then the "philosophers" come in. That is the people who ponder the implications of the results discovered out of necessity. Since these people are not interested in any immediate payback, they insist that everyone shares the results so that more can be discovered by all. They try to convince everyone that this is the "natural" way of things.

But what is "natural"? Without the push of necessity the original results would have never been found. And without the contemplative phase of shared discovery, progress would not have been made to the point when the new era of rapid discovery done to assist in competition would come about. These phases of going in and out of secret (of math, science, heck of all knowledge that is used to maintain society) drive each other. So arguing for one or another is just another flame war.

Load More Comments
Slashdot Account

Need an Account?

Forgot your password?

Don't worry, we never post anything without your permission.

Submission Text Formatting Tips

We support a small subset of HTML, namely these tags:

  • b
  • i
  • p
  • br
  • a
  • ol
  • ul
  • li
  • dl
  • dt
  • dd
  • em
  • strong
  • tt
  • blockquote
  • div
  • quote
  • ecode

"ecode" can be used for code snippets, for example:

<ecode>    while(1) { do_something(); } </ecode>
Sign up for Slashdot Newsletters
Create a Slashdot Account

Loading...