Project Name: Polyhymnia: Geometry for the Many
Grantee: John Connor
Discipline: Computer Science
Funding Cycle: 2016-2017
White Paper: john connor – white paper
Students of computer science are very fortunate to have at their disposal static analysis tools and integrated development environments. These tools check work in real time, are always available, and are never mistaken. While it is true that they seldom give insightful feedback, simply knowing that there is a problem is often enough information for the student to find it.
While static analysis is far from perfect, students in other fields are not nearly so fortunate. Spell check is perhaps as close as they will come to computer assistance in their day to day work. My research will help to bridge this gap in one particular area of common core high-school math- ematics education: Euclidean plane-geometry.
We propose to develop a prototype of a proof assistant for elementary geometry. The design goal is to provide an environment suited for high school students (without knowledge of computer science or programming) to write formal geometric constructions and proofs in a high level language, and to receive feedback from the proof assistant about logical errors in their reasoning, along with any appropriate counter examples.