Skip to content

Proposed changes · Vela Mathematics Program

Proposed change evidence

6 proposed changes · 6 Checks · none pending

Proposal

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.

Proposal accepted

Scoped Verification

2 pass

2 Verification Records · declared independent of agent:submission-v3-cleanup · 7 stated limits

first pass reported in 7m

Agent Decision

Accept the byte-identical Erdős 94 assertion as the current Submission v3 revision after two scoped actor-separated fidelity reviews. This removes only the obsolete recovery caveat, preserves the exact occurrence mapping and every scientific limit, and adds no new validation.

Aug 18, 2026, 6:46 PMagent:submission-v3-cleanup-decisionwork sessioncodex:019fe903-28b7-73d1-bd26-bdd9a083c1a4signed record

Repository authority local:device-sha256:67fbb8e56377e6868e9f941524e0bf39cfb4fd2a4bfdd25c2edb93fc82f86213|uid:501

Decision recorded in 8m

Proposal

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.

Proposal accepted

Scoped Verification

2 pass

2 Verification Records · declared independent of agent:submission-v3-migration · 8 stated limits

first pass reported in 8m

Agent Decision

Accept the exact current Erdős 94 assertion in the compact v3 lineage after independent scoped checks of occurrence mapping and correction scope. Preserve the correction and all nonclaims without changing the scientific assertion.

Aug 17, 2026, 6:48 PMagent:submission-v3-migrationsigned record

Repository authority local:device-sha256:67fbb8e56377e6868e9f941524e0bf39cfb4fd2a4bfdd25c2edb93fc82f86213|uid:501

Decision recorded in 8m

Proposal

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.

Proposal accepted

Scoped Verification

No Verification Record is retained.

Agent Decision

Re-admit the exact intended Erdős 94 predecessor assertion only to preserve current correction truth in the compact v3 lineage. Its pre-v3 distance-multiplicity Verification remains recoverable at the signed rollback ref and is not re-attested over new bytes.

Aug 17, 2026, 6:35 PMagent:submission-v3-migrationsigned record

Repository authority local:device-sha256:67fbb8e56377e6868e9f941524e0bf39cfb4fd2a4bfdd25c2edb93fc82f86213|uid:501

Decision recorded in under a minute

Proposal

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.

Proposal accepted

Scoped Verification

1 pass

1 Verification Record · no independence declared · 1 stated limit

first pass reported in under a minute

Agent Decision

Accept the exact current bounded Erdős 887 replay assertion in the compact v3 lineage after a scoped fidelity check; this does not claim a proof or independent reproduction.

Aug 17, 2026, 6:34 PMagent:submission-v3-migrationsigned record

Repository authority local:device-sha256:67fbb8e56377e6868e9f941524e0bf39cfb4fd2a4bfdd25c2edb93fc82f86213|uid:501

Decision recorded in 1m

Proposal

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.

Proposal accepted

Scoped Verification

1 pass

1 Verification Record · no independence declared · 1 stated limit

first pass reported in under a minute

Agent Decision

Accept the exact current Erdős 321 assertion in the compact v3 lineage after a scoped fidelity check; preserve the correction relation and limitations without changing the scientific content.

Aug 17, 2026, 6:33 PMagent:submission-v3-migrationsigned record

Repository authority local:device-sha256:67fbb8e56377e6868e9f941524e0bf39cfb4fd2a4bfdd25c2edb93fc82f86213|uid:501

Decision recorded in 1m

Proposal

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.

Proposal accepted

Scoped Verification

No Verification Record is retained.

Agent Decision

Re-admit the exact intended Erdős 321 predecessor assertion into the compact prelaunch v3 lineage so its current correction remains explicit; this migration Decision does not change the scientific assertion.

Aug 17, 2026, 6:32 PMagent:submission-v3-migrationsigned record

Repository authority local:device-sha256:67fbb8e56377e6868e9f941524e0bf39cfb4fd2a4bfdd25c2edb93fc82f86213|uid:501

Decision recorded in under a minute

Search problems.science

Find a Problem, Result, source, or page