Currently no, we do not have this. Here are two related things that are also not what you are looking for.
1) Formal proof assistants etc. such as Coq.
2) Proof verifiers in a more informal (though rigorous) sense, such as the open source Lurch.
There are also some 'automatic theorem-discoverers' especially in combinatorics (WZ, or at least I understand it thusly) - for an interesting request for this in Sage, see this CS.SX question.
As to Wilf-Zeilberger creative telescoping, we have now hypergeometric functions in Sage and, regarding the recent more general creative telescoping approach, the ore_algebra package is optional in Sage. A good overview over algorithms needed to make creative telescoping work is the recent Koutschan paper.
I have opened the respective ticket. Please contribute.
It seems that you are asking whether Sage can think. It cannot. We are fortunately still not there. That would be very dangerous for human kind, as has been recently remarked by Stephen Hawking, among other people. There are many people trying to make it happen, though, but it still seems quite far.
Asked: 2014-07-05 13:47:36 +0200
Seen: 1,555 times
Last updated: Jul 09 '14
Copyright Sage, 2010. Some rights reserved under creative commons license. Content on this site is licensed under a Creative Commons Attribution Share Alike 3.0 license.
