“I wonder if mathematical software today is so good that it can do better than humans at symbolic manipulation. This would mean that it would be really worthwhile to acquire some background in using such software, especially in those fields of research where one often has to deal with huge formulas.”
I would say faster and more accurate symbolic manipulation is one of the main points of Mathematica so yes I’d agree with the above implication and that it would be worthwhile acquiring some background.
Symbolic manipulation appears in many contexts however, and your header question about its usefulness in “pure theoretical research in Mathematics and Computer Science” is almost a completely separate (and loaded) question in itself with its own philosophical and practical overtones well beyond the two subquestions posed. These subquestions do tangentially relate to these overtones though:
Citations:
"beginning from formula X, using Mathematica we get Y" I think as general rule this would be OK provided details are provided (perhaps in appendices/code attachments) about how this was done and in particular how such results can be reproduced. Usually it is the conceptual insights that are of interest more so than the mechanical manipulation. The other way is to cite computational work is to create a related Demonstration and cite this using it’s own citation syntax (that appears below each Demonstration).
Correctness:
For sufficiently large manipulations I think correctness actually becomes much more of an issue if Mathematica (or similar) is not used. The chance of error doing this manipulations by hand is much higher that from using Mathematica's inbuilt transformations. I’d even go further and say the chance of an error using these inbuilt transformations is actually much lower than the chance of an error appearing in published theoretical proofs (usually done entirely by hand). The caveat to this is of course good programming practice that builds upon these transformations and constant vigilance some of which Leonid mentioned but some rules of thumb I’ve found useful are:
For lower-dimensions, implement solutions using at least 3 different (“conceptionally orthogonal”) methods.
(The flexibility of Mathematica’s language means this is usually not too difficult and provides a good margin of error)
For higher-order dimensions check for lower-order consistency
(It is usually impractically to refine 3 different implementations so usually it is sufficient to settle on one for refinement and efficiency improvements in tackling higher-order dimensions)
Use sanity checks often
(graphs, implications of output in relation to obvious truths)
Use validation suites routinely (either unit tests in Wolfram Workbench, or custom-made ones in the frontend- my preferred method)
Cross-reference with other published algorithms/output
Keep an open mind that errors are possible given these aren’t proofs but try to categorize possible error sources - e.g. One crude, overarching one for error sources:
1) Your algorithm
2) The implementation of your algorithm
3) Mathematica’s transformations
4) Your computer system
I’d say 3) and 4) are pretty unlikely error sources; 2) is where most errors occur and hence its focus in the above measures (which can also help in confirming that 1) is a publishable result).
To the specific question in the header -take theoretical computer science (TCS)- one could ask is it even a result in “Theoretical Computer Science” if Mathematica is heavily involved? This comes down to definitions and philosophy. There is a school of thought that for example experimentation using high-performance computation in TCS is unlikely to yield too many insights. (I’m talking about traditional experimentation, not actual TCS proofs in mathematica which is again is an even more loaded question.)
Take one luminary - Scott Aaronson’s view about using high-performance computation in TCS research given in a presentation in which he states (slide 4):
The hope: Examining the minimal circuits would inspire new conjectures about asymptotic behavior, which we could then try to prove
Conventional wisdom: We wouldn’t learn anything this way
- There are $~2^{2^{n}}$ circuits on $n$ variables — astronomical even for tiny $n$
- Small-$n$ behavior can be notoriously misleading about asymptotics
My view: The conventional wisdom is probably right. That’s why I’m talking in this session.
This stackexchange entry indicates some successes in in experimental complexity theory although it appears pretty limited and in limited domains.
I can offer a kind of counter-example in a Demonstration in which for a type of CNF circuit a conjecture about asymptotic (threshold) behaviour is surprisingly clear from considering only the first few dimensions $n=2,3,4$ (it had been checked statistically for larger values of $n$ and in related theoretical work)
(Note how “The hope:” part above implicitly reveals what is considered TCS or of value in TCS).
Then there are also the cultural issues worth considering.
How many (latex) papers in “TCS journals” even mention runnable code? (I’d suggest <1%)
Timelessness. It’s a pretty good bet that latex-generated PDF’s in TCS will be viewable in 10-20-50 years mainly because this format already houses so much scientific knowledge. Conversely it’s almost guaranteed that a sufficiently large Mathematica package (e.g. of the sort that might involve some systematic experimentation in TCS) will not be runnable in even 5 years. This of course is not a Mathematica issue per-se (it perhaps handles backward compatibility better than most) but one common to all experimentation since backward compatibility is an order of magnitude greater problem for runnable code compared with static documents. One of the potentially important things about the Demonstration site IMO is that maybe this backward compatibility will end up being managed for you.
This timelessness and cultural issues become relevant to the extent that your code becomes more and more complex and more and more part of your results - which in many ways will be inevitable in any systematic experimentation (if you take the philosophical position about the potential of symbolic manipulation in TCS) that might increasingly be needed to discover something new.
So my take it on using Mathematica systematically in TCS would be:
For “mainly theoretical results” any motivation/checking/illustrations using Mathematica could be beneficial.
Closer and deeper integration between mathematica experimentation and TCS is still a relatively unexplored and potentially fruitful area IMO (- as someone not working in the field) but … most experts in the area would probably disagree and at any rate …
Technically the infrastructure for a larger-scale Latex/Mathematica - theoretical/experimental framework is not sufficiently developed (IMO) to
currently go too far down this path.
Demonstrations might be a step in the right direction and perhaps provide a good litmus test for the level of complexity in terms of symbolic manipulation used in TCS research. If it can be put into a Demonstration your work may have a better chance of gaining some sort of timelessness. Currently Demonstrations are a fair way behind what can be done in a notebook (e.g. integration of packages, input fields, external data sources etc) but IMO this situation may improve over time and particularly if WRI shares this view about the importance of imbuing this timelessness in computational research (perhaps adding package support, Google Play/App Store functionality etc).
Mathematica
when it is not necessary. On the other hand it may be an indispensable tool. $\endgroup$