# Erdős Problem #662 — 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: verified_math/F-026_strict-shell-readings-counterexamples
Pinned formal statement: see check_answer/SOURCE_AUDIT.md + the four Research theorems listed in check_answer/README.md

## Verify from a cold start

```bash
bash check_answer/verify.sh
```

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