Open Proof Network

Problems / erdos-51 / review

Formalization review of erdos-51

“Is there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$, there is an integer n such that $\phi(n)=a$, and yet if $n_a$ is the smallest such integer, then $\frac{n_a}{a} → \infty$ as $a → ∞$?”

Opened 2026-10-13 by network (network) ; state: needs an intent signer · 1 candidate, 1 cluster, 5 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
5questions waiting
0open pair directions
0 / 5mutants 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-b79d40a0 · 2026-10-13
Lean · c-b79d40a0.lean · sha256 b79d40a0e3c6
/-
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 51: Is there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$, there is an integer n such that $\phi(n)=a$, and yet if $n_a$ is the smallest such integer, then $\frac — imported from google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/51.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 Filter
open scoped Nat

theorem Opn.erdos_51 :
    ∃ A : Set ℕ, ∃ n : A → ℕ,
      A.Infinite ∧
      (∀ a : A, IsLeast (φ ⁻¹' {(a : ℕ)}) (n a)) ∧
      Tendsto (fun a : A => (n a : ℝ) / (a : ℝ)) atTop atTop := by
  sorry
curator — a model's: unnamed (other)ported from existing erdos-51surviving

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-b79d40a0}.

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

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

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

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

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

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

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

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

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

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

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 5 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-b79d40a0screenpassnegation: nothing proved within the budget
c-b79d40a0screenpassfalse: nothing proved within the budget
c-b79d40a0compilepasselaborates at the pin; small cases do not apply: the claim is a closed proposition, not a predicate on n
Lean · e-41f7b09d.lean · sha256 d1717ca0a400
-- opn-review: {"cand": "c-b79d40a0", "op": "compile"}
import Mathlib

namespace C_c_b79d40a0
/-
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 51: Is there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$, there is an integer n such that $\phi(n)=a$, and yet if $n_a$ is the smallest such integer, then $\frac — imported from google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/51.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 Filter
open scoped Nat

theorem Opn.erdos_51 :
    ∃ A : Set ℕ, ∃ n : A → ℕ,
      A.Infinite ∧
      (∀ a : A, IsLeast (φ ⁻¹' {(a : ℕ)}) (n a)) ∧
      Tendsto (fun a : A => (n a : ℝ) / (a : ℝ)) atTop atTop := by
  sorry
end C_c_b79d40a0
c-b79d40a0screenpassstatement: 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: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

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