IsarStep converts declarative Isar proofs into sequence-to-sequence examples where a proof fragment has an intermediate proposition removed.
Wenda Li, Lei Yu, Yuhuai Wu and Lawrence C. Paulson introduced IsarStep, a benchmark mined from Isabelle's Archive of Formal Proofs in which models must predict a missing intermediate proposition from surrounding proof context, covering undergraduate- and research-level mathematics and computer science material.
IsarStep converts declarative Isar proofs into sequence-to-sequence examples where a proof fragment has an intermediate proposition removed. The task tests whether a model can reconstruct a semantically useful bridge between surrounding proof states, and the authors evaluated Transformer-based baselines including a hierarchical architecture designed for long proof context.
The benchmark shifted part of learned theorem proving toward human-readable intermediate reasoning over real proof corpora. Together with contemporaneous formal-math pretraining work, it supplied an important pre-LLM testbed for learning reusable mathematical representations and proof steps from mature proof-assistant libraries.
Significance rationale: IsarStep created a large non-synthetic benchmark from human-written Isabelle proofs and focused evaluation on recovering missing intermediate propositions rather than only predicting low-level tactics. It helped establish high-level proof-step generation over real formal mathematics as a distinct learning problem before later language-model theorem-proving systems scaled similar ideas.
—
—
The arXiv research record establishes the IsarStep task, Isabelle-derived dataset and reported neural sequence-model experiments.
The public IsarStep repository exposes the code and links to the released dataset, hierarchical Transformer implementation and test suite. E3 records artifact-level inspectability rather than independent reproduction of every reported result.
No corrections recorded.
