The algorithm Mathematica uses for its PrimeQ
function is described on MathWorld. That web page says PrimeQ
uses, "the multiple Rabin-Miller test in bases 2 and 3 combined with a Lucas pseudoprime test." It also says,
"As of 1997, this procedure is known to be correct only for all $n<10^{16}$, but no counterexamples are known and if any exist, they are expected to occur with extremely small probability (i.e., much less than the probability of a hardware error on a computer performing the test)."
More details on the algorithm are given in A Course in Computational Number Theory by David Bressoud. That book says there are 52,593 integers less than $10^{16}$ that are 2- and 3- strong pseudoprimes. It also suggests Lucas pseudoprimes less than $10^{16}$ are rare. Number theory is a very rigorous field. Has any rigorous work been done to substantiate the claim above that, if a PrimeQ
counterexamples exist, they are expected to occur with extremely small probability. All I can find so far is an extrapolation of the trend for ($n<10^{16}$), and that is a very hand-wavy argument.
Besides that, I am aware of no efforts to extend the brute force testing beyond $10^{16}$. With Moore's law and 15 years of work, considerable progress could have been made in that way.