# Open Source Math

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

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

## Lol (5, Funny)

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

## Re:Lol (1)

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

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

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

## 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)

Any software that contains i = i+1 must license my math.

## Re:Lol (4, Funny)

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

## Re:Lol (4, Funny)

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

## Maths...... (5, Funny)

## Seoulstriker (748895) | more than 6 years ago | (#21398695)

That's how I learned maths in high school.

## I don't know what to say (-1, Offtopic)

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

## Re:I don't know what to say (1)

## fbjon (692006) | more than 6 years ago | (#21398433)

## Re:I don't know what to say (1)

## Wonko the Sane (25252) | more than 6 years ago | (#21398963)

## It's all... (2, Insightful)

## Shikaku (1129753) | more than 6 years ago | (#21398057)

## 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)

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)

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)

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

## El_Isma (979791) | more than 6 years ago | (#21398549)

It's a GPL Computer Algebra System and it's in active development. I use it all the time.

## Re:Python is part of the answer (1)

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

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

## jrminter (1123885) | more than 6 years ago | (#21398827)

## Re:Python is part of the answer (0)

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

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

independentlydeveloped 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 (1)

## ndevice (304743) | more than 6 years ago | (#21398373)

## 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

is42. 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)

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)

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

needthe 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)

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

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

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

## Re:Python is part of the answer (0)

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

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)

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

## Re:Python is part of the answer (1)

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

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

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

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)

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)

## 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 %notbe open source!

Now we'll never know.

## PDF rant. (4, Insightful)

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

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)

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)

## Re:PDF rant. (1)

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

## Re:PDF rant. (2)

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

## 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)

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'ta 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)

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)

## Re:speaking of proprietary (3, Informative)

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

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)

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 filebother you any more than the proprietary fontface of a book?4. First of all, PDF

iseditable [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)

## Re:quote is out of context (0)

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

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)

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)

how you knowit'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

cannotever 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)

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

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

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)

## Re:Openness is Fundamental to Mathematics (1)

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

## Should journals reject such proofs? (3, Insightful)

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

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)

TWW

## I agree... (1)

## TheSHAD0W (258774) | more than 6 years ago | (#21398199)

## Re:I agree... (1)

## TheSHAD0W (258774) | more than 6 years ago | (#21398213)

## Re:Not Proven (4, Informative)

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

## Propriatary Software (4, Funny)

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

## Re:Propriatary Software (1)

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

## file under self-serving nonsense (0)

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

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)

## Re:file under self-serving nonsense (0)

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

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)

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)

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)

## From the flip side... (1)

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

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)

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

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

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)

## Open Formats (2, Insightful)

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

## openmodelica.... (2, Interesting)

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

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)

even ifboth 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)

Perhaps I'm being too pessimistic, but shouldn't the source code

haveto 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 readsINCREMENT 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)

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

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

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)

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)

## Why I don't trust Python (1)

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

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)

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)

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:

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

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

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)

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)

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)

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

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

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 commonright 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

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

## Re:look at who's speaking... (0)

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

http://sage.math.washington.edu/home/wdj/research/index.html [washington.edu]

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

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

## greed rears its ugly head (-1, Offtopic)

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

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.