[silentvoice]

Symbolic math is not the same thing as formalized math, and doesn't carry with it the same guarantees of correctness. That's the price one pays for having black box functions spit out answers to hard problems in a reasonable time, they won't spit out proofs of correctness alongside their answer.

Any symbolic system should be treated with care, but they can of course be extremely useful. My typical use case is to have it compute very challenging symbolic expressions for me. I then treat it as a "very plausible hypothesis" which I then prove.

[monochr]

That's only true for closed source systems. You can easily debug open source ones, look at their insides and so on.

This whole article is really just telling people to use the scientific method in computing too: if you don't know how to reproduce a result it's not science. Fast computation which a human can't possibly do is something that's new from the last 30 years and most scientists still don't know how to deal with it.

It is very sad to see that statisticians have switched to R, biologists to python, computer scientists to the gnu tool chain, yet physics and maths seem to have been colonized by mathematica when you have a whole set of open source tools which are superior in every way: pari pg, gnu arbitrary precision libraries, axiom, maxima and sage is you want everything under one roof with a unified interface.

[fddr]

As a former physicist that used Mathematica heavily not that long ago, I have to disagree. It would be great if there were open source alternatives that were "superior in every way" but that is just not the case.

For some use cases at least, Mathematica is clearly better than anything else I have tried.

I feel like something like ipython notebooks with the right combination of libraries might eventually get there, but that is unfortunately still years away.

[tel]

> "Easily debug"

One of the major driving forces in the design of computer proof systems is that they (a) output proofs along with assertions that are (b) trivially verifiable. Indeed, verification is a major philosophical and practical force behind the theory of any type theory.

Ultimately, this is a major component of the design of a proof checker because while lots of its pieces can be complex and scary and potentially buggy, the proof verifier must always be tiny and easy and impeccable because it bears the entire burden of safety.

A similar argument cannot really be made for CAS, I think. Even open source ones.

(There's a catchy name for this principle, but I forget it. "Somebody's Something")

[conistonwater]

> That's only true for closed source systems.

What? This is a software bug. Open source software has bugs just as closed source software has bugs.

The average user of sage is not going to go hunting for a bug in sage's source, whether it's available or not, which is just the same as with Mathematica. Examining an unfamiliar code base will be of no help when you want to know why a certain integral was evaluated incorrectly.

> open source tools which are superior in every way

They are not superior. At best they are equivalent. What you list is a number of disparate tools that may or may not cooperate together well. What Mathematica provides by way of competition is a set of reasonably polished packages, all in one place.

Mathematica also makes it possible to quickly write a one-liner that solves a problem and lets you move along. This experience is simply not there for tools like sage. Sage's plotting (matplotlib, IIRC) is just not comparable.

[tzs]

> That's only true for closed source systems. You can easily debug open source ones, look at their insides and so on.

Who is "you"? In fact, very few people can debug a modern symbolic mathematics system. They are fiendishly complex.

[dalke]

"if you don't know how to reproduce a result it's not science."

Astronomy is one of many sciences which can never reproduce its results in the way you're talking about. Do you not consider astronomy to be a science?

In any case, this paper was looking for counter-examples. If found, then they would be all the evidence that's needed. The method to compute the counter-examples is nice, but irrelevant.