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.

翻译：类型注解对于在解析和类型推断下保持项含义的打印至关重要。我们研究了Isabelle中使用的一阶多态λ演算项上完备且最小类型注解的问题。基于Smolka、Blanchette等人先前的工作，我们给出了该问题的元理论阐述，包含完整的形式化规约与证明，并在Isabelle/HOL中对其进行了形式化。我们的开发过程包含一系列实验，展示了人类驱动与AI驱动的形式化工作流程：人类和基于LLM的AI代理独立生成笔算证明，而AI代理将两者自动形式化为Isabelle代码，并通过进一步的人类提示型AI干预来优化和推广该开发成果。