most recent 30 from http://mathoverflow.net 2013-05-21T19:38:05Z http://mathoverflow.net/feeds/user/4811 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/19046/open-source-mathematical-software/19059#19059 mathy 2010-03-22T20:23:57Z 2010-03-22T20:56:09Z

<p><em>The kind of program I have in mind is Mathematica or Matlab. Altough probably those are not designed por abstract mathematics.</em></p> <p>What would be extremely useful to the progress of abstract mathematics would be a library of mathematical algorithms which were <em>formally verified for correctness</em>. Results obtained via such a library could be routinely cited in research papers without any doubt as to their correctness. The authors of SAGE suggest open source software as a means of achieving "research grade" mathematical software in [ <a href="http://www.ams.org/notices/200710/tx071001279p.pdf" rel="nofollow">http://www.ams.org/notices/200710/tx071001279p.pdf</a> ][ <a href="http://wstein.org/mathsoftbio/history.pdf" rel="nofollow">http://wstein.org/mathsoftbio/history.pdf</a> ], but arguably they don't go far enough.</p> <p>None of the "open source" mathematical software mentioned here currently meets this standard; the closest is C-CoRN [ <a href="http://c-corn.cs.ru.nl/" rel="nofollow">http://c-corn.cs.ru.nl/</a> ], a library of constructive mathematics for the Coq proof assistant.</p> <p>Now don't get me wrong, building a <em>comprehensive</em> library of formalized mathematics covering even the undergrad curriculum would be a vast undertaking. But the benefits would be huge, not just for computational mathematics but for all kinds of mathematical practice. The main obstacle is the nature of the work involved, which tends to be tedious and offering little reward to professional mathematicians, if occasionally playful and addictive. Perhaps undergraduate students should be encouraged to take courses in logic and contribute to such efforts.</p>