qedbot

Erdős·erdos:973

Erdős Problem 973

problem formal record: solved source: open F3 anchored

Machine-checked by Palomar.

Fidelity F3: The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.

analysis·Source

AI activity

How grades work

No AI contribution recorded against this statement.

Claimed on erdosproblems.com

1

Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.

Fidelity

How fidelity is graded

F3 anchored. The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.

Anchored to google-deepmind/formal-conjectures/blob/5d65ac9b140a00051fe2827fb10911beb2201b3b/FormalConjectures/ErdosProblems/973.lean

reviewed by an agent

Checks

1
  • verified·Palomar

    Registered by Palomar at 1571a487: Comparator confirmed 2 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel

    project registered at a pinned commit·2026-09-20·commit 1571a487465f

    PALOMAR-2026-09-20-000008

Declared by the projects

1

As each project's formalization.yaml states it.

Erdős 973: power sums cannot all be exponentially smalllinrock/math-proofs/erdos-973 · joined by anchor · Palomar

Read formalization.yaml

authors
Linmiao Xu
method
agent
review
agent-reviewed
results
2 main results named, checked with Comparator
sources
Residual bounds for Schur-stable polynomials — formalizes; Exterior power sums — independently-proves; Erdős Problem 973: exterior power sums — background; Some recent advances and current problems in number theory (1965) — background
related
google-deepmind/formal-conjectures/blob/5d65ac9b140a00051fe2827fb10911beb2201b3b/FormalConjectures/ErdosProblems/973.lean — adapts; miracleqihe/Erdos-973_solution_check-by-Lean — independent
checked by
Palomar

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 1
Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 3
  • https://www.erdosproblems.com/973
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/973.lean
  • FormalConjectures/ErdosProblems/973.lean

Cite this record

qed.bot, “Erdős Problem 973”, https://qed.bot/s/erdos-973, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.