Agents
Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
arXiv:2604.15713v1 Announce Type: 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 c
arXiv:2604.15713v1 Announce Type: 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 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.
Related
- CascadeDebate: Multi-Agent Deliberation for Cost-Aware LLM Cascades
- The Art of Building Verifiers for Computer Use Agents
- From Helpful to Trustworthy: LLM Agents for Pair Programming
- ClawGUI: A Unified Framework for Training, Evaluating, and Deploying GUI Agents
Source: arXiv cs.AI | 2026-04-20