agentleFS
Sign inStart free
VeryMathVeryMath/AI4Math-Lean-Agents/.cursor/rules/lean-formalization.mdc

AI4Math-Lean-Agents / rules

Cursor rule9 starsChanged 4 months agoMITView on GitHub

Lean Formalization workflow for Lean 4 formalization and proof repair

  • Where files are headingNew Cursor rule files have more rules about planning and tracking tasks, and fewer about code style.

    Of the Cursor rule files we read, the 4,181 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 lean-formalization.mdc into the rules it gives an agent

1 rule. About 0 are common, 0 are distinctive, and 1 is very specific to this project.

  • ≈0

    Common · estimate

    Many files like this have a rule of this kind.

  • ≈0

    Distinctive · estimate

    This author's own choices. Worth a look.

  • 1

    Very specific

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

  • Common
  • Distinctive
  • Very specific
  1. Very specific:

    Use skills/lean-formalization/SKILL.md as the canonical workflow.

    line 10

≈ “Common” is an estimate: at least 1 in 5 of the 6,668 Cursor rule 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
lean-formalization.mdc
---
description: Lean Formalization workflow for Lean 4 formalization and proof repair
globs:
  - "**/*.lean"
  - "**/lakefile.*"
  - "**/lean-toolchain"
alwaysApply: false
---

Use `skills/lean-formalization/SKILL.md` as the canonical workflow.

This is a coding-agent-first Lean skill. The coding agent is the primary Lean worker: read/edit Lean, run Lean/Lake, iterate from errors, and validate final patches locally. Official Numina is the only currently supported deployable backend adapter; preserve that deployment/call path but do not make it the default. Archon and other backends are future adapters until their setup, call, credential, mutation, and validation contracts are documented. Match the user's language by default; if the user's language is ambiguous, default to Chinese. Do not treat language switches as task resets. Lead the interaction: inspect context, summarize what is ready, recommend the next useful step, and ask at most one blocking question. 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. Opening readiness should inspect local Lean readiness first; inspect Numina/backend readiness only when the user asks for an optional Lean-specialist backend. Do not require API keys for the default coding-agent path. Shared workspace is the default Lean project context; Numina may target it instead of upstream examples. The helper CLI under `skills/lean-runtime/scripts/` is optional shared tooling and should be used only for environment checks, structured validation, optional Numina readiness/setup, patch review, `sorry` detection, or minimal failure handoff.

Deploy or call the official Numina backend only when the user asks for it or approves it after an explanation. Keep secrets in environment variables or ignored local files.

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