@Theo, sin duda en el año transcurrido desde que respondiste a esta pregunta, alguien que puede producir notas tan impresionantes habría conseguido todos los detalles de una respuesta exhaustiva ordenada, pero mi propia prueba de Lie III de mi propia exposición próxima sobre la teoría de Lie, por lo que vale, es básicamente una vuelta en su cabeza de la prueba de que dos grupos de Lie simplemente conectados son isomorfos y se ejecuta aproximadamente como sigue. Una vez que tenemos el grupo de Lie local, formamos el conjunto de todos los productos formales de la forma $\gamma = \Pi_j \exp\left(X_j(\tau)\right)$ donde $X_j(\tau)$ son un $C^1$ caminos en el grupo de Lie local, por supuesto lo suficientemente pequeños como para que la CBH se aplique a todos los pares de sus productos. Entonces se puede demostrar que todas las deformaciones continuas de este camino a través del conjunto de productos formales se pueden escribir, gracias a la fórmula de Hadamard, como $\Pi_j \exp\left(X_j(\tau)\right) \Pi_j \exp\left(\delta X_j(\tau)\right)$ es decir, se puede barajar toda la variación a un extremo del producto. Ahora restringe las variaciones $\delta X_j$ sea lo suficientemente pequeño como para que la fórmula CBH se aplique a cada etapa del producto n-fold $\Delta = \Pi_j \exp\left(\delta X_j(\tau)\right)$ . Así, aunque no hayamos definido rigurosamente el "valor" del producto formal, ahora tiene sentido el concepto de pequeñas variaciones continuas, pero finitas, de la trayectoria que dejan inalterado el "valor" del producto formal: es cualquier variación tal que, calculada por CBH, $e = \Delta = \Pi_j \exp\left(\delta X_j(\tau)\right)$ donde $e$ es la identidad del grupo. Así que ahora podemos definir dos de nuestros productos formales como equivalentes si se puede encontrar una secuencia finita de pequeñas variaciones continuas que dejen el "valor" de los productos sin cambios, en el sentido definido anteriormente, que deforme paso a paso un producto formal al otro. De este modo, condensamos el gran conjunto de productos formales en sus clases de equivalencia, modulando la equivalencia que acabamos de definir. Este enfoque hace dos cosas: $\mathbf{(i)}$ elimina cualquier incoherencia que pueda surgir por el hecho de que un elemento tenga muchas representaciones potenciales como productos formales diferentes y $\mathbf{(ii)}$ el conjunto de clases de equivalencia, ya que un conjunto de clases de homotopía es simplemente conectado por construcción. Así que ahora sólo tenemos que comprobar que esta bestia es un grupo de Lie y hemos terminado: en mi exposición esto es fácil, porque uso esencialmente una inversa del Satz 1 de Freudenthal de 1941 "Die Topologie der Lieschen Gruppen Als Algebraisches Phanomen. I" para definir un grupo de Lie - demuestro que uno puede tomar esencialmente las propiedades enumeradas en el teorema de Freudenthal, usarlas como axiomas y mostrar que un grupo que es una variedad simplemente conectada se construye a sí mismo a partir de ellas. Lo que hemos hecho, por supuesto, es construir el único grupo de Lie simplemente conexo que tiene el álgebra de Lie "de entrada" a nuestra demostración".
Creo que mi enfoque es algo parecido al de las conferencias de J.P. Serre de 1964 citadas en la primera respuesta.
