Well known theorems that have not been proved I believe that there are numerous challenging theorems in mathematics for which only a sketch of a proof exists. To meet the standards of rigor, a complete proof of these theorems has yet to be established. Here is an example of a theorem that as far as I am aware fits into this category:

Theorem (Sullivan). A topological manifold of dimension $n\neq 4$ admits a unique Lipschitz structure.

The original paper of Sullivan [S] is a brief 13 pages note published in a conference proceeding. It contains a plethora of ideas, but hardly any proofs. Nevertheless the paper is a widely recognized as a source for the proof of the above result.
I am not the only one who struggled with this paper. Tukia and Vaisala [TV] wrote a 40 pages long paper whose aim was to understand some of the arguments on Sullivan. However they wrote in the introduction:
Since the presentation in [S] is very sketchy, a large part of this article is devoted to a fairly detailed exposition of Sullivan's theory. We take on faith the most difficult part, namely the existence of Sullivan groups.
I am reluctant to accept faith as a mathematical argument and so I am reluctant to accept that the paper [S] contains the proof of the theorem, so unless there is a detailed proof somewhere else, I think the above result is an example of a theorem that has not been proved yet. If I am wrong, please provide correct references.

Question. What are the other examples of such results?

[S] Sullivan, D.: Hyperbolic geometry and homeomorphisms. Geometric topology (Proc. Georgia Topology Conf., Athens, Ga., 1977), pp. 543–555, Academic Press, New York-London, 1979.
[TV] Tukia, P.; Väisälä, J.:
Lipschitz and quasiconformal approximation and extension.
Ann. Acad. Sci. Fenn. Ser. A I Math. 6 (1981), no. 2, 303–342 (1982).
 A: This is not meant to be an answer to the OP, but an explanation of the existence theorem for "Sullivan manifolds," which is the critical step omitted in the paper by Tukia and Väisälä. See also Remark 12 here. Sullivan manifolds are almost parallelizable compact $n$-dimensional hyperbolic manifolds.
The existence of "Sullivan manifolds" (in all dimensions) follows from the results in a paper by Boris Okun:
Okun, Boris, Nonzero degree tangential maps between dual symmetric spaces, Algebr. Geom. Topol. 1, 709–718 (2001). ZBL1066.53100.
Caveat 1. If you read Okun's paper, the result about hyperbolic manifolds is not stated anywhere. But his result implies that for every compact hyperbolic $n$-manifold $M$ there exists a finite-sheeted covering $M'\to M$ and a smooth degree 1 map $f: M'\to S^n$ such that $f^*(TS^n)=TM'$ (stably). Ideally, one should double check with Okun that my reading of his theorem is correct. From this, it follows that $M'$ is almost parallelizable (since $S^n$ is), i.e. removing a point from $M'$ results in a parallelizable manifold.
Caveat 2. Okun's paper (as well as Sullivan's original argument) depend critically on a paper by Deligne and Sullivan:
Deligne, Pierre; Sullivan, Dennis, Fibrés vectoriels complexes à groupe structural discret, C. R. Acad. Sci., Paris, Sér. A 281, 1081–1083 (1975). ZBL0317.55016.
The argument given in this 3-page paper is quite sketchy. However, a detailed proof is contained in Chapter 11 of
Friedlander, Eric M., Etale homotopy of simplicial schemes, Annals of Mathematics Studies, 104. Princeton, New Jersey: Princeton University Press and University of Tokyo Press. VII, 190 p. (1982). ZBL0538.55001.

A related MO question: Almost parallelizable hyperbolic manifolds
A: I am not sure whether this qualifies as "well-known".
Anyway, in set theory, in the study of the partition calculus (transfinite generalizations of Ramsey's theorem), effort centered for a while in studying relations of the form $$ \omega^m\to(\omega^n,k)^2 $$ for $m,n,k$ positive integers. Here, exponentiation is in the ordinal sense. This relation holds if and only if any graph on a set of vertices of order type $\omega^m$ either contains a complete subgraph with underlying set of vertices of order type $\omega^n$, or else it contains a copy of the empty graph on $k$ vertices (as an induced subgraph).
Results of the 50s and 60s "reduced" many of these questions to problems of finite combinatorics, all of which are algorithmically solvable (via completely unfeasible  algorithms, though). So, it was suspected that there was a general such reduction. This is what is shown in this paper:

MR0332507 (48 #10834) zbMATH 0384.05011
Milner, E. C.
A finite algorithm for the partition calculus. In Proceedings of the Twenty-Fifth Summer Meeting of the Canadian Mathematical Congress (Lakehead Univ., Thunder Bay, Ont., 1971), pp. 117–128. Lakehead Univ., Thunder Bay, Ont., 1971.

This is a very nice paper, with many examples and useful ideas. Unfortunately, it does not contain an algorithm, or a proof. With some effort, one can be extracted from the examples, which were very carefully chosen with this goal in mind but, as far as I am aware, neither an explicit description nor the relevant details have appeared in print. In fact, there are several results in the partition calculus that were announced decades ago but details were never published. (I have spent some time in recent years on a survey hoping to fix some of these gaps. The results I have checked are all correct, but it would sure be nice if we had proofs in the literature.)
