Aesop is a proof automation tactic for Lean 4, designed to automate the process of finding proofs for mathematical theorems. It targets Lean 4 users, from researchers to power users, aiming to significantly reduce the manual effort required in formalizing mathematics by providing a flexible and extensible automation framework.

How It Works

Aesop operates by building a search tree of potential proof steps. Users define "rules" (which can be arbitrary Lean tactics) and tag them with an @[aesop] attribute. Aesop normalizes the initial goal using a customizable set of rules (including simp_all), then recursively applies registered rules to generated subgoals. Rules can be marked as "safe" (applied eagerly, no backtracking) or "unsafe" (backtrackable, with a user-assigned success probability to guide the search). This best-first search strategy prioritizes more promising proof paths, making it efficient even with large rule sets.

Quick Start & Requirements

• Install via lake build after adding aesop from git "https://github.com/leanprover-community/aesop" to your lakefile.lean.
• Requires matching Lean 4 toolchain versions for Aesop and its dependencies (e.g., std4).
• Example usage: import Aesop; example : α → α := by aesop.
• Official documentation and examples are available in the repository.

Highlighted Details

• Supports custom rule builders (apply, forward, destruct, constructors, cases, simp, unfold, tactic).
• Generates proof scripts (aesop?) for manual inspection and optimization.
• Integrates with Lean's simp tactic for normalization.
• Allows fine-grained control over search strategy and rule application order via priorities and success probabilities.

Maintenance & Community

• Actively maintained by the Lean prover community, with Jannis Limperg as a primary contact.
• Questions and contributions are welcomed via GitHub issues and the Lean Zulip chat.

Licensing & Compatibility

• Licensed under the Apache License 2.0.
• Compatible with commercial and closed-source projects.

Limitations & Caveats

• Proof script generation is not fully reliable and may require manual adjustments.
• Rules that create metavariables can lead to performance issues or infinite loops and are best used sparingly or on a per-call basis.