# Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 15 of its 52 references that are in the map.
- First posted on arXiv 17 Apr 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 15 of 15)

- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [Agentic Proof Automation: A Case Study](https://mlsanity.com/paper/2601.03768/) (2026)
- [Spine-local Type Inference](https://mlsanity.com/paper/1805.10383/) (2018)
- [Bidirectional Typing](https://mlsanity.com/paper/1908.05839/) (2019)
- [A Linter for Isabelle: Implementation and Evaluation](https://mlsanity.com/paper/2207.10424/) (2022)
- [A Formal Analysis of Algorithms for Matroids and Greedoids](https://mlsanity.com/paper/2505.19816/) (2025)
- [Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar](https://mlsanity.com/paper/2603.07771/) (2026)
- [Munkres' General Topology Autoformalized in Isabelle/HOL](https://mlsanity.com/paper/2604.07455/) (2026)

## Abstract (arXiv)

Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annotations for rank-one polymorphic λ-calculus terms, as used in Isabelle. Building on prior work by Smolka, Blanchette et al., we give a metatheoretical account of the problem, with a full formal specification and proofs, and formalize it in Isabelle/HOL. Our development is a series of experiments featuring human-driven and AI-driven formalization workflows: a human and an LLM-powered AI agent independently produce pen-and-paper proofs, and the AI agent autoformalizes both in Isabelle, with further human-hinted AI interventions refining and generalizing the development.