Advancing Methods for Analyzing Mathematical Proof Language

This project aims to serve the national interest by studying the language conventions used in formal mathematical proof using scalable, artificial intelligence-based approaches. Many advanced undergraduate mathematics courses focus on the reading and writing of mathematical proofs. This transition from primarily computation-based mathematics to formal proving is often a substantial barrier for students. One reason for this struggle is that formal mathematical proof uses an idiosyncratic and precise set of language conventions. Yet, the nature of these conventions is understudied, especially at scale, and students receive little explicit instruction on them. The goal of this project, Advancing Methods for Analyzing Proof Language (AMPL), is to identify these conventions using large corpora of proof writing from mathematicians (collected from publications and textbooks) and a corpus of student proof attempts (collected from undergraduate classes and online). This provides a means to identify conventions and characterize places where student conventions might differ from expert convention allowing for more targeted instruction. The results will help instructors make proof expectations more transparent. The products will be openly available to researchers and educators supporting the long-term goal of improving access to proof-based mathematics. The AMPL project will consist of several phases. First, we will build two new educational corpora: undergraduate textbook proofs and undergraduate student proof attempts. These corpora will be prepared for analysis by isolating proofs from surrounding narrative and identifying student proof attempts. Additionally, we will make use of an existing corpus of mathematician publications. The next phase involves analysis to identify linguistic conventions which we call proof-language markers. We will combine qualitative human coding, weak supervision, semantic embeddings, and transformer-based language models to identify the markers, develop a codebook, and reproducible computational methods for identifying proof-language markers. After this iterative process, we will conduct cross-corpus analyses of research articles, textbooks, and student proof attempts to identify how student proof language aligns with and diverges from disciplinary conventions. The project team will disseminate openly available instructor inventories and proof-language resources along with making corpora, codebooks, and models public. These efforts will establish the first large-scale empirical description of proof-language conventions across research, textbook, and undergraduate proof writing while providing reproducible methods for studying disciplinary language. This project is supported by NSF’s EDU Core Research (ECR) program. The ECR program emphasizes fundamental STEM education research that generates foundational knowledge in the field. Investments are made in critical areas that are essential, broad and enduring. 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.