This project leverages Large Language Models (LLMs) to integrate programming proof assistants like Lean or Coq into CS theory courses, such as Data Structures, Algorithms, and Complexity. These courses emphasize theoretical rigor, making abstract concepts challenging for students. Proof assistants allow expressing mathematical proofs as programs, enhancing comprehension and enabling automatic verification. However, they are rarely used in teaching due to the manual effort required. With LLMs now capable of generating programs from proofs, we aim to streamline this process.
Our project will design curriculums that guide students to utilize LLM-supported proof assistants to study theoretical topics. Automated proof verification will support self-assessment and help instructors refine teaching strategies. Additionally, we will develop a proof assistant library covering core concepts taught in CS theory courses, filling a longstanding gap in CS education. This initiative will make proof assistants more accessible, fostering independent learning and benefiting the broader academic community.

Project currently ongoing