Open Proof Network

Problems / erdos-52 / review

Formalization review of erdos-52

“Copyright 2026 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.”

Opened 2026-10-13 by network (network) ; state: needs an intent signer · 1 candidate, 1 cluster, 16 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
16questions waiting
0open pair directions
0 / 16mutants 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-6c899a4a · 2026-10-13
Lean · c-6c899a4a.lean · sha256 6c899a4a782f
/-
Copyright 2026 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 52 — erdosproblems.com/52, imported from
google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/52.lean at
c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae, Apache-2.0), adapted to D-3's shape: the
registry states a yes/no question as `answer(sorry) ↔ P`; this states P, its affirmative
reading (F11-Q24). Listed, not claimable, at Stage 0. -/

open scoped Pointwise

theorem Opn.erdos_52 :
    ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (C : ℝ), 0 < C ∧ ∀ (A : Finset ℤ),
      (max (A + A).card (A * A).card : ℝ) ≥ C * (A.card : ℝ) ^ (2 - ε) := by
  sorry
curator — a model's: unnamed (other)ported from existing erdos-52surviving

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-6c899a4a}.

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-36c9bd6e), 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-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-b4a9e9ac), 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-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-1a00d42b), 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-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-e70a2784), 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-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-21476c69), 2026-10-14

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

  6. q-14 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-f4c24885), 2026-10-14

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

  7. q-15 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-36b65c5b), 2026-10-14

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

  8. q-16 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-2d5347f8), 2026-10-14

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

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

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

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

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

  11. 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-64d9b71c), 2026-10-14

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

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

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

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

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

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

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

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

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

  16. 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-6434cee8), 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 16 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-6c899a4ascreenpassnegation: nothing proved within the budget
c-6c899a4ascreenpassfalse: nothing proved within the budget
c-6c899a4ascreenpassstatement: nothing proved within the budget
c-6c899a4acompilepasselaborates at the pin; small cases do not apply: the claim is a closed proposition, not a predicate on n
Lean · e-a1753788.lean · sha256 838b7bf16c07
-- opn-review: {"cand": "c-6c899a4a", "op": "compile"}
import Mathlib

namespace C_c_6c899a4a
/-
Copyright 2026 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 52 — erdosproblems.com/52, imported from
google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/52.lean at
c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae, Apache-2.0), adapted to D-3's shape: the
registry states a yes/no question as `answer(sorry) ↔ P`; this states P, its affirmative
reading (F11-Q24). Listed, not claimable, at Stage 0. -/

open scoped Pointwise

theorem Opn.erdos_52 :
    ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (C : ℝ), 0 < C ∧ ∀ (A : Finset ℤ),
      (max (A + A).card (A * A).card : ℝ) ≥ C * (A.card : ℝ) ^ (2 - ε) := by
  sorry
end C_c_6c899a4a

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.