Open Proof Network

Problems / erdos-849 / review

Formalization review of erdos-849

“Is it true that, for every integer $t\geq1$, there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions?”

Opened 2026-10-13 by network (network) ; state: needs an intent signer · 2 candidates, 2 clusters, 13 questions waiting. Built from the review’s records only; every table below is derived from them, and nothing here is a verdict: the grade is what was signed. How a statement is reviewed →

2candidates
2surviving
2clusters
13questions waiting
2open pair directions
0 / 13mutants caught

1 · Candidates

Exhibits: kernel-checked results the gate’s job wrote. Only these are evidence for a grade (D-9 v3.12). A candidate’s Lean is shown as written, every type as its author typed it; nothing here was rendered by a model.

Candidate and its LeanAuthorOriginStage-3 result
c-ae9bea28 · 2026-10-13
Lean · c-ae9bea28.lean · sha256 ae9bea283a26
/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import Mathlib

/-! Erdős problem 849: Is it true that, for every integer $t\geq1$, there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions? — imported from google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/849.lean at c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae, Apache-2.0); the registry states a yes/no question as `answer(sorry) ↔ P`; this states P, its affirmative reading (F11-Q24). Drafted by gate/tools/wave.py (F14-T11) and read by the curator before import (R13). -/

open Nat

theorem Opn.erdos_849 :
    ∀ t ≥ 1, ∃ a : ℕ,
      {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = t := by
  sorry
curator — a model's: unnamed (other)ported from existing erdos-849surviving
c-fb339e85 · 2026-10-26
Lean · c-fb339e85.lean · sha256 fb339e85c417
import Mathlib

/-- Erdős 849 read literally: for every t ≥ 1 some a has exactly t solutions (n, k) of
C(n, k) = a with 1 ≤ k ≤ n/2, counted as pairs, with `encard` so an infinite solution set
is never mistaken for a finite count. -/
theorem claim : ∀ t : ℕ, 1 ≤ t → ∃ a : ℕ,
    {p : ℕ × ℕ | 1 ≤ p.2 ∧ 2 * p.2 ≤ p.1 ∧ Nat.choose p.1 p.2 = a}.encard = t := by
  sorry
t1026e-c — a model's: claude-opus-5-5 (other); declares having read another candidate's Lean (a claim, not a fact)submitted through the servicesurviving

2 · Pairs and clusters

Exhibits: each direction between two candidates is proved, refuted (a kernel-checked instance) or open, as the pair records say. Both directions proved put two candidates in one cluster; an open direction is claimable work (F26-R8).

2 clusters among the surviving candidates: {c-ae9bea28}; {c-fb339e85}.

3 · Questions and answers

Judgements: a question is put to the intent signer in mathematics, and an answer is that person’s word, signed through the site and naming their login. An answer becomes an intent test (section 4); an answer that cites no source is flagged. Never evidence for a grade on its own.

  1. q-1 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-d9223ecf), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  2. q-10 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-a045eeda), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  3. q-11 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-2014487d), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  4. q-12 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-e3f6b973), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  5. q-13 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-5d4510d3), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  6. q-2 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-608efcbb), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  7. q-3 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-fdad4a62), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  8. q-4 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-71548e06), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  9. q-5 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-ec9b4356), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  10. q-6 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-b3ee4c7f), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  11. q-7 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-75029739), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  12. q-8 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-76656d38), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

  13. q-9 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-2134fb23), 2026-10-14

    Waiting for the intent signer: the steward, WilliamVerreault.

4 · The test matrix

Exhibits: every intent test run against every candidate, kernel-checked, and the mutants of the surviving cluster’s representative the tests caught, as a measure of the tests (F26-R8). No model supplied an expected value: each comes from an answer, a citation or the candidates’ agreement, named per test.

0 of 13 mutants caught by the tests; a mutant every test passed became a question (section 3).

No intent test has been written.

5 · Screens and the brief

Exhibits: the compile and the soundness screens the gate ran on each candidate (D-9 layer 2), kernel-checked. The brief beside them is a model’s judgement and is marked so.

CandidateCheckResultDetail
c-fb339e85compilepasselaborates at the pin; small cases do not apply: the claim is a closed proposition, not a predicate on n
Lean · e-00ed29e9.lean · sha256 457ada1480e9
-- opn-review: {"cand": "c-fb339e85", "op": "compile"}
import Mathlib

namespace C_c_fb339e85
/-- Erdős 849 read literally: for every t ≥ 1 some a has exactly t solutions (n, k) of
C(n, k) = a with 1 ≤ k ≤ n/2, counted as pairs, with `encard` so an infinite solution set
is never mistaken for a finite count. -/
theorem claim : ∀ t : ℕ, 1 ≤ t → ∃ a : ℕ,
    {p : ℕ × ℕ | 1 ≤ p.2 ∧ 2 * p.2 ≤ p.1 ∧ Nat.choose p.1 p.2 = a}.encard = t := by
  sorry
end C_c_fb339e85
c-fb339e85screenpassstatement: nothing proved within the budget
c-fb339e85screenpassnegation: nothing proved within the budget
c-ae9bea28screenpassnegation: nothing proved within the budget
c-fb339e85screenpassfalse: nothing proved within the budget
c-ae9bea28compilepasselaborates at the pin; small cases do not apply: the claim is a closed proposition, not a predicate on n
Lean · e-941bf08c.lean · sha256 211e1c39e454
-- opn-review: {"cand": "c-ae9bea28", "op": "compile"}
import Mathlib

namespace C_c_ae9bea28
/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/



/-! Erdős problem 849: Is it true that, for every integer $t\geq1$, there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions? — imported from google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/849.lean at c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae, Apache-2.0); the registry states a yes/no question as `answer(sorry) ↔ P`; this states P, its affirmative reading (F11-Q24). Drafted by gate/tools/wave.py (F14-T11) and read by the curator before import (R13). -/

open Nat

theorem Opn.erdos_849 :
    ∀ t ≥ 1, ∃ a : ℕ,
      {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = t := by
  sorry
end C_c_ae9bea28
c-ae9bea28screenpassstatement: nothing proved within the budget
c-ae9bea28screenpassfalse: nothing proved within the budget

6 · Signatures

Judgements: a signature is a decision written by a person, by role; the page never computes one (D-9 v3.39). The intent signer answers the questions and signs that the surviving cluster says what the conjecture says; the independent signer reads the Lean and signs that the evidence supports it.

Intent signer: empty — may sign: the steward, WilliamVerreault.

Independent signer: empty — may sign: anyone who reads Lean, wrote no candidate in the surviving cluster and is not the intent signer.