Skip to content

Conversation

@mo271
Copy link
Collaborator

@mo271 mo271 commented Jan 7, 2026

No description provided.

@mo271 mo271 requested a review from callesonne January 7, 2026 09:13
@github-actions github-actions bot added the erdos-problems Erdős Problems label Jan 7, 2026
@mo271 mo271 added misformalization and removed erdos-problems Erdős Problems labels Jan 7, 2026
@mo271 mo271 enabled auto-merge (squash) January 7, 2026 09:19
@YaelDillies YaelDillies changed the title Fix Erdős problem 659 fix(ErdosProblems/659): make asymptotic Jan 7, 2026
@YaelDillies YaelDillies disabled auto-merge January 7, 2026 11:21
@YaelDillies YaelDillies added the awaiting-author The author should answer a question or perform changes. Reply when done. label Jan 7, 2026
@CoolRmal
Copy link
Collaborator

CoolRmal commented Jan 9, 2026

I just notice this PR and I'll close mine. I think we need to change ∀ n into ∀ n ≥ 4 (as the problem only makes sense for n ≥ 4). If we don't add this requirement, then one can prove the opposite by taking the advantage of the fact that a 0 is an empty set and thus 3 ≤ minimalDistinctDistancesSubsetOfSize (a 0) 4 = 0.

@YaelDillies
Copy link
Collaborator

You're right. The issue ultimately is that 3 ≤ minimalDistinctDistancesSubsetOfSize (a n) 4 doesn't mean "every subset of $4$ points determines at least $3$ distances" if a n has size at most three. Let me fix this

@YaelDillies YaelDillies removed the awaiting-author The author should answer a question or perform changes. Reply when done. label Jan 9, 2026
Copy link
Collaborator

@callesonne callesonne left a comment

Choose a reason for hiding this comment

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

LGTM!

mo271 and others added 2 commits January 9, 2026 18:19
@YaelDillies YaelDillies enabled auto-merge (squash) January 9, 2026 18:20
@YaelDillies YaelDillies merged commit 5c73f5c into google-deepmind:main Jan 9, 2026
6 checks passed
@mo271 mo271 mentioned this pull request Jan 15, 2026
2 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants