agentleFS
Sign inStart free
VeryMathVeryMath/AI4Math-Lean-Agents/AGENTS.md

AI4Math-Lean-Agents

AGENTS.md9 starsChanged 4 months agoMITView on GitHub

Use skills/lean-setup/SKILL.md for setup-only tasks such as installing or verifying Lean 4, elan, lake, or a reusable mathlib workspace. Use the canonical shared Skill layer at skills/lean-formalization/SKILL.md for Lean 4 formalization, proof repair, theorem transcription, sorry completion, Lean patch review, optional adapter-first Lean-specialist backend work, local Lean validation, and minimal failure handoff. Reusable scripts, examples, prompts, schemas, and references live in the non-user-facing support layer at skills/lean-runtime/; install it alongside the two public Skill entrypoints. Useful validation:

  • Where files are headingNew AGENTS.md files have more rules about keeping secrets out of the code, and fewer about code style.

    Of the AGENTS.md files we read, the 31,700 first seen in the last six months, against the older ones: the kind of rule that gained most share, and the kind that lost most. About files like this in general, not this one, and an estimate, since a kind is a pattern in the words.

  • In this repository5 other files it gives its agents.

The file

We split this AGENTS.md into the rules it gives an agent

10 rules. About 2 are common, 4 are distinctive, and 4 are very specific to this project.

  • ≈2

    Common · estimate

    Many files like this have a rule of this kind.

  • ≈4

    Distinctive · estimate

    This author's own choices. Worth a look.

  • 4

    Very specific

    Tied to their project's names, files or tools. Probably skip.

  • Common
  • Distinctive
  • Very specific
  • could be automatic: a setting could enforce it
  1. Very specific:

    Use skills/lean-setup/SKILL.md for setup-only tasks such as installing or verifying Lean 4, elan, lake, or a reusable mathlib workspace.

    line 3
  2. Very specific:

    Use the canonical shared Skill layer at skills/lean-formalization/SKILL.md for Lean 4 formalization, proof repair, theorem transcription, …

    line 4
  3. Distinctive:

    If the user's language is ambiguous, default to Chinese.

    line 15
  4. Distinctive:

    Do not treat a language switch as a task reset.

    line 17
  5. Distinctive:

    When no target is provided, run or propose a safe local smoke/readiness check before asking for more input.

    line 18
  6. Distinctive:

    Use the bundled smoke test when no user target is available.

    line 19
  7. Common:

    Do not require API keys for the default coding-agent path.

    line 22
  8. Very specific:

    Prefer the user's existing Lake project.

    line 24
  9. Very specific:

    Use ${AI4MATH_HOME:-~/.ai4math}/lean-workspaces/<version-key>/ for standalone tasks that need a different Lean/mathlib revision.

    line 25
  10. Common:

    Do not commit API keys, local runtime state, or machine-specific Numina paths.

    line 28

≈ “Common” is an estimate: at least 1 in 5 of the 40,246 AGENTS.md files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.

Keep what fits and drop the rest. Your version, ready for your agents.
Files
AGENTS.md

Agent Instructions

Use skills/lean-setup/SKILL.md for setup-only tasks such as installing or verifying Lean 4, elan, lake, or a reusable mathlib workspace. Use the canonical shared Skill layer at skills/lean-formalization/SKILL.md for Lean 4 formalization, proof repair, theorem transcription, sorry completion, Lean patch review, optional adapter-first Lean-specialist backend work, local Lean validation, and minimal failure handoff. Reusable scripts, examples, prompts, schemas, and references live in the non-user-facing support layer at skills/lean-runtime/; install it alongside the two public Skill entrypoints.

Core rules:

  • This is a coding-agent-first Lean skill.
  • The coding agent is the primary Lean worker.
  • Setup-only mode should not ask for a theorem target.
  • Backend integration is adapter-first. Numina and Archon are recommended adapter candidates, not defaults or hard requirements; official Numina has a built-in recommended adapter recipe.
  • Other Lean-specialist backends may be connected by the coding agent through skills/lean-runtime/references/backend_adapter_checklist.md; do not call any backend until deployment, readiness checks, invocation, validation, and failure triage are documented.
  • Match the user's language by default.
  • If the user's language is ambiguous, default to Chinese.
  • Lead the interaction: inspect context, summarize what is ready, recommend the next useful step, and ask at most one blocking question.
  • Do not treat a language switch as a task reset; keep the current diagnosis and continue leading in the new language.
  • When no target is provided, run or propose a safe local smoke/readiness check before asking for more input.
  • Use the bundled smoke test when no user target is available.
  • Formalization/proof readiness should inspect local Lean readiness first; inspect Numina/backend readiness only when the user asks for an optional Lean-specialist backend.
  • Setup-only readiness should focus on local Lean/mathlib state, and should mention or inspect a backend only when the user asks for an optional backend adapter.
  • Do not require API keys for the default coding-agent path.
  • Shared workspace is the default Lean project context for standalone work; Numina may target it instead of upstream examples.
  • Prefer the user's existing Lake project. Use the shared ${AI4MATH_HOME:-~/.ai4math}/lean-workspace only when a standalone file needs project context, and default that managed workspace to leanprover/lean4:v4.28.0 unless the user explicitly overrides it.
  • Use ${AI4MATH_HOME:-~/.ai4math}/lean-workspaces/<version-key>/ for standalone tasks that need a different Lean/mathlib revision; do not overwrite the canonical managed workspace for version drift.
  • Preserve theorem statements unless the user explicitly approves a change.
  • Reject final patches containing sorry, admit, or newly introduced axiom.
  • Do not commit API keys, local runtime state, or machine-specific Numina paths.

Useful validation:

PYTHONDONTWRITEBYTECODE=1 python skills/lean-runtime/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests

Download now (ZIP)

Does it work?

Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.

No reviews yet

People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.

  • It worked
  • Partly
  • It didn't
What did you use it for? e.g. Reviewing pull requests in a Rails app

Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.

Your trail

Files you open will collect here, so you can find them again.

Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.

Now do this for your own.

Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.

Check your setup, free