Source-linked AI summary
Proof Interfaces for Exploratory Mathematics
Nishant Kheterpal, Matthew Keenan, Cyrus Omar, Jean-Baptiste Jeannin
TL;DR
Paper and whiteboard mathematics can be tedious and error-prone, while expert tools do not support the open-ended exploratory work described here. The paper extends Hazel Prover with configurable rewrite automation and Rocq proof export; case studies demonstrate supported stepwise tasks while identifying interaction and proof-export limits for complex Taylor work.
Problem
Paper and whiteboard derivations are tedious and error-prone, while computer algebra systems support fixed transformations but not the open-ended exploration needed to bound terms or prove theorems.
Source: §1 · p. 1Method
The paper extends Hazel Prover with profile-controlled rewrite search, multiple levels of automation, and proof export to Rocq.
Source: §1 · p. 2, §3 · p. 2, §3.1 · p. 2Results
Case studies show the interface supporting stepwise arithmetic, completing the square, and trigonometric rewriting, while complex Taylor work incurs high interaction overhead and lacks Rocq export for Taylor remainders.
Source: §4 · pp. 3–4Takeaways & Limitations
The case studies demonstrate a single interface serving educational and exploratory tasks with different step granularity, while exposing boundaries in complex Taylor workflows.
Source: §4 · pp. 3–4Whole-program stepping can increase interaction overhead, and Rocq export does not yet support Taylor remainders.
Source: §4 · p. 4
Abstract
from arXiv · showhide
This paper describes a mathematics interface intended for both educational applications and exploratory mathematics. Both learners and mathematics practitioners often use pen and paper or a whiteboard to perform equational reasoning, manipulate expressions, or construct proofs. These workflows lead to a variety of problems: transcription errors, tedious writing and notation, and/or unclear standards for proof justification. We extend the Hazel Prover, an equational-reasoning interface in the Hazel live programming environment, to add capabilities for exploratory mathematics, with varying levels of verbosity and automation aimed at both students and expert users. Students require more deliberate practice when learning mathematical concepts and correspondingly more verbose justifications, while experts may benefit from significant mathematical automation. With this in mind, our interface supports multiple levels of mathematical automation and simplification, grounded in a rewrite search architecture. For expert users, motivated by a gap in the accessibility of formal methods, we support proof export to the Rocq theorem prover, extending this rewrite search to proof tactics. This paper closes with several case studies covering elementary- to college-level mathematics.
1 Introduction
Exploratory mathematics on paper or whiteboards is tedious and error-prone, while existing tools do not fully support open-ended exploration with incremental correctness. The paper extends Hazel Prover to serve both learners, who need scaffolding and less automation, and experts, who need exploratory work and formal proof export.
1 Introduction
- Whiteboard derivations make rewriting tedious and small sign errors hard to notice, while results must later be transcribed or photographed for sharing.The cited passage gives flipping + to − as an example of an easily missed error.Source: §1 · p. 1
- LaTeX can make copying easy but tedious to write, while computer algebra systems support fixed transformations rather than open-ended exploration or theorem proving.The passage names Mathematica, SymPy, Maple, and MATLAB as examples of computer algebra systems.Source: §1 · p. 1
- Students need deliberate practice and verbose justification, whereas experts need open-ended exploration with incremental correctness and may benefit from greater automation.Students can struggle to break arguments into sufficiently small steps or apply new rules correctly.Source: §1 · p. 1
- The paper extends Hazel Prover for exploratory mathematics, with step derivations that can emit a formal proof.Hazel Prover was previously used in classrooms to teach structural induction proofs [5].Source: §1 · pp. 1–2
- The work aims to lower the formal-methods barrier for applied practitioners such as aerospace engineers and physicists who perform rigorous mathematical reasoning without that training.Examples include deriving equations of motion, linearizing dynamics, and discretizing continuous systems.Source: §1 · p. 1
- Its contributions include customizable rewrite search, proof export to Rocq, and case studies spanning order of operations, algebra, calculus, and exploratory numerical methods.The interface varies mathematical capabilities and automation from single steps to simplification.Source: §1 · p. 2
2 Design Goals
The design goals target a usable interface for both learning exercises and expert exploration. They prioritize minimal setup and interaction overhead, appropriate step size, and support for the symbolic tasks studied.
2 Design Goals
- The interface should let new users start representative tasks with little configuration or theorem-prover-specific training.The goals are informed by prior Hazel Prover work [5, Section 2].Source: §2 · p. 2
- Routine operations such as rewrites, differentiation, and substitution should require few actions.Source: §2 · p. 2
- Users should be able to choose steps neither as large as simplifying a full expression nor as small as only commuting terms.Source: §2 · p. 2
- The interface should cover the symbolic tasks used in the paper’s case studies.Source: §2 · p. 2
3 Architecture
Hazel supports student and expert workflows through rewrite search governed by configurable automation and math profiles. Accepted derivations retain a correctness guarantee and can be exported to Rocq.
3 Architecture
- The architecture lets users select expressions, apply or propose transformations, check permissibility, and record accepted derivations for proof export.After a valid rewrite, users may continue with another step.Source: §3 · p. 2
3.1 Rewrite Search
- One Step requires each proposed result to be reachable by one enabled rewrite, with the profile defining what counts as a step.The mode can support more or less verbose rewrites, depending on the active profile.Source: §3.1 · p. 2
- Check Result accepts a proposed equivalent result only when permitted rewrites can reach it; Suggest Result extends this mode by automatically simplifying the selected subexpression.Mathematical equivalence alone is insufficient if the active profile disables a needed operation such as collecting like terms.Source: §3.1 · p. 2, Figure 2 · p. 3
3.2 Math Profiles and Automation Policy
- Math profiles define enabled rewrites and automation, offer contextually applicable rules, and bound search so a result is accepted only when permitted rewrites reach it.The design envisions increasing automation as students master skills, then unlocking capabilities for new subjects such as trigonometry.Source: §3.2 · pp. 2–3
3.3 Proof Export
- Completed rewrite sequences form structured informal proofs that the interface exports as Rocq proof scripts for machine-checked verification.For more automated modes, a found rewrite sequence is checked by a background JSCoq worker.Source: §3.3 · p. 3
4 Extended Case Studies
The case studies exercise the interface from elementary arithmetic through algebra, trigonometric identities, and Taylor approximation. They show supported stepwise work while exposing interaction overhead and a proof-export boundary for more complex Taylor work.
4 Extended Case Studies
- The case studies progress in complexity across algebra-education-to-calculus tasks, with later studies building on earlier interface capabilities.The simplest studies are intended as teaching tools, while later cases target numerical-methods practitioners.Source: §4 · p. 3
- One Step supports deliberately small arithmetic operations in order-of-operations practice, meeting the stated interaction-overhead and step-granularity goals.The exercise simplifies an arithmetic expression to 17.Source: §4 · p. 3
- Check Result supports completing the square by adding +9−9 before factoring, with steps matching paper work and meeting the stated design goals.The case rewrites x²+6x+5 as (x+3)²−4.Source: §4 · p. 3
- Trigonometric identities can offer multiple valid rewrites for the same subexpression at intermediate steps.Source: §4 · p. 3
- Automatic identity suggestions and simplification reduce the tedium of rewriting trigonometric expressions and keep interaction overhead low.The case targets both precalculus education and numerical-methods practitioners who need to manipulate and verify such derivations.Source: §4 · p. 4
- Taylor approximation of a polynomial is feasible, but whole-program stepping can force users to step a larger program to compute an intermediate derivative.For this polynomial, the step burden remains small; more complex functions can make interaction overhead significant.Source: §4 · p. 4
- The trigonometric Taylor case has high interaction overhead, and unsupported Taylor remainders prevent Rocq proof export and limit mathematical coverage.The passage identifies stepping and substituting subexpressions as changes that would reduce the tedium.Source: §4 · p. 4