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干预来完善和推广该开发。