Skip to content

feat(ErdosProblem): 1113#3500

Open
franzhusch wants to merge 6 commits intogoogle-deepmind:mainfrom
franzhusch:erdos-problem-1113
Open

feat(ErdosProblem): 1113#3500
franzhusch wants to merge 6 commits intogoogle-deepmind:mainfrom
franzhusch:erdos-problem-1113

Conversation

@franzhusch
Copy link
Collaborator

@franzhusch franzhusch commented Mar 9, 2026 •
edited
Loading

fixes #1966
fixes #3582

Adds Erdos Problem 1113.

Formalization assisted by Claude Opus 4.6

@github-actions github-actions bot added the erdos-problems Erdős Problems label Mar 9, 2026
@Smetalo
Copy link
Contributor

Smetalo commented Mar 10, 2026

Just a reminder to link this to #1966

mo271
mo271 approved these changes Mar 15, 2026
View reviewed changes
Copy link
Collaborator

@mo271 mo271 left a comment

Choose a reason for hiding this comment

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

Thanks looks good to me!

also create a file/link add reference to https://en.wikipedia.org/wiki/Sierpi%C5%84ski_number?

I think it would be nice to add the three open problems there.

FormalConjectures/ErdosProblems/1113.lean
∀ m, IsSierpinskiNumber m →
m.IsPerfectPower ∨ HasFinitePrimeCoveringSet m := by
sorry

Copy link
Collaborator

@mo271 mo271 Mar 15, 2026

Choose a reason for hiding this comment

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

Please add a TODO for the missing additional statement ("The smallest Sierpinski number is believed to be 78557, which was found by Selfridge" would be nice! -- as two statements one research solved asserting that 78557 is Sierpinski, and then the conjecture that it is the smallest.

Copy link
Collaborator Author

@franzhusch franzhusch Mar 16, 2026

Choose a reason for hiding this comment

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

Added those 2 statements in a Wikipedia File. Also added the other 2 open problems from the Wikipedia page to the Wikipedia File.

@mo271 mo271 added the awaiting-author The author should answer a question or perform changes. Reply when done. label Mar 15, 2026
@franzhusch franzhusch removed the awaiting-author The author should answer a question or perform changes. Reply when done. label Mar 16, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mo271 mo271 mo271 approved these changes

Assignees

No one assigned

Labels

erdos-problems Erdős Problems wikipedia

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Selfridge's conjecture (Sierpiński problem) Erdős Problem 1113: Sierpinski Numbers with No Finite Covering Set

3 participants

@franzhusch @Smetalo @mo271