More Like this

1. Differences in Students’ Beliefs and Knowledge Regarding Mathematical Proof: Comparing Novice and Experienced Provers

   Ruiz, S. ; Roh, K. H. ; Dawkins, P. C. ; Eckman, D. ; Tucci, A. ( August 2023 , Proceedings of the Annual Conference on Research in Undergraduate Mathematics Education)

   Cook, S. ; Katz, B. ; Moore-Russo D. (Ed.)

   Learning to interpret proofs is an important milepost in the maturity and development of students of higher mathematics. A key learning objective in proof-based courses is to discern whether a given proof is a valid justification of its underlying claim. In this study, we presented students with conditional statements and associated proofs and asked them to determine whether the proofs proved the statements and to explain their reasoning. Prior studies have found that inexperienced provers often accept the proof of a statement’s converse and reject proofs by contraposition, which are both erroneous determinations. Our study contributes to the literature by corroborating these findings and suggesting a connection between students’ reading comprehension and proof validation behaviors and their beliefs about mathematical proof and mathematical knowledge base. 

   more » « less
2. Coherence for bicategories, lax functors, and shadows

   Cary Malkiewich ; Kate Ponto ( January 2022 , Theory and applications of categories)

   Coherence theorems are fundamental to how we think about monoidal categories and their generalizations. In this paper we revisit Mac Lane's original proof of coherence for monoidal categories using the Grothendieck construction. This perspective makes the approach of Mac Lane's proof very amenable to generalization. We use the technique to give efficient proofs of many standard coherence theorems and new coherence results for bicategories with shadow and for their functors. 

   more » « less
3. Coherence for bicategories, lax functors, and shadows

   Malkiewich, Cary ; Ponto, Kate ( February 2022 , Theory and applications of categories)

   Shulman, Michael (Ed.)

   Coherence theorems are fundamental to how we think about monoidal categories and their generalizations. In this paper we revisit Mac Lane's original proof of coherence for monoidal categories using the Grothendieck construction. This perspective makes the approach of Mac Lane's proof very amenable to generalization. We use the technique to give efficient proofs of many standard coherence theorems and new coherence results for bicategories with shadow and for their functors. 

   more » « less
4. QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning

   Sanchez-Stern, Alex ; Varghese, Abhishek ; Kaufman, Zhanna ; Zhang, Dylan ; Ringer, Talia ; Brun, Yuriy ( April 2025 , IEEE)

   Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding a search through the proof space using a theorem prover. Unfortunately, the theorem prover provides only the crudest estimate of progress, resulting in effectively undirected search. To address this problem, we create QEDCartographer, an automated proof-synthesis tool that combines supervised and reinforcement learning to more effectively explore the proof space. QEDCartographer incorporates the proofs' branching structure, enabling reward-free search and overcoming the sparse reward problem inherent to formal verification. We evaluate QEDCartographer using the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects. QEDCartographer fully automatically proves 21.4% of the test-set theorems. Previous search-based proof-synthesis tools Tok, Tac, ASTactic, Passport, and Proverbot9001, which rely only on supervised learning, prove 9.6%, 9.8%, 10.9%, 12.5%, and 19.8%, respectively. Diva, which combines 62 tools, proves 19.2%. Comparing to the most effective prior tool, Proverbot9001, QEDCartographer produces 26% shorter proofs 27% faster, on average over the theorems both tools prove. Together, QEDCartographer and non-learning-based CoqHammer prove 31.8% of the theorems, while CoqHammer alone proves 26.6%. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools' search mechanisms. 

   more » « less
5. Instructional interventions and teacher moves to support student learning of logical principles in mathematical contexts

   Roh, K.H. ; Dawkins, P.C. ; Eckman, D. ; Tucci, A. ; Ruiz, S. ( August 2023 , Proceedings of the Annual Conference on Research in Undergraduate Mathematics Education)

   Cook, S. ; Katz, B. ; Moore-Russo, D. (Ed.)

   This study explores how instructional interventions and teacher moves might support students’ learning of logic in mathematical contexts. We conducted an exploratory teaching experiment with a pair of undergraduate students to leverage set-based reasoning for proofs of conditional statements. The students initially displayed a lack of knowledge of contrapositive equivalence and converse independence in validating if a given proof-text proves a given theorem. However, they came to conceive of these logical principles as the teaching experiment progressed. We will discuss how our instructional interventions played a critical role in facilitating students’ joint reflection and modification of their reasoning about contrapositive equivalence and converse independence in reading proofs. 

   more » « less