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

TL;DR

This paper explores how AI agents and humans can collaboratively generate, refine, and generalize formal proofs in Isabelle using minimal type annotations, supported by formal proofs and experiments.

Contribution

It provides a formal specification and proofs for minimal type annotations in Isabelle, integrating human and AI-driven formalization workflows.

Findings

AI agents can independently produce formal proofs in Isabelle.

Human hints improve AI formalization and generalization.

The approach is supported by formal proofs and experimental validation.

Abstract

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 $\lambda$-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.