ASKSAGE: Sage Q&A Forum - Individual question feedhttps://ask.sagemath.org/questions/Q&A Forum for SageenCopyright Sage, 2010. Some rights reserved under creative commons license.Sat, 05 Jul 2014 23:49:50 -0500Does sage have facilities to help prove theorems?https://ask.sagemath.org/question/23222/does-sage-have-facilities-to-help-prove-theorems/ Does sage have modules that assist with proving theorems? Example, we give a few axioms and then a statement we want to prove. Then sage will list the formal proof.Sat, 05 Jul 2014 06:47:36 -0500https://ask.sagemath.org/question/23222/does-sage-have-facilities-to-help-prove-theorems/Answer by kcrisman for <p>Does sage have modules that assist with proving theorems? Example, we give a few axioms and then a statement we want to prove. Then sage will list the formal proof.</p>
https://ask.sagemath.org/question/23222/does-sage-have-facilities-to-help-prove-theorems/?answer=23236#post-id-23236Currently 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](http://coq.inria.fr/).
2) Proof verifiers in a more informal (though rigorous) sense, such as the open source [Lurch](http://lurch.sourceforge.net/).
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](http://cstheory.stackexchange.com/questions/11126/implementation-of-wilf-zeilberger-and-related-methods).Sat, 05 Jul 2014 20:54:07 -0500https://ask.sagemath.org/question/23222/does-sage-have-facilities-to-help-prove-theorems/?answer=23236#post-id-23236Answer by rws for <p>Does sage have modules that assist with proving theorems? Example, we give a few axioms and then a statement we want to prove. Then sage will list the formal proof.</p>
https://ask.sagemath.org/question/23222/does-sage-have-facilities-to-help-prove-theorems/?answer=23238#post-id-23238As 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](http://scholar.google.de/scholar?cluster=17949238727215932881&hl=en&as_sdt=0,5&as_ylo=2010).
I have opened the [respective ticket](http://trac.sagemath.org/ticket/16636). Please contribute.Sat, 05 Jul 2014 23:49:50 -0500https://ask.sagemath.org/question/23222/does-sage-have-facilities-to-help-prove-theorems/?answer=23238#post-id-23238Answer by Zatrapadoo for <p>Does sage have modules that assist with proving theorems? Example, we give a few axioms and then a statement we want to prove. Then sage will list the formal proof.</p>
https://ask.sagemath.org/question/23222/does-sage-have-facilities-to-help-prove-theorems/?answer=23231#post-id-23231It 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.Sat, 05 Jul 2014 16:24:13 -0500https://ask.sagemath.org/question/23222/does-sage-have-facilities-to-help-prove-theorems/?answer=23231#post-id-23231