refactor(GreensOpenProblems): add tests for Green 51#4309
Merged
Conversation
|
👋 This is an automated welcome message. 🤖 A few friendly reminders while the review gets started:
Thanks again for helping improve Formal Conjectures. |
github-actions
Bot
added
the
green-problems
jeangud
commented
Jun 24, 2026
mo271
approved these changes
Jun 24, 2026
mo271
added
the
awaiting-author
jeangud
force-pushed
the
green-51-refactor
branch
from
fa5f1be to
5227fc8
Compare
mo271
pushed a commit
that referenced
this pull request
Jun 24, 2026
# Description This PR proposes to introduce a notation shorthand for 𝔽-p groups, which is already used (and redefined each time) in files over the repo. **Note:** to be merged before #4305 and #4309 # Testing :white_check_mark: Built the whole repo successfully ```shell $ lake --wfail build Build completed successfully (8814 jobs). ```
jeangud
force-pushed
the
green-51-refactor
branch
from
5227fc8 to
6407aad
Compare
jeangud
force-pushed
the
green-51-refactor
branch
from
0db8e0e to
8475324
Compare
jeangud
removed
the
awaiting-author
mo271
pushed a commit
that referenced
this pull request
Jun 25, 2026
# Description
> Suppose that $A \subset \mathbb{F}_2^n$ is a set with an additive
complement of size $K$ (that is, for which there is another set $S
\subset \mathbb{F}_2^n$, $|S| = K$, with $A + S = \mathbb{F}_2^n$). Does
$2A$ contain a coset of codimension $O_K(1)$? Could it even contain a
coset of codimension $O(\log K)$?
[[Gr24](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.52)]
- Closes #1657
- **Update:** I had initially implemented this with the `maxCosetDim`
helper from [Green
51](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/51.lean)
but it complicated everything
- This present implementation is simpler, and focuses on existential
statements, without unnecessary maximality considerations.
- The byproducts of the first attempt might still be useful and were
filed under #4309 if needed
- 🤖 Initial draft obtained with **Gemini 3.1 Pro** and refined
manually for style and correctness.
- Variants left as a later exercise to keep this PR short
# Testing
✅ Files build successfully
```shell
$ lake build FormalConjectures/GreensOpenProblems/52.lean
Build completed successfully (8035 jobs).
```
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Proposing a small refactor for Green 51 as I prepare Green 52, 53.
maxCosetDimconstructFormalConjecturesForMathlibfor re-usabilityTesting
✅ Files build successfully
✅ Tests pass