On Sunday, February 11, 2024 at 7:10:59 AM UTC-8 mmarco wrote: if i understand what you mean correctly, 1) would go along making it easier from the sage part to implement tactics like polyrith (which right now calls the sagecell server to prove equalities between expressions using groebner basis)?
Yes. In particular I would like to not depend on an internet connection, and an online service, to do that kind of thing. Exactly, which is another motivation for improving the usability of Sage as a library (-> modularization, pip-installability). Are there other cases where similar things could be done (that is, concrete computations in Sagemath that could be used as certificates for Lean proofs)? Yes, this is natural and well understood in polyhedral geometry (where Sage has excellent facilities), linear optimization (where Sage has reasonable interfaces) and its extensions, and graph theory / algebraic topology. More generally, the prospect of uses in Lean could inspire developing a style of computation in Sage where not only an answer is computed but also (ideally at low extra cost) a certificate that allows users to check the answer. We have that for some true/false computations (methods of the form "is_...(..., certificate=True)") but not very much for other computations. -- 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 view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/f3e422dc-6702-4760-be5a-ed9d24bb326fn%40googlegroups.com.
