Slashdot Mirror
Open Source Math
An anonymous reader writes "The American Mathematical society has an opinion piece about open source software vs propietary software used in mathematics. From the article : "Increasingly, proprietary software and the algorithms used are an essential part of mathematical proofs. To quote J. Neubüser, 'with this situation two of the most basic rules of conduct in mathematics are violated: In mathematics information is passed on free of charge and everything is laid open for checking.'""
Thanks for the article, now some crazed company is going to try to copyright math.
about the money.
I am no a mathematician but surely if you're going to submit a computer aided proof you must submit a full copy of the program. The are all manor of subtle mistakes that can be made in a program that could cause serious problems with a proof.
Suppose you inspect the source and find it to be faultless, how can you trust the compiler. And if you hand compile the compiler, how can you trust the CPU? Surely it's turtles all the way down.
In many ways, establishing the correctness of a computer-aided proof is very much like security engineering. You want to verify that the whole software stack is operating correctly before you can trust the result. Having the source-code is a pre-requisite to this exercise.
Changing to topic slightly, I was particularly heartened to see that the open-source mathematics framework being developed one of the authors of the article involves the use of Python.
My immediate thought when seeing the title to the article was "Python is the answer." When some problem or algorithm intrigues me the first thing that happens is that I reach for the Python interpreter.
Python seems to deftly marry precision with looseness. When code is laid out in Python I find it is easier to see what it's trying to do than other languages. It's aesthetic qualities aside, it supports a number of features out of the box which I imagine would be ideal of mathematicians. To list a few, it's treating of lists and tuples as first class objects, support for large integers, complex numbers, it's ability to integrate with C for high-performance work.
I often think of Python as "basic done right" and it's ideal for mathematicians (or anybody) who don't want to think about programming but the problem at hand.
Simon
The article (which is actually a PDF, thanks for the warning) uses proprietary fonts (LucidaBright). While it was typeset with TeX (open), only the PDF (closed and uneditable) is provided.
Do you even lift?
These aren't the 'roids you're looking for.
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.
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 - I might have to download it and see if the rusty old brain cells can figure out how to play with it ;)
One swallow does not a fellatrix make
Algorithms cannot be protected by copyright, only by patents and trade secrets. If the algorithm is a trade secret, it has no place in a mathematical proof because it cannot be shared with the world and verified or refuted by anyone interested in doing so.
If the algorithm is part of a patented device or piece of software, its use in a mathematical proof is not subject to the patent on the grounds that pure math cannot be patented.
If journals and academic societies refused to publish proofs based on trade secrets and insisted on a covenant not to enforce the patent against researchers doing purely mathematical research or those who publish the research, the problem would mostly go away. An alternative to the covenant is congressional action or a court ruling that says with absolute clarity that mathematical research is exempt from math-related patents directly related to the research.
--
Personally, I'm against all such patents but I'm not holding out hope that Congress or the Courts will agree with me.
Knowledge is how to play a game, intelligence is how to win, wisdom is knowing what game to play.
TWW
"Encyclopedia" is to "Wikipedia" what "Library" is to "Some people at a bus stop"
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.
...and I don't think journals should accept papers which don't include proofs verifiable only with closed-source software.
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.
...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.
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.
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.
"In our tactical decisions, we are operating contrary to our strategic interest."
How is it I can tell you're a Linux user?
Why does this keep coming up on ./? What is wrong with PDF? It's undeitable, sure, that's kind of the point. However, the spec is accessible, and there are plenty of open readers, e.g. xpdf and ghostscript.
Really, what is wrong with PDFs and why should they require a warning?
By the way, all scientific papers are disseminated by PDF.
SJW n. One who posts facts.
Proprietary math software is not a problem as long as the end result can be exported into a fully documented format and can be then verified by open software, including human mathematicians.
not entirely on-topic, but i figured the slashdot community might be interested in this tool.
OpenModelica
a very nice modelling package that can help you with practical mathematics issues like mathematica might.
cheers.
Peter
True confidence comes not from realising you are as good as your peers, but that your peers are as bad as you are.
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.
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?
politicians are like babies' nappies: they should both be changed regularly and for the same reasons
I would think that hardware errors would be an even worse problem, like the old Pentium bug, since they are so insidious.
There is one special feature of Ruby, that I miss in every single programming language I used since: iterator methods. Any time I want to iterate over elements of an array or hash I just do: That's it, instant "anonymous function" given as a parameter in estetically pleasing syntax. In fact, "for" loop in Ruby is just obfuscated way of calling method #each on an object. But the madness doesn't stop here: It's a pity that so many people disregard Ruby as a "platform for Rails". It is a feature complete countepart to Python, and as my company high volume systems can attest, can handle anything other languages can handle.
Robert
Bastard Operator From 193.219.28.162
We may also mention Coq, a proof assistant wich is available under LGPL and runs on OCaml (which in turn is also open sourced and available on Linux).
/. (article about machine assisted proofs).
This is a tool that can help mathematician prove their theorems.
It was notably being used in the proof of the four color theorem, as mentioned on
"Sufficiently advanced satire is indistinguishable from reality." - [Tips: 1DrYakQDKCQ6y52z6QbnkxHXAocMZJE61o ]
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.
Look around you. Look around you!
That's how I learned maths in high school.
I am defenseless. Use your button. Mod me down with all of your hatred.
A recall a few recent incidents in which papers had to be retracted because the machine did not do what the researchers thought it did. I have personal experience in which the spectroscopy generated by the computer did not reflect reality. If the researcher does not know how to use a tool, then he or she does not know when that tool is being misused.
I am not sure something like mathematica is the issue. Wolfram seems to use standard standard well known algorithm. Almost every academic institution has a license, so, given the data, any number of people can rerun the analysis. Likewise the algorithms can be tested with simpler data sets to understand how they work and breakdown. I would be more worried about homegrown software.
"She's a scientist and a lesbian. She's not going to let it slide." Orphan Black
... 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) and you will be asked for... money. Well that's their interpretation of "... In mathematics information is passed on free of charge..." cheers
http://metamath.org/ has been around for 15 years or so; it has a very nice text-based proof expression, a huge library of existing proofs and a graphical visualization tool
Sage( http://www.sagemath.org/ ) is currently the most full=featured open-source computer algebra system. It is being developed by the two authors of the AMS opinion piece (and many others including myself). Our goal is to provide a free, viable, open-source alternative to Mathematica, Maple, MATLAB, and Magma. Some nice features of Sage include:
* It uses Python as its programming language so that you can use any existing Python modules with your Sage programs.
* Sage also includes Cython ( http://www.cython.org/ ) which is based on Pyrex and allows one to easily compile Python code down to C for speed.
* Sage's notebook interface with also interface with pretty much every existing computer algebra system, open-source or not.
* Sage includes Maxima, GAP, Scipy, Numpy, and many other open source math packages.
* A very active developer community. If there is something that you need Sage to do, chances are that there will be a number of developers willing to help you out.
For some screenshots, see http://www.sagemath.org/screen_shots/ .
One of the things that Sage needs most now is more users. So, if you have an interest in open source math software, definitely check out Sage.
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.
Any guest worker system is indistinguishable from indentured servitude.
1. The only reason you would need a "PDF warning" is that you use an operating system with poor support for the format (i.e. Windows). Switching to a real OS, among other benefits, will make reading math papers (which are almost always in PDF format) a pleasure.
2. PDF is an open standard, which has been implemented by many different parties: Adobe and Apple have closed-source implementations; freedesktop.org's poppler and cairo libraries are Free software.
3. The fontface chosen by AMS is orthogonal to the content of the paper - you can easily copy-paste the text and use Computer Modern, Dejavu, Liberation or any other open-source font of your choice. Why would a proprietary font embedded in a PDF file bother you any more than the proprietary fontface of a book?
4. First of all, PDF is editable. And second, why would you want to edit this particular document? Remember, it's copyrighted by AMS - if you can't prove fair use, you do not have the right to distribute a modified version.
I am convinced that this is the best xkcd ever.
Much of the guts of Mathematica -- the high level functions -- are available for perusal at http://functions.wolfram.com/ Much of the reason why Mathematica works so well is due to careful consideration of branch cuts.
For example, what is Log[a b]? If you look in almost any math book, you'll find Log[a b] = Log[a] + Log[b]. That works fine most of the time, but tends to fail in devastating ways when combined with other functions. The open source programs tend to follow this "good enough" approach.
Log[a*b] == Log[a] + Log[b] + 2*I*Pi*Floor[(Pi-Arg[a]-Arg[b])/(2*Pi)]
is the very careful way to handle the log function.
http://functions.wolfram.com/ElementaryFunctions/Log/16/04/0005/
Do these theorem gap proving helpers not produce a human readable proof? Or do they simply return T/F? Seems quite easy to build in a logging mechanism to keep track of how the proof proceeded in the software and then write a human readable, though probably quite ugly, proof. As long as the proof gets spit out in human readable form the "author" and the readers of such academic papers should attempt to follow the proof and check it for errors.
I'm not going to disagree with the "laid open" part, but the "free of charge" nonsense is just typical marxist university professor hypocrisy.
Let's price some math texts:
Or try a few titles which might be a little more familiar to Slashdotters:
Princeton, which has the finest mathematics department in the world [or at least had the finest mathematics department in the world, before Harold Shapiro & Shirley Tilghman decided they wanted to turn the
These guys are advocating setting up a peer-review process for open source software in machine learning. The idea is that this would encourage researchers to spend more time on the software component of the publication, and perhaps produce something that others can use aswell.
The article is in the Journal of Machine Learning Research.
I'm a chemist involved in academic and industrial research and have to say its been this way in my field for a while. Profs. are trying to make a buck off government funded research and corps are very secretive with their technology for obvious reasons. Its all "intellectual property" - math, physics, chemistry etc. so since we have a system to make ideas equal "property" any idea can be fair game.
We all buy pens and paper without complaining, we should all just buy Mathematica without complaining.
I think they meant to say "non-Mathematica proprietary software".
My point, its always going to hard at the bleeding edge, if its was easy the bleeding edge would already be futher down the path of knowledge growth.
SPSS is the big stats package that all the social sciences and Psychology departments use. It is proprietary. Universities everywhere have bought into this package and the proofs for everything every student produces is on the Blind Faith of SPSS. And you bet you have to pay for it. There is FOSS alternative to SPSS, it is called 'R'. It is not well known. It is hypocritical of academic institutions anywhere to insist that their students prove their work on SPSS, since the code upon which the proof rests cannot be seen.
I've applied for a patent for the carefully aimed use of airborne chairs for intimidation of employees, particularly when they are threatening to resign to go to work for a competitor.
I was able to prove the unified theory of everything using "secret" proprietary algorithms...
http://www.scienceteecher.com/miracle_large.jpg
My rights don't need management.
Would these be the same kind of good-for-nothing, lazy, worthless asses who brought us Special Relativity while working in a lowly position in the Patent Office in Bern? You know, the kind who got together with friends to peruse and discuss the latest freely available scientific texts, the same texts that led him to revolutionise science more than anyone since Newton?
The books in the Princeton Library are free, thanks to the generousity of far-seeing individuals who realised that their money was better spent on a library than a new yacht. They, at least, saw the benefit of sharing knowledge with everyone, regardless of their means. I can only hope that, somewhere in that misanthropic little husk you call a heart, you will some day find room for a similar spirit of openness and sharing.
Crumb's Corollary: Never bring a knife to a bun fight.
Yeah, I got A's in college, too.
It IS Python's fault! It is also a trade-off knowingly made in programming languages.
IEEE standards simply mean that everything FAILS the same way. Less surprises, more calculated risks. But what is important according to this article is whether the AVERAGE math or physics grad, without a CS background, is going to know that.
Ding! Ding! Ding! And that's where the problem comes in!
Try using PHP to calculate the distance between 2 geographical points across the country... oh, wait a minute, you can't! Why? Because the number gets really big, then really small, then really big, etc. You're left with a number that has lost all of its floating point precision... thus being wrong!
Wait a minute, are you saying that the right formula gives the wrong results? YES!!
So that just leads us back at the entire point of the article. How do mathematicians know that they can trust the results of formulas they put into software? The answer: They can't.
Instead, let's be honest with people and tell them this is the best guess and highest probability that the result will be correct. Run simple tests. Check your results. Be diligent. If something doesn't add up, it might actually be because it didn't.
All the IEEE-754 documentation in the world can't change the fact that the wrong answer is the wrong answer... and mathematicians need to know that.
There were differences on the same calc circa 2003-I think it was regression or anova analysis--why is it different (math) and which is correct?
Just today, I sent in my annual membership renewal to SIAM even though the president this year is Cleve Moler who invented matlab(TM), the secret language of crippled users of matrix algorithms. http://www.siam.org/election/president_letter.php
A bit offtopic, but you mention you tried Octave. I myself use Scilab, but never have tried Octave. I've skimmed the docs and they seem very similar. Can someone elaborate on the differences between them? Which one is better?
The books in the Princeton Library are free, thanks to the generousity of far-seeing individuals who realised that their money was better spent on a library than a new yacht.
One other thing: The libraries at Princeton are most decidedly NOT free:
http://library.princeton.edu/about/access-firestone.php
http://library.princeton.edu/about/access-branch.php
To gain admittance, you need to pony up $33,000 in tuition and $11,000 in room and board.
Each year.
The issue is not whether software companies should make their source code open - the real issue is should mathematicians accept proprietary applications as proof of theorums?
As pointed out in the editorial, software developers make mistakes, and this is true regardless of whether that developer is a proprietary software vendor, or a free/open source software project. There is one key difference however, the validity of any given proof can be determined independently when using free/open source code by the very nature of the product (availability of source code). There is no validation for proprietary software beyond the assurances of the company involved.
When mathematic theory becomes applied mathematics (such as the creation of buildings, bridges, aircraft, or thermonuclear devices), which proof would you prefer to hang your life upon - Microsoft's guarantee, or independent verification and peer review? This becomes ever more critical as we create more complex systems that can not be easily verified by hand, yet rushed into applied use by the expediency/efficiencies they deem to provide.
Lodragan Draoidh
The more you explain it, the more I don't understand it. - Mark Twain
I previously used MATLAB in university, and have recently discovered Octave. What would I miss in Octave that would be available in MATLAB?
Also, when you say that the benefits are worth what the institution pays, I presume that you might not find it worthwhile if you yourself paid? I can't even find the price for MATLAB for Linux, because the MathWorks web site wants me to log in before quoting a price for me. I'm not sure they're interested in selling copies to individuals.
404555974007725459910684486621289147856453481154 in hex is "You sank my Battleship?"
[GPG key in journal]
As pointed out in the editorial, software developers make mistakes, and this is true regardless of whether that developer is a proprietary software vendor, or a free/open source software project.
Goro Shimura used to say that 50% of all published "mathematics" was rank nonsense.
Personally, I think he was being generous - I'd guess the figure is more like 95%. Maybe even 99%.
Heck, I'll bet there are even some mistakes somewhere in Higgins on Sampling Theory:
Volume I; $171.60
http://www.amazon.com/dp/0198596995/
Volume II; $264.00
http://www.amazon.com/dp/0198534965/
It's just a crying shame that I have to pony up almost $500 for the honor of discovering them.
WTF?
The Princeton Libraries are NOT FREE!!!
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.
..." -- that's nice. The stable release today just isn't quite there yet.)
So what kinds of optimizations does its compiler perform? How's Unicode support? Where's the description of its grammar? How stable are its OpenGL bindings? (I know the answer to most of these is "Ruby 2.0 is going to
I love Ruby, and I use it every day for my job, but I wouldn't claim it "can handle anything other languages can handle". Every language has strengths, and I'd be a fool to claim otherwise, or even that Ruby's strengths were exactly the same as Python's. (If you mean Turing-completeness, then your statement is true but completely worthless.)
Python's great for some things. Rails, as much as some people hate it, is a particular strength of Ruby. If I need a fast native compiler where I can make sure that my inner loop is running in under 30 CPU instructions, I'd be a fool to use either, and I'll pull out my Lisp compiler instead.
Precisely why, when I bought Stephan Wolframs "A New Kind of Science" that I was dismayed by the fact that a lot of the experiments he conducted could not be replicated without a four thousand dollar layout for his Mathematica product.
A product that is owned by his own company, is closed source and which he posits a great deal in his book.
I think we have to examine closely scientific methods that require a great deal of kick back money in order to replicate the results of experiments.
It seems very, well......unseemly.
-Hack
Got Geometrodynamics? Awe, too hard to figure out? Too bad.
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.
I'm pretty sure investment bankers aren't publishing in mathematical journals.
This isn't about applied math, this is about theory. Investment bankers don't need to produce proofs, let alone publish them... the results are all that matters. Investment bankers and statisticians aren't pushing the boundaries of mathematics, the way you imply, they're applying the framework created by pure mathematics.
This isn't like gunpowder, at all. The practical application of most pure math is decades after its discovery, if at all. Even the closest discipline to "practical pure mathematics", cryptography, is more a matter of mining theorems looking for operations that have properties useful to crypto... and the underlying work is based on applications of well known work.
But for all that, crypto has had to accept that it's most effective and most useful when it's published and open. That's just what has been found to work best for pure mathematics... which is why it's considered "natural".
It is entirely possible to use closed source black box programs to help develop proofs, all based on the fact that in a proof the existential quantifier does not require you to show you how you found the object, only prove that it satisfies the properties required. The program only needs to output the object, plus some "certificates" which can be used to check that the object satisfies the necessary proposition.
For example, consider integer factorization. Suppose you need to factorize a specific integer in your proof (for example a hard upper bound). Given a large integer, we don't care how some program factorizes it, in maths we only care about the factorization. The certificates are the factors, which can be multiplied to check that they are the factorization. Once we have the factorization the proof doesn't care how we got it.
Another example would be proving inequalities of polynomials in the reals. For this we can use sum of square decompositions, and semi-definite programming can give those decompositions. However, the proof doesn't need to know how we got the decomposition, only that we can certify that the given decomposition is indeed correct.
Now a lot of this changes if you use a different existential quantifier, like the constructivists. For these quantifiers more information might be necessary. Are we looking for an open source existential quantifier?
>> Black box science does not work.
That's unfairly harsh. Nearly all science done today is black box science to some extent. I work on molecular systematics. I understand a great deal about the biology of the system I work on, the mathematical underpinnings of the multivariate analyses I do, and some of the biochemistry involved in the reactions I run. However, I do not know how a PCR machine works, beyond the trivial observation that it heats stuff up and cools it down. I could not tell you how the gel I load onto a sequencer converts the samples I load into the picture I analyze three hours later, beyond an equally naive explanation.
This does not invalidate my work, but it does highlight the importance of using open source protocols. Outside of math and physics research, science is far too complex for any individual to understand every aspect of their research apparatus. We rely on each other to fill in the gaps. I have the skills and training to validate a small component of my research. But by using well-documented procedures and relatively widely available equipment, the bits I can't validate myself can be checked by others with appropriate background. But if I use proprietary protocols, reagents, or software, then I can no longer rely on the community to validate my work.
I wish I could say all my work used Free Software and open protocols. It's something I strive towards, and advocate for in areas where I have any say. But too many researchers are too focussed on producing high quality results in their specific area of specialty, to the extent that they rely on proprietary shortcuts in areas that they see as peripheral.
yp.
It's called Math You Can't Use - by Ben Klemens. Makes a bunch of great points in favor of open source, too.
change:
(This is one of that all variables aren't global...
to:
(This is one of the reasons that all variables aren't global...
I think we've pushed this "anyone can grow up to be president" thing too far.
For those who may choose not to mess with PDF - or just not have a PDF reader handy - Google usually will convert stuff to HTML for you. Here's their version of this paper: http://www.google.com/search?q=cache:4Kt5IJC2oWYJ:www.ams.org/notices/200710/tx071001279p.pdf+%22Open+source+mathematical+software%22&hl=en&ct=clnk&cd=4&gl=us
Waiting for Maple to load, I have seen the Java coffee cup icon. It looks like Maple is using Java for the UI as is Matlab these days to help with portability across OS's.
Sorry about the writing. Robot fingers, you know? Cliff Steele in DOOM PATROL #23
On the subject of open source math, Axiom is an interesting 30 years-and-running project started (I believe) at IBM research that recently became open source. A new branch of the project started recently: http://www.open-axiom.org/ and has several people actively working on it. It differs perhaps most significantly from Maple and Mathematica in its use of strong static type checking. This allows its library creation language to be compiled into C, which gets compiled and loaded back into the interactive top-level. Altogether, a very neat system and a gigantic resource.
Mathomatic is a quick and handy package to use for your more everyday math problems. It celebrates 20 years since its first release this year and is still updated with its latest release, version 12.8.0, just three days ago.
For programmers, its 'code' command converts your math problem to source code in your choice of several programming languages.
For more info see http://www.mathomatic.org/math/adv.html
Many thanks for writing it, George Gesslein II.
Trusted Computing FAQ | Free Dawit Isaak!
> the same texts that led him to revolutionise science
> more than anyone since Newton?
Oh please cease this endless hero worship.
Relativity, general and special, was inevitable. Theory was
inexorably marching forward. Any number of theoreticians were
on the cusp of relativity.
Einstein was a genius, but he was not a unique genius.
All he did was join the dots faster than the others.
Python is not part of the answer. Neither are Ruby, Lisp, ...
The problem of trusting a proof by computer is that the languages listed above are too big to be trusted. But that problem has been solved by building engines that are so small that people can fully comprehend them. Then, the engine can be extended by proving theorems using selected fundamental axioms. Combining such proven theorems to derive new theorems is what constitutes a proof.
Here is a list of 100 mathematical theorems and a list of systems used to proof them: http://www.cs.ru.nl/~freek/100/. Mathematicians are taking systems like Coq, HOL, Mizar etc. serious but proofs in Mathematica or Python are not acceptable.
Of course, those systems are written in general purpose computer languages, too. For instance, HOL light is written in OCaml. Errors introduced by the underlying language must be excluded by running the system on different implementations, different hardware, etc. But many mathematicians believe that being too paranoid about a minimal proof assistant is fruitless and only leads to the descend into a fundamentalist death spiral.
Microsoft Enterprise Independent Verification 2008 and Peer Review XP
Why? If you do a proof without a program, you don't have to submit a full copy of your brain, do you?
The "proof" is the thing that proves the theorem (hence the name), and it must do so in adequate detail showing all necessary steps and, as necessary, justifying them. If it does so, no additional information about how it was decided to take particular steps is necessary. If it does not, it fails regardless of what additional information provided.
Two points.
FIRST: I got into this discussion because the hypocrisy of it infuriates me so much. These hypocrites want tens of thousands of dollars of compiled code for free, and, beyond that, billions of dollars of source code for free - yet they won't post their LaTeX's or their PDF's for free [choosing instead to have Springer Verlag, Wiley, Elsevier, et al, demand $150+ per copy], they won't give away their journals for free, they won't open their libraries for free [demanding instead that you pony up $40,000 to $50,000 in tuition, fees, room, and board before you can get an ID card that will offer admittance to the library], they won't open up their student lectures for free [see ID card, as above], they won't open up their conferences for free [try sneaking into a conference lecture hall without an ID badge], etc etc etc.
Look, I don't have a dog in this fight - I think that people should be free to give away their intellectual property gratis, but I also think that people should be free to demand payment for their intellectual property, in the form of cold, hard cash.
On the other hand, if these hypocrites really want to put their moneys where their mouths are, then they can take their multi-billion dollar endowments [Princeton or Harvard could EASILY do this], and purchase these [relatively] puny little companies, like Mathworks, Wolfram, National Instruments, etc, and, once they own the source code, they can simply give it away for free.
In fact, their endowments are so monstrous these days that they could easily afford to pay the salaries of the coding staffs of these [relatively puny little] companies to continue updating, refining, and perfecting the source code from now until the end of time.
SECOND: Now this is not something which drew me into this discussion, but it's an important point which needs to be made, namely: It is not necessarily the case that "free source code" always implies better, less error-prone code.
As an introduction, let me start with a few ugly, little-known facts about "mathematics", as it actually exists in the real world:
1) Most published "mathematics" doesn't even qualify as false - rather, it's just gibberish, plain and simple. If a person with a sufficiently high IQ, a sufficiently meticulous personality, sufficient time on his hands, and sufficient sleep at night [leading to sufficent energy in the daytime] - if such a person were to examine the average published "mathematics" paper, then he would quickly come to realize that the words in the paper didn't even coalesce into logically well-formed statements.
2) Within the subset of published "mathematics" which isn't outright gibberish, most stated "results" are false: If a person with a sufficiently high IQ [and personality/time/sleep/etc] were to examine the average non-gibberish "mathematics" paper [after it had passed muster with Kurt Gödel & Alan Turing's gibberish-detecting filter, to ensure that it wasn't gibberish in the first place], then, pretty early on, he would come to realize that there were intractable errors in the paper, and he'd throw his hands up in despair and move on to some more productive use of his time.
3) Within the tiny subset of all published "mathematics" papers which aren't gibberish, and which contain assertions which are actually true, and which contain "proofs" of those assertions which aren't riddled with intractable errors, it is still exceedingly unlikely that a dis-interested third party [with sufficiently high IQ and personality/time/sleep/etc] will ever come along and verify that the paper is correct in the first place.
Only a tiny, tiny fraction of all "results" in mathematics these days ever draw the attention of the right people, in sufficiently high quantities, for a consensus to emerge [among the right people] that the result is actually true and ought to be added to the canon.
As an example, consider the "proof" of