Google Summer of Code: Organization application deadline Feb 6!

[Matthias Koeppe]

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.

The deadline for our project to apply as a GSoC mentoring organization is rapidly approaching: https://developers.google.com/open-source/gsoc/timeline#february_6_-_1800_utc

Do we have any volunteers for the administrator role?

[Travis Scrimshaw]

Thank you for doing that. I updated my projects and removed all of those with named mentors as they have not agreed at present (AFAIK) to be a potential mentor.

I was expecting to be the main administrator for GSoC again this year. We will discuss this on the mentors list.

For the proposal, what we need from the community is a list of projects they are willing to mentor. There is no commitment at this time. However, it is important for our GSoC proposal that it contains a list of new projects each year.

Best,

Travis

[Travis Scrimshaw]

For the potential projects, you can either edit the corresponding wiki page in Matthias's link or directly post them here (you do not need to be the mentor).

Also, I would like to have a list of potential mentors. Any SageMath developer can be a mentor for a GSoC project; so if you are willing to be a mentor (typically just a few hours a week), please directly email me, post it here, or put your name down as a project mentor. (You do not need to have a specific project in mind either.)

Best,
Travis

[Travis Scrimshaw]

Sorry for the multiple messages.

For potential mentors, there is no commitment required at this time.

You can also decide later to add a project and/or be a mentor.

Best,
Travis

[Martin R]

I would like to propose the exact same project I had for last year again, but I am currently at a conference and additionally don't see how I could edit the page.

Martin

[Travis Scrimshaw]

I have added it. (For reference on editing the pages, you login using your trac credentials from the upper left corner.)

Best,

Travis

[Linden Disney]

I have a proposal for a project I would be willing to mentor (detailed below for completeness), but I'm unsure about how best to estimate the length (I did GSoC 2021 but estimates of length weren't around then). The initial coding would not be too challenging, but the mathematical research which is within scope may be harder (but certainly more interesting). 

Title: Poincare normal form of Riemann matrices.

Areas: Algebra, Algebraic Geometry.

Skills: Knowledge of abstract algebra and Riemann surfaces desirable. 

Length: ? 

Difficulty: Medium-Easy, becoming harder if desired by tackling the research questions. 

Description: Riemann surfaces are key objects in many areas of maths, from mathematical physics to algebraic and arithmetic geometry, with modern usage of Sage typically focusing around computing the Riemann matrix and calculating the associated theta function. The project would involve an implementation of Poincare reduction of the Riemann matrix which allows the theta function to be factorised, following the paper of Martens (http://www.jstor.org/stable/43737152), which in turn will require some matrix methods to be implemented. There is scope for an enterprising applicant to make this into a research paper in two directions, either by analysing the improvement to complexity from computing with factorised theta functions, or by developing an algorithm to go from one reduction to a complete reduction. 

[Travis Scrimshaw]

Hi Linden,

   Thank you. I added the project at the "standard" length 350 hours.

Best,
Travis

[Travis Scrimshaw]

Hi everyone,

   I have submitted the application.

However, we can continue to add projects (and mentors) at any point. So if you are interested or have any features that you want to request, please either add it to the wiki page, post it here, or email me.

Best,

Travis

[Matthias Koeppe]

Great, thanks a lot, Travis, also for taking on the role of the GSoC admin for another year!

[mmarco]

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?

[Matthias Koeppe]

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:

[mmarco]

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)?

[Matthias Koeppe]

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.

[Travis Scrimshaw]

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