# Reproducing the Erdős 1189 Lean build

The attached archive `erdos1189_lean_source.tar.gz` contains the complete
source project: `lakefile.toml`, pinned `lake-manifest.json`, `lean-toolchain`,
`Research.lean`, and every `Research/*.lean` module.

```bash
mkdir erdos1189-lean && cd erdos1189-lean
tar -xzf ../erdos1189_lean_source.tar.gz
lake exe cache get          # fetch pinned Mathlib oleans
LEAN_NUM_THREADS=8 lake build
lake env lean Research/FinalClaimsAudit.lean
```

`lake build` builds the aggregate `Research` target, including
`Research.FinalClaims`. The audit command prints each final theorem followed
by `#print axioms`; the expected only axioms are Mathlib's standard
`propext`, `Classical.choice`, and `Quot.sound`.

The count theorem intentionally exposes `BBMSTLowerDatum` and
`BBMSTUpperHypothesis`, because BBMST's published asymptotic enumeration is an
external mathematical input. The maximum, minimum, reciprocal, and divisor
infinitude final theorems have no external hypotheses.
