Ask Your Question

Does sage have facilities to help prove theorems?

asked 2014-07-05 06:47:36 -0500

ensaba gravatar image

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.

edit retag flag offensive close merge delete

3 answers

Sort by ยป oldest newest most voted

answered 2014-07-05 20:54:07 -0500

kcrisman gravatar image

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.

edit flag offensive delete link more

answered 2014-07-05 23:49:50 -0500

updated 2014-07-09 09:30:28 -0500

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.

edit flag offensive delete link more

answered 2014-07-05 16:24:13 -0500

Zatrapadoo gravatar image

updated 2014-07-05 16:25:07 -0500

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.

edit flag offensive delete link more

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

1 follower


Asked: 2014-07-05 06:47:36 -0500

Seen: 230 times

Last updated: Jul 09 '14