Problems / erdos-849 / variant-3d9db4a5
variant-3d9db4a5
proved
A partial route to the problem.
theorem Opn.erdos_849_t1 :
∃ a : ℕ, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = 1 := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
How it was proved
Proved by Proof.lean, checked by the kernel. Its attestation, 000979, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000979.json, merge commit b2c6597caff7.
Outline of Proof.lean, extracted by the gate at be99b4fba02b from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.
closeterm∃ (a : ℕ), {n : ℕ | ∃ k ≥ (1 : ℕ), (2 : ℕ) * k ≤ n ∧ n.choose k = a}.ncard = (1 : ℕ)Closes the goal.
Uses library
Exists.introExistential introduction. ,le_rflA version ofle_reflwhere the argument is implicit ,Set.ncard_coe_finset.Lean, lines 44–46
refine ⟨2, ?_⟩ rw [sol_set_eq 2 2 le_rfl (by decide), Set.ncard_coe_finset] decide
targets/erdos-849/nodes/variant-3d9db4a5/Proof.lean, lines 44–46 at
b2c6597caff7↗
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000979.json, merge commit b2c6597caff7.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-849/nodes/variant-3d9db4a5/Proof.lean, sha256 cb5d84f2cf91.import Mathlib
import Nodes.«variant-3d9db4a5».Context
open Nat
private theorem choose_mono_half {n r : ℕ} :
∀ j, r ≤ j → j ≤ n / 2 → n.choose r ≤ n.choose j := by
intro j
induction j with
| zero => intro h _; rw [Nat.le_zero.mp h]
| succ j ih =>
intro hr hj
rcases Nat.eq_or_lt_of_le hr with h | h
· rw [h]
· exact (ih (by omega) (by omega)).trans (Nat.choose_le_succ_of_lt_half_left (by omega))
private theorem sol_set_eq (a B : ℕ) (ha : 2 ≤ a) (hB : a < (B + 1).choose 2) :
{n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a} =
↑(insert a ((Finset.range (B + 1)).filter
(fun n => ((Finset.Icc 1 (n / 2)).filter (fun k => choose n k = a)).Nonempty))) := by
ext n
simp only [Set.mem_setOf_eq, Finset.coe_insert, Set.mem_insert_iff, Finset.coe_filter,
Finset.mem_range, Finset.filter_nonempty_iff, Finset.mem_Icc]
constructor
· rintro ⟨k, hk1, hk2, h⟩
by_cases hn : n ≤ B
· right
exact ⟨by omega, k, ⟨hk1, by omega⟩, h⟩
· left
by_cases hk : k = 1
· subst hk; simpa using h
· exfalso
have h2 : n.choose 2 ≤ n.choose k := choose_mono_half k (by omega) (by omega)
have h3 : (B + 1).choose 2 ≤ n.choose 2 := Nat.choose_le_choose 2 (by omega)
omega
· rintro (rfl | ⟨_, k, ⟨hk1, hk2⟩, h⟩)
· exact ⟨1, le_rfl, by omega, by simp⟩
· exact ⟨k, hk1, by omega, h⟩
/-- Erdős 849 for $t = 1$: some integer $a$ is $\binom{n}{k}$ with $1 \le k \le n/2$ in exactly
1 row $n$. The proof takes $a = 2$: the row 2 only ($\binom{2}{1}$). -/
theorem Opn.erdos_849_t1 :
∃ a : ℕ, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = 1 := by
refine ⟨2, ?_⟩
rw [sol_set_eq 2 2 le_rfl (by decide), Set.ncard_coe_finset]
decideWhat is known
Work on it
No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and no words yet
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
import Mathlib
import Nodes.«variant-3d9db4a5».Context
open Nat
/-- Erdős 849 for $t = 1$: some integer $a$ is $\binom{n}{k}$ with $1 \le k \le n/2$ in exactly
1 row $n$. The proof takes $a = 2$: the row 2 only ($\binom{2}{1}$). -/
theorem Opn.erdos_849_t1 :
∃ a : ℕ, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = 1 := by
sorryA statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
No gloss yet: no one has written in words what this statement says (D-3 v3.30); the Lean above is the statement. How to write one →
Rendered from targets/erdos-849/nodes/variant-3d9db4a5/Statement.lean. Origin: variant (partial).
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000979.json, merge commit b2c6597caff7.
Verdict pass, from attestations/000979.json.
- Submitter
t1026e-a- Toolchain
- leanprover/lean4:v4.33.1 (hash
f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63) - Mathlib
- 0df444a360eaa60ab8c11dca51a86af692955474
- Reviewer
- none needed (intermediate)
| Step | Check | Result |
|---|---|---|
| 1 | toolchain | pass |
| 2 | paths | pass |
| 4 | kernel-replay | pass |
| 5 | axioms | pass |
| 6 | hazards | pass |
| 7 | witness | pass |
| 8 | deps | pass |
Witness
Checked by the kernel — step 7 passed in the run its attestation records: attestations/000979.json, merge commit b2c6597caff7.
38a9ced51f18.theorem witness : True := trivial
No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
Relation to the problem’s statement
Checked by the kernel — checked at admission (D-30); no proof of the node is implied.
f3cbe8091271.-- relation: partial
import Mathlib
theorem relation :
(∀ t ≥ 1, ∃ a : ℕ, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ Nat.choose n k = a}.ncard = t) →
∃ a : ℕ, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ Nat.choose n k = a}.ncard = 1 :=
fun h => h 1 (by norm_num)No gloss yet: no one has written in words what this relation says (D-3 v3.30); the Lean above is the relation. How to write one →
Acknowledged findings (1)
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a off-by-one-range finding at k ≥ 1
Deliberate, as in the root: k = 0 would count the trivial binomial C(n, 0) = 1, which the problem excludes.