Skip to content

Erdős problem 80

Erdős problem 80

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:8c823d621b7e1256c8e47c60a5f1c54c016a5507e6f27b2bab537f6f5f232067
Content
sha256:c369e1c1fbef20ee5ec8c24726fe952d10fddd544634c356a9dcc3b12f688d0b
Repository
sha256:a956b84c437202e5a02cc9e036a621bd14a302b34a75758115730bdbb77c52a4
Projection
sha256:c9d14c459c518937e758918b5897dc3b22f1a55f07739afe99502f5b046c907a
Source commit
2415f78e850aeee50afdca525c6f2e0ea606f207
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

Search problems.science

Find a Problem, Result, source, or page