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

ArXi:2604.15713v1 Announce Type: cross 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, we give a metatheoretical account of the problem, with a full formal specification and proofs, and formalize it in Isabelle