Skip to content

Ai policy#1187

Draft
jfindlay wants to merge 2 commits into
leanprover-community:masterfrom
jfindlay:AI-Policy
Draft

Ai policy#1187
jfindlay wants to merge 2 commits into
leanprover-community:masterfrom
jfindlay:AI-Policy

Conversation

@jfindlay

Copy link
Copy Markdown
Contributor

No description provided.

jfindlay and others added 2 commits June 15, 2026 04:23
Agent-actionable instructions belong in the conventionally-discovered
AGENTS.md file; human policy and accountability obligations remain in
AI-POLICY.md. This separation ensures agents can find their instructions
without custom discovery logic, while keeping human-facing policy and
enforcement rules separate.

Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Give agents the merge-blocking checks and a definition-of-done so they
self-verify before finishing.

Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

@jfindlay jfindlay mentioned this pull request Jun 15, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant