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 驱动形式化工作流：人类和基于大语言模型的 AI 代理独立完成纸笔证明，AI 代理则在 Isabelle 中自动形式化这两部分，进一步结合人类提示的 AI 干预来优化和泛化该工作。