홈 › Papers

Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints

2026-04-17 · Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens, Mohammad Abdulaziz, Andrei Popescu, Dmitriy Traytel arxiv

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.

📄 PDF Abstract BibTeX arXiv:2604.15713

Code (0)

등록된 구현이 없습니다.

The Isabelle ENIGMA

2022-05-04 · Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák 외

We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of t…

Automated Theorem Proving

AI solutions for drafting in Magic: the Gathering

2020-09-01 · Henry N. Ward, Daniel J. Brooks, Dan Troha, Bobby Mills 외

Drafting in Magic the Gathering is a sub-game within a larger trading card game, where several players progressively build decks by picking cards from a common pool. Drafting poses an interesting problem for game and AI …

Closed Drafting as a Case Study for First-Principle Interpretability, Memory, and Generalizability in Deep Reinforcement Learning

2023-10-31 · Ryan Rezai, Jason Wang

Closed drafting or "pick and pass" is a popular game mechanic where each round players select a card or other playable element from their hand and pass the rest to the next player. In this paper, we establish first-princ…

Decision Making Deep Reinforcement Learning reinforcement-learning Reinforcement Learning (RL)

Munkres' General Topology Autoformalized in Isabelle/HOL

2026-04-08 · Dustin Bryant, Jonathan Julián Huerta y Munive, Cezary Kaliszyk, Josef Urban arxiv

We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Chapters 2--8), from topological spaces th…

Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL

2021-12-11 · Mark Chevallier, Jacques Fleuriot

We present a formalisation of finite Markov decision processes with rewards in the Isabelle theorem prover. We focus on the foundations required for dynamic programming and the use of reinforcement learning agents over s…

reinforcement-learning Reinforcement Learning Reinforcement Learning (RL)