Formalize the Smarandache–Wellin prime infinitude conjecture

[derekste]

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
• OEIS A019518
• OEIS A069151
• OEIS 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

• ams-11

Choose either option

• 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

[derekste]

Could a maintainer please add the new conjecture label? I do not have permission to add
repository labels.