feat(ErdosProblems): 152 #1501
Merged
feat(ErdosProblems): 152 #1501
Conversation
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
mo271
reviewed
Jan 6, 2026
Collaborator
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Thanks, looks good
Please use latex markdown for the docstrings!
Collaborator
Perhaps actually add a TODO in the file, so it is not forgotten |
Member
|
There already is a TODO |
Collaborator
|
Ah, great, I just didn't see it at the top of the file (because I usually put it at the bottom), now I see it... |
YaelDillies
added
the
awaiting-author
Co-authored-by: Moritz Firsching <firsching@google.com>
Collaborator
Author
|
@mo271 Is it a convention to use $$ instead of backticks in this repository? I am always using backticks in all my PRs to this repo, but I am happy to change it. |
Member
|
You should use $$ for latex and ` for lean. Whether you write the docstring in latex or in Lean depends on how far the formal and informal statements are |
YaelDillies
removed
the
awaiting-author
jdhruv555
pushed a commit
to jdhruv555/formal-conjectures
that referenced
this pull request
Jan 7, 2026
Closes google-deepmind#389 Some remarks: 1. In the paper [ESS94] On Sum Sets of Sidon Sets, the authors formulate this conjecture by using limit, which will be equivalent to the formulation on the website. The limit formulation is easier to formalize and this is why I defined the function `f`. This definition of `f` also makes it easier to talk about the growth rate. 2. For the conjecture related to infinite Sidon sets, one needs the results in the PR google-deepmind#1481, so I left it as a TODO. <img width="1052" height="413" alt="Screenshot 2026-01-06 at 1 40 26 AM" src="https://github.com/user-attachments/assets/28b211a9-0c66-4089-972e-a722939ffc45" /> --------- Co-authored-by: Moritz Firsching <firsching@google.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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 #389
Some remarks:
f. This definition offalso makes it easier to talk about the growth rate.