Erdos Conjecture 386 #1239
Erdos Conjecture 386 #1239
Conversation
|
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. |
callesonne
left a comment
callesonne
left a comment
There was a problem hiding this comment.
Thanks for the contribution! Here are some comments :)
| def erdos_386_equation (a b : ℕ) (A : Finset ℕ) := | ||
| Nat.choose a b = ∏ α ∈ A, α | ||
|
|
||
| /- |
There was a problem hiding this comment.
| /- | |
| /-- |
Docstrings (i.e. comments over theorems / definitions) must start like this.
| def erdos_386_equation (a b : ℕ) (A : Finset ℕ) := | ||
| Nat.choose a b = ∏ α ∈ A, α |
There was a problem hiding this comment.
Since this is only used once in the statement of erdos_386 I would not add it as a definition, and rather just state it there.
| The following set contains all solutions `(n, k, P)` to the Erdős problem 386. | ||
| A solution is a tuple `(n, k, P)`, where `n ≥ 2` and `k` are an integers and `P` | ||
| is a non-empty finite set of | ||
| distinct prime numbers, such that it's product is binomial coefficient n choose k. |
There was a problem hiding this comment.
Could you make this comment more precise? For example you do not mention that 2 ≤ k ≤ n - 2 and that the elements of P need to be primes.
| def erdos_386_solutions : Set (ℕ × ℕ × Finset ℕ) := { | ||
| (n, k, P) | | ||
| (n ≥ 2 ∧ 2 ≤ k ∧ k ≤ n - 2) ∧ | ||
| P.Nonempty ∧ | ||
| (∀ p ∈ P, p.Prime) ∧ | ||
| erdos_386_equation n k P | ||
| } |
There was a problem hiding this comment.
I think this is missing the condition that the primes are consecutive.
| -/ | ||
| def erdos_386_solutions : Set (ℕ × ℕ × Finset ℕ) := { | ||
| (n, k, P) | | ||
| (n ≥ 2 ∧ 2 ≤ k ∧ k ≤ n - 2) ∧ |
There was a problem hiding this comment.
| (n ≥ 2 ∧ 2 ≤ k ∧ k ≤ n - 2) ∧ | |
| (n ≥ 2 ∧ 2 ≤ k ∧ k ≤ n - 2) ∧ |
I would put either n ≥ 4 or no condition on n here, since for n < 3 no such k exist.
3 participants
This is the statement of Erdős Conjecture 386.
fixes #703