He visto tanto contraejemplos como pruebas de "compacto implica compacto secuencial", y no estoy seguro de lo que está pasando.
Aparentemente hay espacios compactos que no son secuencialmente compactos; una rápida búsqueda en Google y consultas en Wikipedia revelarán ejemplos que rondan; tienden a ser variantes de $[0,1]^{[0,1]}$ con la topología del producto. Aquí hay una demostración(?):
$[0,1]^{[0,1]}$ es compacto por el teorema de Tychonoff. Entonces, demostramos la falta de compacidad secuencial.
Elija una representación binaria única para cada $x\in [0,1]$.
Para cada $n\in\mathbb{N}$, sea $f_n : [0,1]\to[0,1]$ (un elemento de $[0,1]^{[0,1]}$) la función que asigna a cada $x$ el dígito de su expansión binaria en la posición $n$.
Sea $f_{n_k}$ una subsecuencia de esta secuencia.
Sea $x'\in [0,1]$ tal que el dígito $n_{2m}$ es $0$ y el dígito $n_{2m+1}$ es $1$, para todo $m\in\mathbb{N}$.
Entonces $f_{n_k} (x')$ no converge (alterna entre $0$ y $1$), y por lo tanto $f_{n_k}$ no puede converger.
Así que hemos encontrado una secuencia en $[0,1]^{[0,1]}$ sin ninguna subsecuencia convergente y por lo tanto no es secuencialmente compacta.
(Aparte: aparentemente esto se basa en un ejemplo en Contraejemplos en Topología de Steen, según http://ncatlab.org/nlab/show/sequentially+compact+space)
No obstante, también hay algunas pruebas(?) flotando alrededor de que la compacidad de un espacio implica compacidad secuencial, siguiendo estas líneas (esta prueba(?) es de la contrapositiva):
Supongamos que $X$ no es secuencialmente compacto.
Por definición, esto significa que hay alguna secuencia $(x_n)$ sobre $X$ sin ninguna subsecuencia convergente.
Si algún $x\in X$ tuviera para cada uno de sus vecindarios $U$ infinitos $n$ para los cuales $x_n \in U$, entonces podríamos definir una subsecuencia convergente de $(x_n)$, contradiciendo nuestra suposición. (Presumiblemente esto se hace eligiendo para cada vecindario un término de índice suficientemente grande en ese vecindario.)
Por lo tanto, para cada $x \in X$ podemos seleccionar un conjunto abierto $U_x$ tal que $x\in U_x$ pero con $x_n \in U_x$ para solo finitos $n$.
La colección $\mathcal{U}=\{U_x : x\in X\}$ es claramente un recubrimiento abierto de $X$.
Si $\mathcal{U}$ tuviera un subrecubrimiento finito $\{U_1, \dots, U_k\}$ entonces la unión $U_1 \cup \cdots \cup U_k$ contendría todo $X$ pero solo contenería $x_n$ para finitos $n$, lo cual es imposible.
Por lo tanto $X$ no es compacto, ya que hemos encontrado un recubrimiento abierto sin un subrecubrimiento finito.
(Aparte: esta prueba es esencialmente la misma que la prueba que aparece en Principios de Análisis Matemático de Rudin para el Teorema 2.37 de que los subconjuntos infinitos de espacios compactos tienen puntos límite.)
Entonces, ¿qué está pasando aquí? No puede ser que tanto el contraejemplo como la prueba nos estén diciendo algo correcto. ¿Hay algún defecto sutil (o más embarazoso para mí - flagrante) en la prueba?