Formalize the Smarandache–Wellin prime infinitude conjecture

### What is the conjecture

The Smarandache–Wellin numbers are formed by concatenating the decimal expansions of consecutive
primes:

$$2,\ 23,\ 235,\ 2357,\ 235711,\ 23571113,\ldots$$

The University of New Mexico's Smarandache problems page states:

> There are infinitely many primes in the smarandache concatenated prime sequence.

The page marks the statement “Not proved yet.” OEIS A019518 defines the underlying sequence,
A069151 records its prime values, and A046035 records the indices at which those values are prime.

References:

- [Smarandache Problems](https://fs.unm.edu/S-PROBL.HTM)
- [OEIS A019518](https://oeis.org/A019518)
- [OEIS A069151](https://oeis.org/A069151)
- [OEIS A046035](https://oeis.org/A046035)

### Prerequisites needed

Mathlib's decimal-digit operations, natural-number exponentiation, the `Nat.nth Nat.Prime` prime
enumeration, primality predicate, and infinite-set API are sufficient. No addition to
`FormalConjecturesForMathlib` is expected.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

- ams-11

### Choose either option

- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by locating the repository's existing Lean conjecture statements and reviewing the decimal-digit operations, natural-number exponentiation, Nat.nth Nat.Prime, primality predicate, and infinite-set API mentioned in the issue. Formalize the Smarandache–Wellin prime infinitude conjecture, with the statement matching the cited sequence and references; the issue says no addition to FormalConjecturesForMathlib is expected.

Written by the indexing model from the issue text.