Clarification about SageMath GSoC Proof Assistant Project.

[Atticus Kuhn]

Dear all (and Professor Koeppe),

I am interested in the following project for Google Summer of Code (GSoC) 2024 (from the ideas page):

Integration of Sage with proof assistants / theorem provers / SMT systems / constraint programming systems

Mentor	Matthias Köppe
Area	Various
Skills	Solid knowledge of a system such as LEAN, Isabelle, CVC5, MiniZinc; Python experience
Length	350 hours
Difficulty	Hard

but I would like to ask for clarification as to exactly what this project will be about. For example, a proof assistant such as Lean is different from an SMT solver such as CVC5. As far as I see it, there are 2 possible ways that Sage could

be integrated with the above technologies:

1. Add a constraint solving to SageMath, with an interface similar to Z3.py
2. Add a theorem-proving interface to SageMath, with interactive theorem proving capabilities like Lean or Isabelle.

The main distinction in the technologies listed in the original listing is that Lean and Isabelle verify that user-generated proofs are valid, whereas CVC5 and MiniZinc automatically generate their own proofs. I believe that the original intention of the project is probably more similar to #1 than #2, but I would just like to ask for some clarification as to exactly what is envisioned by this idea, as the original ideas page seemed a bit sparse on details.

Also, I apologise for sending this email twice, but it was denied the first time as I was not a member of the Google Group.

Sincerely,

Atticus Kuhn