Assertions · Vela Mathematics Program
- Claim recorded6
- Evidence retained6
- Proposal recorded6
Claim ledger
At lean-proofs commit 423344341fbfdf4f8f684a302c5d05379125e7dc, Erdos94.variants.sum_multiplicity proves that for every finite planar point set P, the sum over its distinct determined distances of the unordered-pair distance multiplicities equals P.card.choose 2, matching Formal Conjectures commit 94a278e06a8bcbc2e4f2935e491c0c115ec832e0. For occurrence resolution only, the exact occurrence Erdos94.erdos_94.variants.sum_multiplicity is associated with problem:erdos:94 under resolver entity root sha256:32f6e98a826da23c12c7cfcb8853e4712de130136c59f0454bd115c3fdb1e6b1. That occurrence is one of four Erdős 94 declarations Formal Conjectures publishes, and this identity does not establish the cubic distance-multiplicity conjecture.
acceptedverification passed3 evidence spans6 conditions1 relationrevision 3theoreticalAuthenticated Submission vsb_2d10ba2ff1aff901vcl_6763ba247d40303408a268b226c3e27d7a753b63fca3eb0de99619d509346bfb
At lean-proofs commit 423344341fbfdf4f8f684a302c5d05379125e7dc, Erdos94.variants.sum_multiplicity proves that for every finite planar point set P, the sum over its distinct determined distances of the unordered-pair distance multiplicities equals P.card.choose 2, matching Formal Conjectures commit 94a278e06a8bcbc2e4f2935e491c0c115ec832e0. For occurrence resolution only, the exact occurrence Erdos94.erdos_94.variants.sum_multiplicity is associated with problem:erdos:94 under resolver entity root sha256:32f6e98a826da23c12c7cfcb8853e4712de130136c59f0454bd115c3fdb1e6b1. That occurrence is one of four Erdős 94 declarations Formal Conjectures publishes, and this identity does not establish the cubic distance-multiplicity conjecture.
supersededverification passed3 evidence spans7 conditions1 relationrevision 2theoreticalAuthenticated Submission vsb_d49869f07a7907d4vcl_4cae0d412a95d1965b927e1f7dbaa4245f5b9c3f84c5913e1d6a7880d6349165
At lean-proofs commit 423344341fbfdf4f8f684a302c5d05379125e7dc, Erdos94.variants.sum_multiplicity proves that for every finite planar point set P, the sum over its distinct determined distances of the unordered-pair distance multiplicities equals P.card.choose 2, matching Formal Conjectures commit 94a278e06a8bcbc2e4f2935e491c0c115ec832e0.
supersededno Verification Record2 evidence spans5 conditionstheoreticalAuthenticated Submission vsb_f43df4adcf653c88vcl_9ba852a45d8bc6f9dd024d85ff19e0b81317945f45e9eb073a89e44760a6b009
Under the retained exact public compiled-cache replay, Lean 4.22.0 elaborates the scoped Erdos 887 repaired source with the four expected sorry warnings.
acceptedverification passed1 evidence span5 conditionscomputationalAuthenticated Submission vsb_e804f60a8ffd8658
At Formal Conjectures commit 59f30aa314ba225fcd9268723ce8291616df1ab0, the Lean development starfleet/erdos-321 establishes a two-sided asymptotic bound on extremalSize, which denotes the same quantity as Formal Conjectures' Erdos321.R and therefore supplies a candidate answer for the exact occurrence Erdos321.erdos_321.variants.isTheta, not a proof of it. For occurrence resolution only, the exact occurrences Erdos321.erdos_321 and Erdos321.erdos_321.variants.isTheta are associated with problem:erdos:321 under resolver root sha256:a9d6787719c5c8069a9e14ade0f5a62975410272e6cd1583865b282d1d8669dd. At the exact retained Erdős 321 source revisions, the terminal theorem and structural comparison do not establish implication to either fixed Nat.log variant.
acceptedverification passed1 evidence span5 conditions1 relationrevision 2theoreticalAuthenticated Submission vsb_a72e375d5b327714vcl_b9c6915de55e15c69d06b9aeed786b0e632986374a347d77ff447ad244f67a2e
The Lean development starfleet/erdos-321 establishes a two-sided asymptotic bound on extremalSize, which denotes the same quantity as Formal Conjectures' Erdos321.R at pages commit 59f30aa3, and which therefore supplies a candidate answer for erdos_321.variants.isTheta rather than a proof of it.
supersededno Verification Record1 evidence span3 conditionstheoreticalAuthenticated Submission vsb_6cc500cc8153c8f5vcl_1da4282b752192c52c2a985476fc13bfe460da01e4fe26c5543b7acb37d8b120