Collaborative Research: FMitF: Track III: Proof assistants in discrete mathematics education

Proof assistants---programming languages for the writing of mathematical proofs and interactive environments that check the correctness of proofs in these languages as users write them---have become increasingly user-friendly in the last two decades. It is now realistic to teach them to undergraduate students at the time of their first encounter with mathematical proofs.

Since 2023, the investigators have taught discrete mathematics courses to computer science and mathematics undergraduates at Brown University and Fordham University using the proof assistant Lean; their course materials have already been adopted at several other institutions. This project’s novelties are the extension of these course materials to cover new topics, including combinatorics and probability; the development of infrastructure to allow other instructors more flexibility in reusing their materials; the creation and maintenance of an open repository of automation in Lean specialized to the needs of teaching; and the hosting of workshops for the sharing of ideas and the dissemination of best practices.

The project’s impacts are that the cost of entry to teaching mathematics with a proof assistant is greatly lowered: many students, especially at institutions without formal methods expertise, will have access to tools that inform them of their errors and omissions in real time with a chance to correct them. These students will simultaneously gain experience with formal methods.

An essential part of teaching mathematics with a proof assistant is developing a controlled, limited language for interaction with a particular topic. To this end, the investigators are developing a library of pedagogical tactics. Some of these are domain-specific automation, while others are general-purpose or are variants of existing automation.

The domain-specific tactics focus on combinatorics and probability, two subject areas that are not covered in the investigators’ previous course materials; alongside the tactics, the investigators are creating examples and exercises on these topics. The course materials are organized in a way that instructors can mix or reorder the topics covered with automated assistance and checks.

Course infrastructure tools, including autograders and linters, are included in the work package and made openly available to other instructors.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.