# Erdős Problem #320 — 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-038_two-sided-full-product-estimate/lean
Pinned formal statement: verified_math/F-038_two-sided-full-product-estimate/lean/ResearchPNT/FinalEstimate.lean

## Verify from a cold start

```bash
bash check_answer/verify-lean-theorem.sh verified_math/F-038_two-sided-full-product-estimate/lean ResearchPNT.FinalEstimate ResearchPNT.exists_two_sided_full_product_estimate
```

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