Plectis

Related problems

Related problems

Rendered from docs/RELATED_PROBLEMS.md in the public Lean repository. View source

Related Erdős problems

Where this work sits among the numbered problems it is near. Statuses are as listed on the individual problem pages (68, 249, 257, 1041, 1049, 69, 250, 258) in July 2026. The catalogue column preserves those dated classifications; the local-scope column and source links below describe this repository.

Bounded status route

The external catalogue status and the local release status are separate facts. Use the exact local packets before interpreting an analogy:

For a machine-first return from any indexed problem, run python3 scripts/query_corpus.py --route erdos_<n> for n in 68,243,249,251,257,269,1041,1049, then follow the complete eight-problem return matrix. That matrix binds each public status row to its strongest checked source, paper and TeX record, and exact open-obligation handles without changing the status or claim authority.

  • #249 target: python3 scripts/query_corpus.py --open remaining_open.erdos_249_irrationality; return to its problem-owned evidence with python3 scripts/query_corpus.py --route erdos_249.
  • #257 target: python3 scripts/query_corpus.py --open remaining_open.universal_257_all_infinite_supports; return to its problem-owned evidence with python3 scripts/query_corpus.py --route erdos_257.
  • #69 neighbour: python3 scripts/query_corpus.py --claim prime_support_irrationality
  • #250 neighbour: python3 scripts/query_corpus.py --claim sigma_transcendence

The first two packets are open; the latter two are cited only. A solved neighbour, shared transform, or formalised special case does not advance an open target unless docs/claims.json::machine_readable_paper.argument_graph records an advances_open_target edge.

Problem map

Problem Catalogue status Local relation class
#68 ∑n≥21/(n!−1) open problem-owned checked reductions and finite evidence
#249 ∑φ(n)/2n open open target
#257 ∑n∈A1/(2n−1) open open target with formalised special cases
#1041 short curves in polynomial lemniscates open ani’s exact Formal Conjectures refutation plus dynamical reductions
#1049 ∑1/(tn−1), rational t>1 open (rational t) Zudilin’s strict rational-base region theorem plus rational-base obstructions
#69 ∑ω(n)/2n solved (Tao–Teräväinen) cited-only solved neighbour plus formalised identity bridge
#250 ∑σ(n)/2n solved (Nesterenko 1996) cited-only solved neighbour
#258 ∑τ(n)/(a1⋯an) solved untouched analogy

Relation in this repository

  • #68 — the factorial-carry note routes to the exact FactorialZeroPlateau source: factorial-successor and carry frontiers, structural consumers, and a finite denominator exclusion; open boundary: produce cofinally many non-unit carries, not merely one finite miss.
  • #249 — the problem-owned paper note and canonical source map return the unconditional denominator exclusion and conditional reductions. The new squared-Lambert/GCD-moment family routes to the exact first-moment identity in GcdMomentCalculus; it is an identity with no irrationality consequence, so #249 remains open.
  • #257 — the problem-owned paper note and canonical source map return the named infinite-support cases and full support (A=N), not the universal statement.
  • #243 — the reciprocal-tail note and ReciprocalTailRigidity source exclude bounded negative-error regimes; open boundary: the unbounded mixed-sign/negative-excursion regime.
  • #251 — the prime-gap note and PrimeGapDyadicTail source expose the exact dyadic-tail machinery; open boundary: cofinally many adjacent small tail shifts at indices where prime gaps differ.
  • #269 — the running-lcm note and ThreePrimeRunningLcm source expose exact three-prime identities and a conditional residue-escape route; the rationality-to-carry bridge proves that rationality of the actual {2,3,5} series produces a positive reduced carry from an explicit onset. Open boundary: cofinal window escape for that actual orbit.
  • #1041 — ani’s degree-seven polynomial has a formalised Hausdorff-length refutation of the exact Formal Conjectures statement. This checks one polynomial; independent human review of correspondence with the 1958 wording is not recorded. The paper-facing route also checks Newton-flow ray separation and perturbation lemmas. The source-current frontier delta additionally routes the surviving hub-selection, near-Fekete, perimeter, inverse-sheet, and degree-five premise families through their exact public source notes; it also records the 2026-08-29 refutations that must not be rebuilt. The unrestricted topology, attachment-compatible selection, and metric gluing remain open. Use the machine result map and paper note together, keeping the source-only frontier separate from reviewed claim authority.
  • #1049 — Zudilin’s strict rational-base region theorem proves irrationality at a/b for natural 0<b<a satisfying ZudilinContourRegion a b, including every (31/4)r with positive natural r. The rational-base note and its checked source family — RationalBaseLambert for the 3/2 corridor and 7/2 height input, ZudilinHeightRegion for the 81/200 region, RationalPadeArithmetic and HermitePadeNoGo for finite Padé arithmetic and comparison, and QAperyDiagonalNonEquivalence for the moving-diagonal no-go, with ZudilinConeArithmetic covering the endpoint-unit common-divisor obstruction — route distinct arithmetic and obstruction mechanisms. The integer-base case b≥2 is irrational_erdosSum_full_support; open boundary: universal rational-base irrationality, irrationality at 3/2, the primitive noncollapsed construction, and analytic remainder control.
  • #69 — the prime-support case of #257; only the identity bridge to ∑p1/(2p−1) is formalised, not the irrationality.
  • #250 — the ladder neighbour L(Id); cited, not re-proved.
  • #258 — not addressed here; the monotone φ/σ sequel is the sibling territory of #249.

The one-line summary: formalised settled special cases, exact structural reductions and scoped no-go theorems across eight indexed problems, and finite certificates whose quantifiers are stated explicitly. The degree-seven counterexample found by the erdosproblems.com contributor ani refutes the exact Formal Conjectures statement of #1041 and its total-variation form, and is formalised here; the other seven problems remain open.