# Hammering Higher Order Set Theory

arXiv: https://arxiv.org/abs/2509.08264 · HTML: https://mlsanity.com/paper/2509.08264/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Sep 2025.

## Built on by (most cited first, 3 of 3)

- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents](https://mlsanity.com/paper/2603.06737/) (2026)
- [Munkres' General Topology Autoformalized in Isabelle/HOL](https://mlsanity.com/paper/2604.07455/) (2026)

## Abstract (arXiv)

We use automated theorem provers to significantly shorten a formal development in higher order set theory. The development includes many standard theorems such as the fundamental theorem of arithmetic and irrationality of square root of two. Higher order automated theorem provers are particularly useful here, since the underlying framework of higher order set theory coincides with the classical extensional higher order logic of (most) higher order automated theorem provers, so no significant translation or encoding is required. Additionally, many subgoals are first order and so first order automated provers often suffice. We compare the performance of different provers on the subgoals generated from the development. We also discuss possibilities for proof reconstruction, i.e., obtaining formal proof terms when an automated theorem prover claims to have proven the subgoal.