# Erdős Problem #267 — 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_1_pin_statement/lean
Pinned formal statement: workspace/experiments/experiment_1_pin_statement/lean/Research/Basic.lean

## Verify from a cold start

```bash
cd workspace/experiments/experiment_1_pin_statement/lean
lake exe cache get && lake --wfail build
```

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-267
