Dear All, I am interested in the following idea from the ideas list:
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 As this proposal is somewhat vague, I began to write up what I interpreted this as, which was to have certain SageMath funcitons return Lean4 Expressions for use in Lean Proofs. I attached my work so far below. I would just like to ask if I am on the right track, or if this idea is too ambitious. 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/426fcbf7-0433-4921-a4ee-3b456c35ec75n%40googlegroups.com.
sagemath_gsoc_2024_proposal.pdf
Description: Adobe PDF document
