> > I'm looking for formal outputs that are not calculated as a human can do > (this is for a free french "book"). Do you know such kind of examples ?
Like Simon, I'm no sure if this is what you mean, but Bruno Buchberger was for a while working on a proof-generating system called *Theorema,* and he used to show "human-readable" proofs it generated for common theorem(s) (not sure about the plural, but there was at least one) which he could not find elsewhere in the literature. You might want to look up that work of his. john perry -- You received this message because you are subscribed to the Google Groups "sage-support" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-support+unsubscr...@googlegroups.com. To post to this group, send email to sage-support@googlegroups.com. Visit this group at http://groups.google.com/group/sage-support. For more options, visit https://groups.google.com/d/optout.