In Number of digits in n!, now closed, there was a mention of Dmitry Kamenetsky's formula, $[\bigl(\log(2\pi n)/2+n(\log n-\log e)\bigr)/\log 10]+1$, for the number of decimal digits in $n$-factorial. Here, $[x]$ is the integer part of $x$. The formula appears at A034886 in the Online Encyclopedia of Integer Sequences, http://oeis.org/A034886. My question is whether this formula is exact for all $n$, or is it occasionally off. No proof of exactness is given at the OEIS, no paper of Kamenetsky appears in Math Reviews. 

In the other thread, I mentioned the discussion in the Usenet newsgroup sci.math in January-February, Subject: Number of digits in factorial. Although neither proof nor counterexample was found, I'd recommend looking over that discussion before starting in on this question. 

EDIT 11 Aug 2011: I note that the question also came up at m.se: question 8323, 30 Oct 2010.

A counterexample is $n_1 := 6561101970383$, with
$$
\log_{10} \left( (n_1/e)^{n_1} \sqrt{2\pi n_1} \right)
= 81244041273652.999999999999995102483 - \phantom; ,
$$
but
$$
\log_{10} (n_1!)
= 81244041273653.000000000000000618508 + \phantom;.
$$
If I computed correctly, $n_1$ is the first counterexample, and the only one up to $10^{13}$.  The computation should reach $10^{15}$ sometime next week, with a probability of about $1 - \exp(-\frac16) \sim 15\%$ of finding an $n_2$.

The computation (in gp/pari) took about 40 CPU hours here, compressed to 4 hours by running in parallel on 10 of the 12 heads of alhambra.math.harvard.edu .  This was not done by calculating $\log_{10} (n!)$ to enough precision for every $n \leq 10^{13}$, which would have taken hundreds of times longer.  The problem of finding nearly integral values of $\log_{10} (n!)$ is a special case of the "table maker's dilemma" (Wikipedia attributes this felicitous coinage to William Kahan); in this case, the linear-approximation technique suggested by Lefèvre at the bottom of page 15 of his slides takes time $\tilde O(N^{2/3})$ to find all examples with $n < N$.  That's what's running on alhambra now.

Along the way a few more terms of sequence A177901 turned up:
$252544447$,
$1430841730$,
$5042264463$,
$31774693500$,
$40752166709$,
$46787073630$,
$129532358256$,
$421559495894$,
$2418277169072$,
$6105111564681$,
and then $n_1 = 6561101970383$, which might even turn out to be the last term up to $10^{15}$ because $\log_{10} (n_1!)$ is so close to an integer (about $9$ times closer than necessary for our purpose).  [EDIT It's the last term $<10^{14}$ but not $10^{15}$, see below.]
The term $252544447$ was reported on math.se #8323 by Byron Schmuland [EDIT and a few months earlier by David Cantrell on sci.math], though it has not been posted to OEIS yet.  The further ones seem to be new, and I'll post them on OEIS soon.

Kamenetsky was right to suggest that the approximation should fail sometimes: in base 10, we expect $n$ to be a counterexample with probability about $1/cn$ with $c = 12 \log 10$, so on average each range $[N, 10^{12}N]$ should have about one.  Thus it is not surprising that the first one (past $n=1!$) turns out to have $13$ digits.  This heuristic is also the source of the estimate $1-\exp(-\frac16)$ for the probability of another counterexample in $ [10^{13}, 10^{15}]$.

UPDATE The calculation has now passed $10^{14}$, finding no new counterexample.  It did, however, find a new term for the OEIS sequence a bit beyond $10^{14}$: $n=125291661119688$, with $\log_{10}(n!)$ close to but just below the nearest integer $1711938609606982$ (where a counterexample must be a bit above), and also not quite as close as $1/(12n)$ — the difference is about $1/(8.4n)$.

While I'm at it: I should have mentioned that the gp/pari computation also found (in a minute or two) all the terms in $[10^4,10^8]$ listed by OEIS, which lends the new results some credibility; and I thank Gerry Myerson for drawing my attention to this question with his edit of about two weeks ago. 
