mlsanityData to 7 Oct 2026

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

arXiv 2604.15713 ↗First posted 17 Apr 2026cs.LO cs.AI cs.PLcited by 0

On the map: LLM agents and tool use → Educational agents and math problem solving

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.

Key facts. No citing papers in the map yet (data through 7 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.

Builds on

15 of 52 references.

References · 15

  1. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  2. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  4. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  5. 2025The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofscited by 27
  6. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 18
  7. 2026130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?cited by 16
  8. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 15
  9. 2026Agentic Proof Automation: A Case Studycited by 4
  10. 2018Spine-local Type Inferencecited by 1
  11. 2019Bidirectional Typingcited by 1
  12. 2022A Linter for Isabelle: Implementation and Evaluationcited by 1
3 more
  1. 2025A Formal Analysis of Algorithms for Matroids and Greedoidscited by 1
  2. 2026Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isarcited by 1
  3. 2026Munkres' General Topology Autoformalized in Isabelle/HOLcited by 1

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
  2. 2025L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL ↗
  3. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
  4. 2026Advancing Mathematics Research with AI-Driven Formal Proof Search
  5. 2026Agentic Proving for Program Verification
  6. 2026ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
  7. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
  8. 2026LAMP: Lean-based Agentic framework with MCP and Proof Repair