From 3369993e709eb76b4ee4f6121625a65e9200c998 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Fri, 22 May 2026 21:26:11 -0400 Subject: [PATCH 1/3] move AI policy to top --- CONTRIBUTING.md | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b9b6b8068..bdc12fb89 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -57,6 +57,11 @@ If you are adding something new to CSLib and are in doubt about it, you are very If you are unfamiliar with CSLib as a whole and want to understand how to get started, please see [Getting started](#getting-started). +# The role of AI + +CSLib in general follows the Mathlb [Use of AI](https://leanprover-community.github.io/contribute/index.html#use-of-ai) policy. In particular, take note of: +> If you use artificial intelligence ... please explain this in the PR description. Explain which tool(s) you used and how you used it. This provides useful context for reviewers: tools make different mistakes than humans, so knowing this makes it easier to spot common errors. + # Style and documentation We generally follow the [mathlib style for coding and documentation](https://leanprover-community.github.io/contribute/style.html), so please read that as well. Some things worth mentioning and conventions specific to CSLib are explained next. @@ -322,12 +327,3 @@ The formal methods community has a wide range of verification techniques that co Since Boole back ends reduce correctness questions to Lean conjectures, automation is central. We already rely on key techniques such as `grind` and `lean-smt`. Additional work on automation for conjectures generated from Boole is welcome, including domain-specific automation that remains performant and readable. - -#### The role of AI - -There are two primary areas where generative AI can help: - -- generating/refining specifications (at the front-end or Boole level) -- helping to prove Lean conjectures - -Other creative uses of AI are welcome, but contributions should remain reviewable and maintainable. From edf9d8703a36cbdd55c27797960497f055cea7b9 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Fri, 22 May 2026 21:27:25 -0400 Subject: [PATCH 2/3] adjust TOC --- CONTRIBUTING.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index bdc12fb89..3d9f20e0c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -2,6 +2,7 @@ - [Contributing to CSLib](#contributing-to-cslib) - [Contribution model](#contribution-model) +- [The role of AI](#the-role-of-ai) - [Style and documentation](#style-and-documentation) - [Variable names](#variable-names) - [Proof style and golfing :golf:](#proof-style-and-golfing-golf) @@ -38,8 +39,6 @@ - [Back ends for Boole](#back-ends-for-boole) - [Implementing verification paradigms](#implementing-verification-paradigms) - [Lean automation](#lean-automation) - - [The role of AI](#the-role-of-ai) - # Contributing to CSLib From 36e58b77fd0e27bb7b1d4a07d9088a563bf35245 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sat, 23 May 2026 12:43:36 +0200 Subject: [PATCH 3/3] small fix --- CONTRIBUTING.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 3d9f20e0c..a2f8f8841 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -58,8 +58,8 @@ If you are unfamiliar with CSLib as a whole and want to understand how to get st # The role of AI -CSLib in general follows the Mathlb [Use of AI](https://leanprover-community.github.io/contribute/index.html#use-of-ai) policy. In particular, take note of: -> If you use artificial intelligence ... please explain this in the PR description. Explain which tool(s) you used and how you used it. This provides useful context for reviewers: tools make different mistakes than humans, so knowing this makes it easier to spot common errors. +CSLib in general follows the Mathlib policy on [use of AI](https://leanprover-community.github.io/contribute/index.html#use-of-ai). In particular, take note of: +> If you use artificial intelligence [...] please explain this in the PR description. Explain which tool(s) you used and how you used it. This provides useful context for reviewers: tools make different mistakes than humans, so knowing this makes it easier to spot common errors. # Style and documentation