Accessible integrated formal reasoning environments in classroom instruction of mathematics

Abstract

Computer science researchers in the programming languages and formal verification communities, among others, have produced a variety of automated assistance and verification tools and techniques for formal reasoning. While there have been notable successes in utilizing these tools on the development of safe and secure software and hardware, these leading-edge advances remain largely underutilized by large populations of potential users that may benefit from them; among these are instructors and students engaged in the undergraduate-level instruction and study of mathematics. Building on earlier work in assembling and evaluating accessible formal verification tools for research and classroom instruction, we have assembled an interactive web-based integrated formal reasoning environment that incorporates several standard techniques developed by the programming languages and formal verification communities. This environment can run entirely within a standard web browser, and provides interactive and instant verification feedback about logical validity, as well as an interactive, exhaustive list of all inferred properties for a given formal argument input. The environment provides an explicit library of logical definitions and formulas that instructors can curate and students can utilize to complete assignments; these formulas can be browsed and filtered by students within the environment. The underlying infrastructure also allows instructors to assemble lecture notes and assignments containing within them formal arguments (including both complete examples and problems to be solved by students) that can be automatically loaded into the environment with one click. This environment has been utilized within the classroom for an undergraduate-level course in linear algebra, both by the instructor in presenting examples during lectures, and by students when completing homework assignments.