Add Erdős Problem 601 (infinite path or large independent set, $500 prize)#3788
Add Erdős Problem 601 (infinite path or large independent set, $500 prize)#3788henrykmichalewski wants to merge 5 commits into
Conversation
…n ordinals ($500)
Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff.
| @@ -0,0 +1,201 @@ | |||
| /- | |||
| Copyright 2025 The Formal Conjectures Authors. | |||
There was a problem hiding this comment.
nit: Could you update the copyright year to 2026 for this new file?
| **Status**: OPEN. | ||
| -/ | ||
| @[category research open, AMS 5] | ||
| theorem erdos_601 : |
There was a problem hiding this comment.
Does the source ask for a characterization of which limit ordinals have the property? This states that every limit ordinal has it, which is a much stronger concrete assertion. Could you put the class or criterion behind answer(sorry), or otherwise phrase erdos_601 as a characterization problem, with the all-ordinals statement as a named conjectural variant only if intended?
Paul-Lez
added
the
awaiting-author
…ok] + copyright 2026 Per Paul-Lez review on PR google-deepmind#3788. Mechanical nits applied on top of an upstream/main merge to pick up the new attribute infrastructure (google-deepmind#3900).
|
@Paul-Lez — applied the mechanical nits in |
…ul-Lez review) The headline previously asserted the property for every limit ordinal, which is much stronger than the source's actual question — namely, to characterize which limit ordinals have it. Per Paul-Lez's review, the headline now asserts pointwise equivalence between `HasPathOrIndepSetOfType α` and a conjectural predicate behind `answer(sorry)`. The universal "for every limit ordinal" form is moved to a named variant.
|
Thanks for the review @PaulLez. Pushed d11479d on |
2 participants
Problem
Erdős Problem 601: https://www.erdosproblems.com/601 ($500 prize)
Contents
erdos_601($500 prize note)HasPathOrIndepSetOfType αdefinitionCloses #820
Assisted by Claude (Anthropic).