SIGNIFICANCE

Checked 2026-08-23 · source current · v1

Evan Beller · ErdősProblems.com #132

What is claimed?

The submission claims a proof of the first assertion of Erdős Problem #132 for n = 8: every eight-point planar set has two distinct distances occurring at most eight times.

Quoted from the source · b4ller · 2026-08-23 · View source

Component dates
Preprint
Not recorded
Exposition
Not recorded
Formalization
2026-08-23

Component dates (preprint / exposition / formalization). Formalization date from the artifact reported by the source. “Not recorded” means no dated source is recorded for that component. Preprint dates refer to the pinned manuscript version.

Reader summary

Claimed
A public proof claim says the n = 8 case of the first assertion of Problem #132 is proved. It is not a claim to resolve the general problem.

Reader summary · Significance · 2026-08-23

What has been checked?

Significance inspected the proof-claim page, downloaded the linked proof PDF, and recorded the linked formalization repository and its public commit.

Reader summary · Significance · 2026-08-23

Independent reruns
0
Math assessments
0
Written reviews
0

Where is help needed?

Significance has not assessed the geometric deduction, the cited classification results, the Lean correspondence, or the finite computation.

Reader summary · Significance · 2026-08-23

See 2 open checks →

Problem link

ErdősProblems.com #132 · open the original problem page

Quoted from the source · Significance editor · 2026-08-23 · View source

Author involvement

Evan Beller reviewed the rendered draft and confirmed the scope, description, and two proposed checks on 2026-08-24.

Record note · b4ller · 2026-08-24

Start here · for reviewers

Main deduction

Check the (9,9,9,1) multiplicity reduction, the two seven-point deletions, and the overlap-rigidity contradiction.

The proof PDF; formalization directory · The claim identifies the profile reduction and overlap-rigidity lemma as the central route. · Quoted from the source · b4ller · 2026-08-23 · View source

Risk points

  • Check that the cited classification of seven-point three-distance sets applies exactly to each deletion.

    Proof PDF, deletion and classification argument · Significance’s interpretation · Significance editor · 2026-08-23

  • Check the overlap-rigidity lemma and the contradiction from the two distinct diameter endpoints.

    Proof PDF, overlap-rigidity lemma · Quoted from the source · b4ller · 2026-08-23 · View source

Useful background

  • The Hopf–Pannwitz diameter bound, basic distance multiplicity counting, and the cited seven-point classification.

    Proof PDF references and introduction · Significance’s interpretation · Significance editor · 2026-08-23

Needs checking

  • Reconstruct the finite n = 8 argument and compare the Lean declarations with the informal statement. — The public claim reports formal verification conditional on cited literature inputs; no independent check is recorded.

    Proof PDF and formalization directory · Quoted from the source · b4ller · 2026-08-23 · View source

  • Suggest another focused check
Copy for sharing

Copy and paste this summary.

A public proof claim says the n = 8 case of the first assertion of Problem
#132 is proved. It is not a claim to resolve the general problem.

Checked: Significance inspected the proof-claim page, downloaded the linked
proof PDF, and recorded the linked formalization repository and its public
commit.

Not checked: Significance has not assessed the geometric deduction, the
cited classification results, the Lean correspondence, or the finite
computation.

As of 2026-08-23T19:11:00Z (freshness: current)
Full record: https://hjyuh.github.io/significance/2026-evanbeller-erdos-132/
Significance records evidence. It does not judge the mathematics.
Scope
This is only the n = 8 case of the first assertion; the general problem remains open. Quoted from the source · b4ller · 2026-08-23 · View source
Source
Erdős Problem #132, n = 8 proof writeup · github-EvanBeller-erdos-132-ffd0920dedff01f04f1c605754384a6a5207f662 · retrieved 2026-08-23T19:11:00Z
sha256 5d3faea03531…

Evidence: 2 entries

  1. Source inspection

    ev-source-inspection

    Public-source and version check only. This is not a mathematical review.

    The public proof-claim page and its linked PDF and formalization repository were inspected. This is source inspection, not a mathematical review.

    Significance’s interpretation · Significance editor · 2026-08-23 · View source

  2. Formal code published by the source

    ev-formalization-reported

    Published by the source. Any independent rerun appears as a separate entry.

    The claim page links a Lean formalization directory. No independent build receipt is recorded here.

    Open link @ ffd0920dedff… · Quoted from the source · b4ller · 2026-08-23 · View source

Plain-language explanation

This is a bounded n = 8 result, not a solution of the general distance problem. A reader can begin with the multiplicity profile and the two deletion arguments.

Explanation · Significance

Limits of this record
  • This record does not issue a whole-paper correctness judgement.
  • Open invitations identify work not yet represented by a completed evidence entry.
  • No independent reproduction or mathematical assessment is represented unless an evidence entry above says otherwise.