Add a machine-checked barrier (lower bound) for Erdős Problem 307

`ErdosProblems/307.lean` currently states the open problem and its coprime variants. I have a `sorry`-free Lean 4 (Mathlib) formalization of a **lower bound** on any solution: at least 59 primes in total, and `(∏ P)² ≥ 4·10¹¹²` (so `∏ P ≥ 2·10⁵⁶`).

I'd like to add it to that file as a `@[category research solved, AMS 11]` theorem with the proof hosted in my own repository and linked via `@[formal_proof using lean4 at …]`, following the pattern in `ErdosProblems/26.lean`. The main `erdos_307` statement stays `research open` and untouched.

- Proof + paper: https://github.com/ElVec1o/erdos307 (archived: https://doi.org/10.5281/zenodo.20684626)
- The proof builds on Lean v4.30; only the *statement* would live here (built by CI under v4.27). The linked `Closed.lean` (tag `v1.0.0`) proves both conjuncts sorry-free (`card_ge_59`, `erdos307_barrier_closed`); axioms `propext, Classical.choice, Quot.sound` + a `native_decide` evaluation of the first 59 primes.

I'll open a PR alongside this issue. Happy to reshape it however you prefer — standalone theorem vs. a reference on `erdos_307`. Thanks!