Is $\ 7!=5040\ $ the largest highly composite factorial? A highly composite number is a natural number $\ n\ge 1\ $ that has more divisors than any smaller natural number $\ m\ge 1$.
Checking the $\ 1000\ $ entries in the OEIS-sequence, I noticed that only the following factorials are highly composite :
$$[1, 2, 6, 24, 120, 720, 5040]$$

Is it known whether $\ 7!=5040\ $ is the largest highly composite factorial ?

The factorials have some conditions necessary for a number to be highly composite :


*

*They contain the first $k$ prime numbers as prime factors.

*The exponents are non-increasing.

*The exponent corresponding to the largest prime factor is $\ 1$.


So, it is not obvious whether the above list is complete.
 A: Yes, it is known. If you look at the number of divisors function, a number $n$ with prime factorization $p_1^{a_1}p_2^{a_2}p_3^{a_3}\ldots$ has $\sigma_0(n)=(a_1+1)(a_2+1)(a_3+1)\ldots$ divisors.  The factorials have too many small factors.  Every time you multiply by a prime you double the number of divisors, but when you increase the power of $2$ from $n$ to $n+1$ you only multiply the number of divisors by $\frac {n+2}{n+1}=1+\frac 1{n+1}$.  The greedy algorithm for finding highly composite numbers would look at $\log \sigma_0(n)$.  If you multiply $n$ by a prime $p$ that is currently in the factorization of $n$ as $p^a$ you add $\log 1+\frac 1{a+1}$ to the log of the number of factors and you add $\log p$ to the log of $n$, so the benefit/cost ratio of each increase is $\frac {\log 1+\frac 1{a+1}}{\log p}$  Search over the primes, find the best, and that is your next multiplier.  When you look at OEIS A002182 not every entry is a multiple of the previous one, but you see there are too many small factors among the factorials.  $n!$ has about $\frac n2$ factors of $2$, for example.  To really justify this you need to use the prime number theorem to show how large the next prime will be, then show you want to use it before $n!$ will.  You can find a finite limit of factorials that are candidates, then check them.
A: Suppose $n \ge 20$. Trivially, $n!$ is then divisible by $16$, so $\dfrac{13}{16}n!$ is an integer smaller than $n!$.
Let the prime factorization of $n!$ be $n! = 2^{e_1}3^{e_2}\cdots11^{e_5}13^{e_6}17^{e_7}\cdots p_r^{e_r}$. 
Then the prime factorization of $\dfrac{13}{16}n!$ is $\dfrac{13}{16}n! = 2^{e_1-4}3^{e_2} \cdots11^{e_5}13^{e_6+1}17^{e_6}\cdots p_r^{e_r}$.
Then, the number of divisors of $n!$ is $\sigma_0(n!) = (e_1+1)(e_6+1)\displaystyle\prod_{k \neq 1,6}(e_k+1)$ and the number of divisors of $\dfrac{13}{16}n!$ is $\sigma_0(\dfrac{13}{16}n!) = (e_1-3)(e_6+2)\displaystyle\prod_{k \neq 1,6}(e_k+1)$. 
Hence, $\sigma_0(\dfrac{13}{16}n!) > \sigma_0(n!)$ iff $(e_1-3)(e_6+2) > (e_1+1)(e_6+1)$ iff $e_1 > 4e_6+7$. 
Using the well known formula for the largest power of a prime dividing a factorial, we have 
$e_1 = \displaystyle\sum_{k = 1}^{\left\lfloor \log_2 n\right\rfloor}\left\lfloor \dfrac{n}{2^k} \right\rfloor  > \displaystyle\sum_{k = 1}^{\left\lfloor \log_2 n\right\rfloor} \left(\dfrac{n}{2^k} - 1\right) \ge n - \dfrac{n}{2^{\left\lfloor \log_2 n\right\rfloor}} - \left\lfloor \log_2 n\right\rfloor \ge n - 2 - \log_2 n$.
Similarly, $e_6 = \displaystyle\sum_{k = 1}^{\left\lfloor \log_{13} n\right\rfloor}\left\lfloor \dfrac{n}{13^k} \right\rfloor \le \displaystyle\sum_{k = 1}^{\left\lfloor \log_{13} n\right\rfloor}\dfrac{n}{13^k}  \le \dfrac{n}{12}$. Hence, $4e_6+7 \le \dfrac{n}{3}+7$. 
I'll leave it as an exercise to show that $\dfrac{n}{3}+7 < n - 2 - \log_2 n$ holds for all integers $n \ge 20$. 
Therefore, for all integers $n \ge 20$, we have $4e_6+7 \le \dfrac{n}{3}+7 < n - 2 - \log_2 n < e_1$, and thus, $\sigma_0(\dfrac{13}{16}n!) > \sigma_0(n!)$. 
So, $n!$ is not highly composite for $n \ge 20$. Now, it remains to check if any factorials between $7!$ and $20!$ are highly composite.
EDIT: From the list of the first 1000 highly composite numbers that OP mentioned, it appears that the $149$-th largest highly composite number is $\approx 1.49 \times 10^{17}$, while $19! \approx 1.22 \times 10^{17}$. None of  the numbers $8!, 9!, \ldots, 19!$ appear in that list, so $7!$ is indeed the largest highly composite factorial.
