qedbot

Erdős·erdos:973

Erdős Problem 973

problem formal record: solved source: openno 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.

Does the formal statement say what was claimed?

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

Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.

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

Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict 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.

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