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 <https://www.math.ucdavis.edu/~mkoeppe/>
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
--
You received this message because you are subscribed to the Google Groups
"sage-gsoc" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to sage-gsoc+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/sage-gsoc/6d42d538-7769-42d6-a082-4ce09634e946%40gmail.com.
