Metadata-Version: 2.4
Name: IsaMini
Version: 0.5.0
Summary: Isabelle/Minilang
Author-email: Qiyuan Xu <xqyww123@gmail.com>
License-Expression: LGPL-2.1-or-later
Project-URL: Homepage, https://github.com/xqyww123/Isa-Mini
Classifier: Programming Language :: Python :: 3
Classifier: Operating System :: OS Independent
Description-Content-Type: text/markdown
License-File: COPYING
License-File: COPYING.LIB
License-File: COPYRIGHT
Requires-Dist: msgpack>=1.1.2
Requires-Dist: isabelle-rpc>=0.4.0
Requires-Dist: Isabelle_Semantic_Embedding>=0.1.0
Requires-Dist: rich
Requires-Dist: PyYAML>=6.0.3
Requires-Dist: platformdirs>=4.9.4
Requires-Dist: jsoncomment>=0.4.2
Requires-Dist: claude-agent-sdk>=0.1.72
Requires-Dist: zstandard>=0.23.0
Requires-Dist: xxhash
Requires-Dist: mcp>=1.26.0
Requires-Dist: uvicorn>=0.41.0
Provides-Extra: repl
Requires-Dist: IsaREPL; extra == "repl"
Provides-Extra: openai-api
Requires-Dist: openai>=2.33.0; extra == "openai-api"
Requires-Dist: httpx>=0.28.1; extra == "openai-api"
Requires-Dist: tiktoken; extra == "openai-api"
Provides-Extra: anthropic
Requires-Dist: anthropic>=0.52.0; extra == "anthropic"
Requires-Dist: httpx>=0.28.1; extra == "anthropic"
Provides-Extra: api
Requires-Dist: IsaMini[anthropic,openai-api]; extra == "api"
Provides-Extra: web
Requires-Dist: aiohttp>=3.13.5; extra == "web"
Provides-Extra: all
Requires-Dist: IsaMini[api,web]; extra == "all"
Dynamic: license-file

Isabelle/Minilang
====

A minimalist proof language for Isabelle/HOL, designed for machine learning and LLM agents.

## News 🎉🎉🎉

We release the **AoA agent**, now the primary interface for proving with
Minilang. AoA is a proof agent built on Minilang, exposed as an ordinary
Isabelle proof method: on any goal in any existing Isabelle context, simply
write `by aoa` and the agent takes over.

```isabelle
theory Scratch
  imports Complex_Main Minilang_AoA.Minilang_AoA
begin
  theorem sqrt2_not_rational: "sqrt 2 ∉ ℚ"
    by aoa
end
```

AoA integrates seamlessly into existing proof developments — no fine-tuned model, no local LLM infrastructure to set up, no changes to your theory files. The agent never edits/touches your Isabelle script: all of its work happens in the background, and its effects are confined to the target proof context (here, the one opened by `sqrt2_not_rational`); outside that context, anything is untouched.

The proof found by `aoa` is saved to a separate file (`scratch.proof-cache` in the example above). Replaying `by aoa` reuses the
stored proof directly — the agent is not re-run and no API cost is incurred — unless the cached proof no longer holds, in which case the agent is automatically invoked again.

Read [AoA User Manual](/IsaMini/AoA/Readme.md) for how to install and other details.

## Key Features

Minilang eliminates the human-oriented complexities of Isabelle/Isar, letting language models focus on high-level proof planning while delegating fine-grained reasoning to classical automation (Sledgehammer & friends). What started as a minimal proof shell has grown into a full stack:

- **Minilang** — a minimalist proof language with only ~10 core operations, each with clear semantic distinctions ([OOPSLA'26 paper](https://dl.acm.org/doi/10.1145/3798275))
- **Translator** — a rule-based Isar → Minilang translator that has converted ~85% of ~340K existing Isabelle/AFP proofs into a large-scale training corpus ([code](https://github.com/xqyww123/Isa-Mini-Translator))
- **AoA Agent** — *Agent over AST*: a token-efficient LLM proof agent that edits Minilang proofs directly as JSON abstract syntax trees, usable from inside Isabelle via a single `by aoa` method ([paper](https://arxiv.org/abs/2607.16372), [code](/IsaMini/AoA), [README](/IsaMini/AoA/Readme.md))

Visit our [Example Gallery](https://docs.google.com/presentation/d/14VY5HkMRmOhRkKBvmISymKtNg5e650EZgzt-KajqMRI/edit?usp=sharing) to see more.

### AoA: Agent over AST

The AoA agent answers a practical question: *how do we cut the prohibitive API cost of LLM proof agents, and how do we let general-purpose LLMs write proofs in a language for which they lack corpus-scale exposure?*

- **AST-native interaction**: instead of emitting source text and re-locating states by line numbers after every edit, the model supplies proofs as JSON representations of Minilang's AST — a format native to tool-calling LLMs — and drives the prover through a tree-edit model.
- **Proof tree = operations + states**: proof operations and proof states are fused into one tree, so each operation carries its own subgoal's state, readable directly off the tree without separate queries.
- **Token- and cost-efficient**: against Amazon's Isabelle Agent on the miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by **2.3–4.7×**, uses **2.9–6.9× fewer tokens** and **3.9–8.9× fewer tool calls**, and finishes **1.4–2.0× faster** — while solving more problems on the harder verification benchmark.
- **No fine-tuning required**: works with general-purpose LLMs out of the box, with drivers for Claude Code, Codex, and OpenAI-compatible / Anthropic APIs.
- **One-line usage inside Isabelle**: invoke the agent on any goal simply with the proof method `by aoa`.

See the paper: [*Theorem-Proving Agent over Abstract Syntax Tree of Redesigned Language*](https://arxiv.org/abs/2607.16372).

### Proven effectiveness of Minilang for Neural Theorem Proving

Fine-tuning LLMs on the Minilang corpus (instead of raw Isar) improves the pass@1 success rate on the PISA benchmark by up to **20/29 percentage points** compared to Isar-based models with/without Sledgehammer:

- **pass@1 reaches 69.1%**, exceeding Baldur's pass@64 (65.7%)
- **pass@8 reaches 79.2%**, exceeding the previous SOTA on PISA (71.0%, Magnushammer)

See the paper: [*A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL*](https://arxiv.org/abs/2507.18885).

### The corpus & translator

- Rule-based translation from Isar to Minilang via three strategies: *elaboration* (make implicit information explicit), *normalization* (consolidate diverse idioms into uniform representations), and *elimination of tactics* (replace tactics with Sledgehammer\*, except those matching informal reasoning).
- **~290K proofs** (85.25% of ~340K Isar proofs from Isabelle/AFP) successfully translated, forming one of the largest structured proof corpora for machine learning. Available on [Hugging Face](https://huggingface.co/datasets/ANTPG/Minilang-AFP-v1).


## Citation

If you use Minilang or this repository, please cite:

```bibtex
@misc{xu2026aoatheoremprovingagent,
    title={AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language}, 
    author={Qiyuan Xu and Joshua Ong Jun Leang and Renxi Wang and Wenda Li and Haonan Li and Luke Ong and Conrad Watt},
    year={2026},
    eprint={2607.16372},
    archivePrefix={arXiv},
    primaryClass={cs.SE},
    url={https://arxiv.org/abs/2607.16372}, 
}

@article{10.1145/3798275,
    author = {Xu, Qiyuan and Wang, Renxi and Wang, Peixin and Li, Haonan and Watt, Conrad},
    title = {A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL},
    year = {2026},
    issue_date = {April 2026},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    volume = {10},
    number = {OOPSLA1},
    url = {https://doi.org/10.1145/3798275},
    doi = {10.1145/3798275},
    month = apr,
    articleno = {167},
    numpages = {26},
    keywords = {Interactive Theorem Proving, Isabelle/HOL, Large Language Models, Neural Theorem Proving, Proof Language Design}
}
```
