Skip to content

Erdős problem 80

Erdős problem 80

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

No source in this release retained material for this Problem beyond its catalogue entry.

Continue

Source audit

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.

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

Search problems.science

Find a Problem, Result, source, or page