# Erdős Problem #1189 — 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/shared/erdos1189_lean_source.tar.gz (complete pinned Lean project)
Pinned formal statement: Research/FinalClaimsAudit.lean inside the pinned project; workspace/shared/LEAN_REPRODUCE.md documents the exact steps. The count theorem carries the published BBMST enumeration as explicit named hypotheses (BBMSTLowerDatum/BBMSTUpperHypothesis); the max/min/reciprocal/divisor theorems have no external hypotheses.

## Verify from a cold start

```bash
mkdir erdos1189-lean && cd erdos1189-lean && tar -xzf ../workspace/shared/erdos1189_lean_source.tar.gz
lake exe cache get && lake build
lake env lean Research/FinalClaimsAudit.lean
cd ../check_answer && cargo test --release && cargo run --release -- fixtures/classic_k5.txt
```

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