Teaching Computer Science Theory Courses with LLM-enhanced Automatic Proof Assistant
Kelin Luo
Project Team- Xiangyu Guo, Assistant Professor of Teaching, Department of Computer Science and Engineering, SUNY at Buffalo; Chong Liu, Assistant Professor, Department of Computer Science, SUNY at Albany
Buffalo (UB)
2025
IITG
$40,300.00
The project integrated LLM-enhanced Lean proof assistants into computer science theory courses across four sections and 237 students, providing students with interactive support for developing and verifying formal proofs. The project also produced openly accessible instructional materials that can support broader adoption of AI-assisted formal reasoning in computer science education.
(1) GitHub repository containing examples, exercises, proof-assistant materials: https://github.com/Lean4CStheory/Lean4CStheory-Exercises.git; (2) Conference presentation: SUNY CIT 2026, "Teaching CS Theory Courses with LLM-Enhanced Automatic Proof Assistants"; (3)Publication and Conference Presentation: ACL 2026, "HintMR: Eliciting Stronger Mathematical Reasoning in Small Language Models" https://arxiv.org/pdf/2604.12229