feat(ErdosProblems): 794 #1739
feat(ErdosProblems): 794 #1739
Conversation
formalize Erdős google-deepmind#794 (disproved)
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
| /-- Harris's counterexample has exactly 28 edges. -/ | ||
| @[category test, AMS 5] | ||
| theorem harrisCounterexample_card : HarrisCounterexample.card = 28 := by native_decide | ||
|
|
||
| /-- Harris's counterexample is 3-uniform. -/ | ||
| @[category test, AMS 5] | ||
| theorem harrisCounterexample_is3Uniform : Is3Uniform HarrisCounterexample := by | ||
| unfold Is3Uniform | ||
| native_decide |
There was a problem hiding this comment.
Can these be closed with decide or decide +kernel ?
There was a problem hiding this comment.
Tried decide / decide +kernel, but it hit maxRecDepth during lake build.
There was a problem hiding this comment.
Done, ran this morning and avoided maxRecDepth
| ∃ (S : Finset α) (_ : S ∈ Finset.univ.powersetCard k), | ||
| (H.filter (fun e => e ⊆ S)).card ≥ m |
There was a problem hiding this comment.
| ∃ (S : Finset α) (_ : S ∈ Finset.univ.powersetCard k), | |
| (H.filter (fun e => e ⊆ S)).card ≥ m | |
| ∃ S : Finset α, #S = k \and #{e \in H | e ⊆ S} ≥ m |
You will need open Finset first
| -- `answer(False)` is `False`, so this is equivalent to `¬ Statement`. | ||
| simp only [false_iff] |
There was a problem hiding this comment.
| -- `answer(False)` is `False`, so this is equivalent to `¬ Statement`. | |
| simp only [false_iff] | |
| simp? |
and see what it comes up with
YaelDillies
added
the
awaiting-author
3 participants
Adds a formalization of Erdős Problem 794 (disproved; see erdosproblems.com/794). Hope this is a good fit for the repository’s “short counterexample / not a lengthy proof” guideline but I'm happy to adjust if you’d prefer a different level of abstraction. Completed with the assistance of Harmonic's Aristotle and Claude Opus 4.5.