Skip to content

Erdős problem 80

Start work

No written statement is retained for this problem.

How the state got here

0 of 6 recorded
  1. Prior stateNone retained
  2. WorkNo submitted work retained
  3. VerificationNo check retained
  4. DecisionNo Repository has decided
  5. StandingNothing recorded here
  6. Next gapNot recorded

Result history

Published changes, performers, checks, and later corrections.

No result history yet
No proposed change is retained for this Problem, so there is nothing to show a decision on.

Correction history

No correction history

Technical detailsExact roots, source, and retained record identifiers

Exact provenance

Problem row
sha256:bc904392846098ed5491ec571abe2332ea798bc0e037a0fc9a3929741f315649
Metadata
sha256:38843f4343be67d1bbfad1011b3da5d4f8bf718d2cf86959170b9e87d7602dc5
Observation
sha256:9c8326e865b6017b103af7611c852a06776d81964979b8ab5a1b800cd550dff6
Content
sha256:c369e1c1fbef20ee5ec8c24726fe952d10fddd544634c356a9dcc3b12f688d0b
Repository
sha256:a956b84c437202e5a02cc9e036a621bd14a302b34a75758115730bdbb77c52a4
Projection
sha256:a4a96441668a9f8b33afbcb3f696a2639f5fae145f36ddc063d7f67d5fb87ce8
Source commit
36c6d0fef71a3fec84d9dcd5eeca4e22e378f7cb
Upstream sourceInspect recordsSource JSON

Source review

1 exact matching record

Native pull-request state, mechanical checks, semantic findings, and artifact availability are separate source facts. None is a Vela Verification, Decision, or change to Math Standing.

Formal Conjectures PR #4830

FormalConjectures/ErdosProblems/80.lean

PR mergedreview approvedsource audit: needs revision
failsemantic

hypothesis satisfiability

At exact PR 4830 head e2e2a606/blob 9dd6a993, Admissible requires c*n^2 edges in a simple n-vertex graph while the theorem quantifies over every c>0.

Witness: At c=2 and n=100 the hypothesis needs 20000 edges, but a simple graph has at most 4950; the admissible set is empty and sInf is 0.

Limit: The witness establishes the vacuity defect at the stated parameter, not a replacement theorem.

Open upstream PROpen Problem 80head e2e2a6064b

Read-only projection

Approval and merge remain upstream PR state. A passing build does not establish semantic fidelity. An unavailable artifact identity is not a proof failure.

Adapter conformance 9 / 9: exact source revision, bounded complete reads, typed roots, custody, implementation identity, reconstructibility, unsupported-state refusal, rights, and lifecycle semantics.

Web read projection
sha256:ca753f3b6ad07fd62ef1035ae56de1646cb2133dd1705f991bf29a2bd7da2780
Math source projection
sha256:1a90cbe1732e21e730753a12e6b3b1ecbd3e0019a287a5ba001c9a9fdccf881b
Adapter profile
sha256:6491df603d880f00dc7e69cb0817fda1a0d903efee3812c5af3c7b3e02773303
Adapter contract
sha256:5de25828202d0682f8ac39c2e58e5d9ed7a3f0474910d77c1c4e641a08543615
Inspect exact Math projection
View complete five-record source audit