Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.02449

Proof Interfaces for Exploratory Mathematics

Nishant Kheterpal·Matthew Keenan·Cyrus Omar·Jean-Baptiste Jeannin
View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Nishant Kheterpal, Matthew Keenan, Cyrus Omar, Jean-Baptiste Jeannin. 2026-10-01. Proof Interfaces for Exploratory Mathematics. https://arxiv.org/abs/2610.02449

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

WAMpy: Efficient Synthesis of Prolog Programs in Python

We present WAMpy, a Python framework optimized for synthesizing Prolog programs. Unlike general-purpose Prolog systems, WAMpy targets workloads that repeatedly generate and evaluate small candidate programs. WAMpy compiles Prolog clauses into NumPy array-based WAM instructions and supports partial recompilation of hypotheses against fixed background knowledge. Performance-critical routines are accelerated using Numba just-in-time (JIT) compilation. In a benchmark of repeated compilation-and-evaluation workloads, WAMpy improves end-to-end performance compared with SWI-Prolog accessed from Python using Janus.

cs.PL↗
arXiv2026

OpenMP Meta-Lowering: A Declarative Approach to Performance Portable Parallel Code Generation

The increasing diversity of parallel hardware challenges existing compilation flows. While OpenMP provides a portable abstraction for shared-memory parallelism, existing compilers tightly couple the frontend semantics with fixed lowering strategies. This design limits performance portability across different runtimes and architectures. In this paper, we present a modular approach to parallel code generation based on the Multi-Level Intermediate Representation (MLIR) framework. Our approach combines an OpenMP frontend with a domain-specific language (DSL) that specifies how OpenMP constructs are lowered for a target. We call this approach OpenMP meta-lowering, treating lowering as a programmable component rather than compiler-specific logic. This design provides explicit control over code outlining, data sharing, and runtime interfacing across diverse targets. We evaluate our approach on PolyBench/C-OMP across general-purpose and embedded multicore targets. Our results show that the proposed method matches the performance of state-of-the-art compiler toolchains with negligible code-size overhead (< 0.7%). Preserving OpenMP constructs until late lowering stages enables both general-purpose and OpenMP-specific MLIR optimizations. By decoupling lowering from compiler internals, our approach expresses the same OpenMP subset in 5,182 lines of code, ~32% fewer than the corresponding lowering code in Clang and ~76% fewer than in GCC, while supporting the pmsis runtime costs only a few specification lines, enabling rapid support for new runtimes without modifying the compiler.

cs.PL↗
arXiv2026

Bao: Automatic Region Placement and Memory Allocation for Intermittent Computing

Intermittent computing enables batteryless embedded devices to operate in harsh environment, but frequent power failures interrupt program execution and require careful management of state across power cycles. The core challenge is to guarantee both memory consistency and forward progress while minimizing the energy overhead of checkpointing. Recent compile-time approaches identify regions that fit in the energy buffer. At runtime, the device waits and recharges between the regions. However, they still rely on greedy or path-local heuristics that commit to local decisions and can miss globally lower-overhead boundary placements. To address this limitation, we present Bao, a system that jointly finds optimal energy-aware region formation and memory allocation decisions with formal correctness guarantees, by formulating it as a mixed-integer linear program. We prove that any feasible solution guarantees energy safety and implement our approach in LLVM. Our evaluation on 13 benchmarks across 3 capacitor sizes shows that Bao outperforms existing baselines, achieving 10% faster execution and 52% fewer region boundary hits on average compared to the best baseline.

cs.PL↗