# Erdős Problem #415 — verification bundle

This bundle contains everything needed to independently verify the claimed
solution: the problem statement (problem.md), the checker/statement audit
(check_answer/), and the complete proof sources.

Primary proof location: workspace/experiments/experiment_3_adjacent_equal_density/lean
Pinned formal statement: workspace/experiments/experiment_1_formalize_patterns/lean/Research/Basic.lean (pinned F, patterns)

## Verify from a cold start

```bash
cd workspace/experiments/experiment_3_adjacent_equal_density/lean
lake exe cache get && lake build
cd ../../.. && grep -RnE '\b(sorry|admit)\b' workspace/experiments/experiment_3_adjacent_equal_density/lean --include='*.lean' && echo ESCAPE-FOUND || echo CLEAN
```

Requires Lean 4 (elan) — https://leanprover-community.github.io/get_started.html. `lake exe cache get` downloads the prebuilt Mathlib cache; the project's own files are then compiled and kernel-checked on your machine. The axiom audit must list only [propext, Classical.choice, Quot.sound].

Full run archive and report: https://www.starfleetmath.com/solutions/erdos-415
