Miguel, can you add the project to the wiki page (or tell me the information here), even if it is not fully prepared? It will help increase our chances of being selected for GSoC again.
For everyone, there is a new 90 hour option for GSoC project lengths this year. Best, Travis On Monday, February 12, 2024 at 3:36:12 AM UTC+9 Matthias Koeppe wrote: > 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/dddc6923-8cab-4e2b-ae75-8639b1e909b1n%40googlegroups.com.
