feat(ErdosProblems): 254#2324
Closed
danielchin wants to merge 27 commits intogoogle-deepmind:mainfrom
Closed
Conversation
mo271
reviewed
Feb 22, 2026
Collaborator
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Thanks, looks good, just some minor comments
…epmind#2299) Map 'solved (Lean)', 'proved (Lean)', 'disproved (Lean)' to 'formally solved' as a distinct category from 'solved', and tags the issue "formalisation exists elsewhere".
Resolves google-deepmind#199. Note: I'm using Claude + Opus for supervised formalization tasks. Claude has no permission to use git on my machine. --------- Co-authored-by: Moritz Firsching <firsching@google.com>
Fixes google-deepmind#1828 This PR formalizes Gourevitch's series identity. Statement: ∑' n, ((1 + 14 n + 76 n^2 + 168 n^3) / 2^(20 n)) * (Nat.centralBinom n)^7 = 32 / π^3 Details: - Adds theorem `gourevitch_series_identity` - Uses `Nat.centralBinom` for binomial coefficient formulation - Categorized under `research solved` and `AMS 11 33` - Includes literature references References: - Guillera (2003), Experimental Mathematics - Au (2025), Journal of Symbolic Computation --------- Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de> Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>
The `=` should be an `≤` because "eventually zero" should be a possibility. See also [Thomas Bloom's comment](https://www.erdosproblems.com/forum/thread/943#post-2158)
…ind#2325) Went through all of these by hand and updated them accordingly. This was one of those PRs where half way through, I realize it might have been better to split it up individually. Let me know if you want me to break these into smaller PRs for the sake of reviewability. All these fall into a category: 1) Some of these were actually solved and I've changed the status of them. 2) Some of these do not have a theorem labeled `erdos_{number}` due to poor naming convetion. 3) Some of these purposely do not have a theorem labeled `erdos_{number}` because the original problem was stated in multiple parts and the parts of the questions are labeled as `erdos_{number}.parts.i` which are not caught by the py script. 4) Some of these are trying to formalize problems in the form of `Estimate f(n)`, which doesn't seem to have an agreed upon standard right now. Some examples of these are problems 1084, 1085, and 1095. Maybe we can come up with an agreement on how to formalize these? Possibly defining a lower bound, upper bound, and an equality? Problem 851 is interesting because it's marked as Proved but is still red, so I'm not sure what the current status of that one is and left that as is. I've also taken the liberty to update references and docstrings to better match the Erdos Problem website. Closes google-deepmind#2300 Closes google-deepmind#2301 Closes google-deepmind#2302 Closes google-deepmind#2303 Closes google-deepmind#2304 Closes google-deepmind#2305 Closes google-deepmind#2306 Closes google-deepmind#2307 Closes google-deepmind#2308 Closes google-deepmind#2309 Closes google-deepmind#2310 Closes google-deepmind#2311 Closes google-deepmind#2312 Closes google-deepmind#2313 Closes google-deepmind#2314 Closes google-deepmind#2315 Closes google-deepmind#2316 Closes google-deepmind#2317 Closes google-deepmind#2318 Closes google-deepmind#2319 Closes google-deepmind#2320 Closes google-deepmind#2321 Closes google-deepmind#2322
github-actions
bot
added
linter
mathoverflow
arxiv
wikipedia
green-problems
Originally done in google-deepmind#1371. Co-authored-by: Bolton Bailey <bolton.bailey@gmail.com>
# Description
Let $A_1, \dots, A_{100}$ be ‘cubes’ in $\mathbb{F}^n_3$. Is it true
that $A_1 + \dots + A_{100} = \mathbb{F}^n_3$?
- Closes google-deepmind#1561
# Testing
- Builds successfully
```shell
$ lake build FormalConjectures/GreensOpenProblems/26.lean
Build completed successfully (7975 jobs).
```
Website now contains the condition that the set $A$ is pairwise coprime. If not then there are always infinitely many unrepresentable numbers (the non-multiples of the gcd).
- Fix order of quantifiers in Selfridge example because the length `k` of the sequence is determined by the magnitude of the primes. If we take `k = 1` before the primes themselves, then very large primes will never straddle `1` in their sums of reciprocals, giving a contradiction. - Redefine `consecutivePrimes` in order to formalise this interpretation. - The condition that `A` is the set of numbers with only one prime from the sequence dividing it requires multiplicity one as well. - Fix constraints on `eps` - Add a TODO since the updated website mentions that repetitions may be allowed in `Set.IsMulCardSet`, although both versions are open.
fixes google-deepmind#1975 Assisted by Claude Opus 4.6 --------- Co-authored-by: catalan <noreply> Co-authored-by: Moritz Firsching <firsching@google.com>
Contributor
Author
|
The rebase was a bit messier than expected. I'm also not entirely sure why the CLA check is failing either. Worse case, I can just spin up a new PR from head. |
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
11 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.
Closes #444
Formalizes Erdos Problem 254: https://www.erdosproblems.com/254
Assisted by Gemini/Antigravity