Skip to content

Conversation

@CoolRmal
Copy link
Collaborator

@CoolRmal CoolRmal commented Jan 8, 2026

I think the suggestion here https://www.erdosproblems.com/forum/thread/289#post-2245 makes sense, but I don't 0<a is necessary.

Closes #1539

@github-actions github-actions bot added the erdos-problems Erdős Problems label Jan 8, 2026
@CoolRmal CoolRmal changed the title Update 289.lean fix(ErdosProblems/289) Jan 8, 2026
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Could we change the statement so that the intervals are given by their endpoints? That would make the non-overlapping condition easier to state

@YaelDillies YaelDillies changed the title fix(ErdosProblems/289) fix(ErdosProblems/289): assume intervals are Jan 9, 2026
@YaelDillies YaelDillies changed the title fix(ErdosProblems/289): assume intervals are fix(ErdosProblems/289): assume intervals are non-overlapping Jan 9, 2026
@CoolRmal CoolRmal requested a review from YaelDillies January 14, 2026 09:18
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Looks great, thanks!

@YaelDillies YaelDillies merged commit e9e462c into google-deepmind:main Jan 14, 2026
6 checks passed
@CoolRmal CoolRmal deleted the Erdos289 branch January 14, 2026 19:10
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.

Erdős Problem #289 problem statement updated

4 participants