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/f334026e-a1e7-481d-b561-b70ef873da95n%40googlegroups.com.
