Isa-Mini: A Minimal Proof Language for AI Agents Built on Isabelle/HOL

Isa-Mini is a minimal language for Isabelle/HOL designed specifically for AI agents. It simplifies Isabelle's dozens of commands and strategies into fewer than 10 core proof instructions, allowing AI to focus on macro proof path planning while leaving tedious detail proofs to automated tools like Sledgehammer.

Isabelle/HOL is a powerful interactive theorem prover with rich features optimized for human interaction (e.g., Isar language, diverse commands like have/hence/show, strategies like simp/auto). However, these features create unnecessary cognitive burden for AI agents—too many command choices and complex syntax rules become efficiency bottlenecks. Isa-Mini addresses this by retaining Isabelle's strength while providing an AI-friendly minimal interface.

Core Design Philosophy: Let AI focus on macro proof path planning; delegate trivial proofs to automation. Key Features:

1. Minimal interface: <10 core commands (CRUSH, HAVE, OBTAIN, LET etc.)
2. Textual standard I/O: JSON format for easy AI parsing/generation
3. Concurrency support: Utilize Isabelle's thread scheduler for multi-branch proofing
4. State management: Allow restoring historical proof states for path backtracking
5. Bidirectional channel: Reserve interface for future Isabelle-AI collaboration

Take the proof of 'sqrt 2 is irrational' as an example:

• Traditional Isabelle Proof: Requires precise selection of strategies (rule, auto, fastforce, simp) and parameters.
• Isa-Mini Proof: Uses simple commands like HAVE/OBTAIN; all small proof steps are automatically handled by Sledgehammer. AI only needs to describe the macro structure (introduce variables, establish intermediate conclusions). This shows Isa-Mini's simplicity and focus on macro planning.

Isa-Mini has been applied in practice: the team successfully translated ~260,000 proofs from the Archive of Formal Proofs (AFP) into Isa-Mini format. This demonstrates the language's sufficient expressiveness for complex mathematical arguments and the feasibility of automated translation, lowering AI's barrier to using formal tools.

Significance: Isa-Mini represents a trend of making human-designed formal tools accessible to AI. Future Outlook:

• Extend to other formal tools (Coq, Lean) with similar adaptation layers.
• Enable closer human-AI collaboration: AI proposes proof strategies/sketches, humans supervise key decisions, Isabelle verifies correctness.

Isa-Mini simplifies Isabelle/HOL's commands to <10 core instructions for AI agents, focusing on macro proof planning and automating details. Its practical value is proven by the AFP translation achievement. For researchers in AI+formal verification, Isa-Mini provides a valuable tool direction and a reference for adapting other formal tools to AI.