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 show that a reverse-greedy approach leads to a locally minimal and complete set of annotations.
Our development is a series of experiments featuring human-driven and AI-driven formalization workflows: a human and an AI agent independently produce pen-and-paper proofs, and the agent autoformalizes them in Isabelle.
We refined the resulting AI proof developments for this AFP submission, the original version and our experimental setup can be found in the related Zenodo entry.
We give a metatheoretical account of the problem, with a full formal specification and proofs in our paper "Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints".
License
Note
Generative AI (Claude Opus 4.6 via I/Q) was used to develop an initial version of the Isabelle theories. Subsequently, we checked all definitions manually and refactored the development before submitting it to the AFP.
Topics
Related publications
- Blanchette, J. C., Böhme, S., Fleury, M., Smolka, S. J., & Steckermeier, A. (2015). Semi-intelligible Isar Proofs from Machine-Generated Proofs. Journal of Automated Reasoning, 56(2), 155–200. https://doi.org/10.1007/s10817-015-9335-3
- Kappelmann, K., Schäffeler, M., Stevens, L., Abdulaziz, M., Popescu, A., & Traytel, D. (2026). Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints (Version 3). arXiv. https://doi.org/10.48550/ARXIV.2604.15713
- Kappelmann, K., Schäffeler, M., Stevens, L., Abdulaziz, M., Popescu, A., & Traytel, D. (2026). Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints [Dataset]. Zenodo. https://doi.org/10.5281/ZENODO.19406624