SageMath GSoC 2024 Theorem Prover Proposal

[Atticus Kuhn]

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

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

[Atticus Kuhn]

Dear All,

I am sorry for not completely filling out the proposal before. I have added more details and lengthened my proposal. 

Sincerely,

Atticus Kuhn