Open Proof Network

Problems / erdos-1094 / review

Formalization review of erdos-1094

“For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$, with only finitely many exceptions.”

Opened 2026-10-13 by network (network) ; state: needs an intent signer · 1 candidate, 1 cluster, 8 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 →

1candidate
1surviving
1cluster
8questions waiting
0open pair directions
0 / 8mutants 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-bbeff8af · 2026-10-13
Lean · c-bbeff8af.lean · sha256 bbeff8af9bb8
/-
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 1094: For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$, with only finitely many exceptions. — imported from google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/1094.lean at c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae, Apache-2.0); stated as the registry states it. Drafted by gate/tools/wave.py (F14-T11) and read by the curator before import (R13). -/

open scoped Nat

theorem Opn.erdos_1094 :
    {(n, k) : ℕ × ℕ | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite := by
  sorry
curator — a model's: unnamed (other)ported from existing erdos-1094surviving

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).

1 cluster among the surviving candidates: {c-bbeff8af}.

No pair has been compared yet.

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-f0003362), 2026-10-14

    Waiting for the intent signer: the steward, thisisanameforsure.

  2. 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-3528e369), 2026-10-14

    Waiting for the intent signer: the steward, thisisanameforsure.

  3. 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-6b7bc1b2), 2026-10-14

    Waiting for the intent signer: the steward, thisisanameforsure.

  4. 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-350d191c), 2026-10-14

    Waiting for the intent signer: the steward, thisisanameforsure.

  5. 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-179b07a1), 2026-10-14

    Waiting for the intent signer: the steward, thisisanameforsure.

  6. 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-13e8ccfe), 2026-10-14

    Waiting for the intent signer: the steward, thisisanameforsure.

  7. 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-7bd0206a), 2026-10-14

    Waiting for the intent signer: the steward, thisisanameforsure.

  8. 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-c9216720), 2026-10-14

    Waiting for the intent signer: the steward, thisisanameforsure.

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 8 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-bbeff8afscreenpassnegation: nothing proved within the budget
c-bbeff8afscreenpassfalse: nothing proved within the budget
c-bbeff8afscreenpassstatement: nothing proved within the budget
c-bbeff8afcompilepasselaborates at the pin; small cases do not apply: the claim is a closed proposition, not a predicate on n
Lean · e-fa693af0.lean · sha256 af61f20708ad
-- opn-review: {"cand": "c-bbeff8af", "op": "compile"}
import Mathlib

namespace C_c_bbeff8af
/-
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 1094: For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$, with only finitely many exceptions. — imported from google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/1094.lean at c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae, Apache-2.0); stated as the registry states it. Drafted by gate/tools/wave.py (F14-T11) and read by the curator before import (R13). -/

open scoped Nat

theorem Opn.erdos_1094 :
    {(n, k) : ℕ × ℕ | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite := by
  sorry
end C_c_bbeff8af

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, thisisanameforsure.

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