(Disclaimer: I'm no expert in homotopy theory nor in higher categories!) If I understand it correctly, Grothendieck's homotopy hypothesis states that there should be an equivalence (of $(n+1)$-categories) between "homotopy $n$-types" and $n$-groupoids. Where, by "homotopy $n$-types" is probably meant the $(\infty,n+1)$-category that has (nice) topological spaces with vanishing homotopy groups above the $n$-th as objects, and higher morphisms given by homotopies and homotopies-between-homotopies etc. And by "$n$-groupoid" is probably understood $(\infty,n)$-groupoid.
Edit: the homotopy types probably are defined to be some localization of the thing I stated above?
To which extent has the homotopy hypothesis been proved? By "proved" I mean precise statements and rigorous proofs, not just "philosophical" evidence; and not "tautological" solutions in which homotopy types are defined to be $\infty$-groupoids in the first place.
All this fits in the context of Whitehead's algebraic homotopy programme
Which is the present status of that programme, both in the sense of formalization and of proof?
How can any advance in the programme be made at all if Grothendieck's conjecture is not fully proven first?
Best Answer
The problem is that the question is highly dependent on the definition of $n$-groupoids. The notion of strict $n$-groupoid is very clear and precise but we know very well (and Grothendieck knew that) that the homotopy hypothesis is false if we only use strict groupoids.
One needs to use weak $n$-groupoids (where for example composition is associative up to isomorphism and so one). But there is not a unique definition of what an $n$-groupoids is. There are plenty of non-equivalent definitions, which are supposed to become equivalent once we move to "homotopy categories".
For example, even for $2$-groupoids, you could ask to have a binary composition operation that composes two (composable) arrows and satisfies associativity up to isomorphism, plus the coherence condition between the associativity isomorphisms, or, follow the "unbiased" path and have for each $n$ a $n$-ary composition operation that compose string of (composable) $n$ arrows plus compatibility isomorphisms between these operations. The two approaches are not strictly equivalent, but will produce the same "homotopy category" (i.e. will be equivalent if one only considers groupoids up to categorical equivalence).
For example, taking "Kan complex" as a definition of $\infty$-groupoids can be considered as a reasonable choice and not as you said a "tautological solutions in which homotopy types are defined to be $\infty$-groupoids in the first place":
In a Kan complex, you do have a notion of $n$-morphisms and you can compose them and so on. It is a purely algebraic notion so to some extent I guess it could be considered an answer to the Whitehead program, depending on how you interpret the vague formulation given on the link you mention. Finally, the equivalence between the homotopy category of spaces and of Kan complexes is a rather non trivial result relying on an "algebraic approximation" result (the "simplicial approximation theorem").
(My understanding of history is that the realization that one can do homotopy theory purely algebraically using simplicial sets follows from Kan's work in the 50's, so a few years after Whitehead ICM talk, but I don't know much about it, so maybe someone would clarify this ? )
In Pursuing Stacks, Grothendieck did gave a different definition of $\infty$-groupoid, which follow a "globular" combinatorics, i.e. where instead of simplex as in Kan complexes, one has just have a notion of $n$-arrows between each pair or parallel $n-1$-arrows and operations on those. By the "homotopy hypothesis" one often refer to the statement that the homotopy category of Grothendieck $\infty$-groupoids is equivalent to the homotopy category of spaces. (see G.Maltsiniotis paper on this )
This version of the homotopy hypothesis is still widely open.
On the other hand, a proof of this version of the homotopy hypothesis does not seem that it would provide a better answer to the Whitehead program than a Kan complex: it is basically not easier to compute homotopy classes of maps with globular $\infty$-groupoids that it is with Kan complexes. The only difference between the two is the type of combinatorics that you have to describe your $n$-arrows and the relations between them. A bit in the same vein as the example I gave in the beginning with $2$-groupoids.
Finally, if I'm allowed to quote my own work (which I think bring some light on the question) in a recent paper I gave a different definition of $\infty$-groupoid, which is still globular (i.e. where you just have a collection of $n$-arrows between each pair of parallel $n-1$-arrows and some operation one those) but for which one can prove the homotopy hypothesis. These groupoids can be defined informally as globular sets equipped with all the operations than you can construct on a type in a weak version of intentional type theory.
I also proved in the same paper that Grothendieck formulation of the homotopy hypothesis is implied by some technical conjecture on the behavior of homotopy group of finitely generated Grothendieck $\infty$-groupoids, which can be dually understood as the fact that certain operation that you should be able to perform on arrows in a $\infty$-groupoid can indeed be defined from the operations Grothendieck puts on his $\infty$-groupoids (because map between finitely generated object, are the same as operations...).
I believe that my results show that our inability to prove Grothendieck's formulation of the homotopy hypothesis has nothing to do with an inability to express homotopy type as $\infty$-groupoids, but rather with some technical combinatorial difficulties inherent to Grothendieck's definition (basically, that it is not totally clear yet if Grothendieck's definition of $\infty$-groupoid is 'correct' and well behaved).