On Monday, September 30, 2013 11:42:43 PM UTC-7, Keshav Kini wrote: > > > > But as far as I know, Sage is not proof-aware in any way.
Why would you necessarily know about this? I am well aware that Maxima, a component of Sage, has been used to generate proofs. I assume it is not the only component used in this way. As for whether anyone has tried to prove that parts of Sage are correct -- that might be of interest. > I've never > heard theorem-proving people talk about making use of existing computer > algebra systems and I can't imagine how they could be useful in the > business of well-founded theorem proving when they are themselves not > verified. I guess you are not listening to the right theorem-proving people. > If any CAS were to be used in such an endeavour I imagine it > would be something with a more principled code structure than Sage, like > Axiom. And indeed, Wikipedia tells me that there are plans to formalize > Axiom in Coq or ACL2. > That would be a challenge. > > But the above is just "as far as I know". > My experience with theorem > proving is mainly from the CS / PLT perspective, and I've never heard of > MKM so clearly I don't have a sufficiently broad view of the subject. > I'll endeavor to further edify myself. > Google is your friend. > > To return to my question, you mentioned Sage specifically as an example > of a problem and a solution. I was wondering what you meant by that -- > do you see Sage as posing and/or solving some particular theorem proving > -related problem? > I think you could spend some time with the Google... But if you need a particular pointer ... It has been shown that certain geometry theorem proofs can be reduced to algebra, http://en.wikipedia.org/wiki/Wu%27s_method_of_characteristic_set for some people the most prominent example among many connections between computer algebra and proofs. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at http://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/groups/opt_out.
