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

arXiv:2604.15713v1 Announce Type: cross 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...