Skip to content

chore: reword AI policy for clarity#850

Merged
grunweg merged 6 commits into
leanprover-community:lean4from
grunweg:reword-ai-disclosure
May 27, 2026
Merged

chore: reword AI policy for clarity#850
grunweg merged 6 commits into
leanprover-community:lean4from
grunweg:reword-ai-disclosure

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented May 22, 2026

  • move the sentence about LLM use one paragraph down: the current wording may be confusing for new contributors (who may think the current policy is mainly about writing comments)
  • make the expected level of disclosure more precise, by suggesting a possible format
  • reword the paragraph about vouching to clarify what we actually mean. It is not 'I understand the math, and formalisation has no intrinsic content anyway'.

No substantial policy change (intended), but clarifications in spirit of the current policy.

- move the sentence about LLM use one paragraph down: the current wording
  may be confusing for new contributors (who may think the current policy
  is mainly about writing comments)
- make the expected level of disclosure more precise, by suggesting a
  possible format
- reword the paragraph about vouching to clarify what we actually mean
  It is not 'I understand the math, and formalisation has no intrinsic
  content anyway'.
@grunweg grunweg requested a review from b-mehta May 22, 2026 21:43
@grunweg grunweg force-pushed the reword-ai-disclosure branch from 44e5f84 to e723058 Compare May 22, 2026 22:15
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great, thanks

Comment thread templates/contribute/index.md Outdated
Comment thread templates/contribute/index.md Outdated
Comment thread templates/contribute/index.md Outdated
@thorimur
Copy link
Copy Markdown
Contributor

Looks good to me! :)

grunweg and others added 2 commits May 26, 2026 16:34
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
@grunweg grunweg merged commit 3831eac into leanprover-community:lean4 May 27, 2026
1 check passed
@grunweg grunweg deleted the reword-ai-disclosure branch May 27, 2026 15:32
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.

4 participants