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

Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints arXiv:2604.15713v2 Announce Type: replace-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 Isabelle. Building on prior work by Smolka, Blanchette et al., we give a metatheoretical account of