So, 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)?
That sounds very nice. In particular I would like to not depend on an internet connection, and an online service, to do that kind of thing. 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)? El sábado, 10 de febrero de 2024 a las 20:12:00 UTC+1, Matthias Koeppe escribió: > Hi Miguel, > There's of course a large scope of work that can be meaningful. I'll just > mention two directions, but I'll be happy to have a broader and/or more > detailed conversation. > 1. For interactive proof assistants/theorem provers such as LEAN, it can > be powerful to make CAS capabilities available, in particular on the proof > tactics and user interface levels. A first example of using Sage in this > way (basically as an interface to Singular's Gröbner bases) showed up in > LEAN / mathlib in 2022, see links in > https://github.com/sagemath/sage/issues/34180 > 2. There is an interesting opportunity to improve the Sage reference > manual by cross-referencing mathlib (or mathematical libraries of other > theorem provers); for example and perhaps starting with sage.categories. In > contrast to just linking to a Wikipedia page for a definition, this could > be doctested and roundtripped. > > Matthias > > On Saturday, February 10, 2024 at 8:50:42 AM UTC-8 mmarco wrote: > > One question, Matthias: I see that you have proposed a project involving > integration with proof assistants/theorem provers. Just out of curiosity: > how do you envision such integration? > > On Sunday, February 4, 2024 at 7:19:44 AM UTC+9 Matthias Koeppe wrote: > > To get the process started for this year, I have created the page > https://wiki.sagemath.org/GSoC/2024 by copying last year's page, removing > a completed project and adding a new project that I hope to mentor this > summer. > > > -- 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/36e8b2da-0814-4956-a315-0acb4fc926fdn%40googlegroups.com.
