Current status of Grothendieck's homotopy hypothesis and Whitehead's algebraic homotopy programme (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?

 A: 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).
A: I think this question is an interesting one, and the two approaches should be compared. I have more knowledge of Whitehead's programme, and have been involved with others in the development of aspects of that programme. A report on the background of part that work is in the paper Modelling and Computing Homotopy Types: I, to appear in 2017 in a special issue of Indagationes Mathematicae in honor of L.E.J. Brouwer. A notable feature of this work is that it deals not with "bare" spaces but with "Topological Data", and this somewhat reflects Grothendieck's view expressed in "Esquisse d'un Programme" Section 5. Also among the aims of Whitehead's work was to introduce invariants  which allowed specific calculation and even if possible enumeration. 
I should explain that having from 1965 to 1974 tried to define for a space $X$  a strict homotopy double groupoid which could satisfy a van Kampen type Theorem, and so enable specific calculations,  it was a considerable relief to find with Philip Higgins that this could be done  in a natural and intuitive way  for a pair $(X,A,c)$ of pointed spaces by mapping the square $I^2$ into $X$ so that the edges of $I^2$ mapped to $A$ and the vertices mapped to $c$. This gave a vast generalisation of a tricky theorem on free crossed modules, proved in Section 16 of the 1949 paper "Combinatorial Homotopy II" (CHII). 
Further this definition of homotopy double groupoid generalised, with considerable more work, to all dimensions using filtered spaces, so  continuing Whitehead's programme in CHII.  
The algebraic data used here of strict cubical $\omega$-groupoids, and the equivalent crossed complexes, do not model all homotopy types, and indeed contain in essence only "linear" information, i.e. no Whitehead products, for example. However these models do contain more information than chain complexes with a group of operators, conforming with an observation of Whitehead in CHII.  
However a meeting with J.-L. Loday in 1981 in Strasbourg started our link with his work on what he called $n$-cat-groups, and we later  agreed to call cat$^n$-groups, and which are $n$-fold groupoids in which one direction is a group.  Loday had proved in 1982 modelled pointed homotopy $(n+1)$-types. We conjectured then and eventually proved a van Kampen type theorem in the  context of $n$-cubes of spaces; this work was eventually accepted for the journal Topology, and a companion paper was accepted for Proc. London Math Soc, both appearing in 1987.  The latter paper proved an $n$-adic Hurewicz Theorem, the triadic version of which was a conjecture of Loday in 1981. 
Actually Grothendieck objected to the pointed condition, and did not recognise what had been achieved - he always wanted the most general conditions! However one aspect of the work with Loday, a nonabelian tensor product of groups which act on each other, has been well taken up by group theorists, and  a current bibliography has 158 items dating from 1952. 
H.-J. Baues in several books has continued aspects of Whitehead's programme, but he does not apply the Brown-Loday work, and his models do not satisfy the Criteria set out in Section 1 of the cited paper  "Modelling and Computing Homotopy Types:I". However paper II of that has been delayed for various health  reasons. 
This paper, in a volume in memory of J.F.Adams,  refers to work of G.J.Ellis and R. Steiner which applies the Brown-Loday work to solve an old problem in homotopy theory, on which Whitehead had written, to determine the value of the critical (i.e. first non vanishing) group of an $(n+1)$-ad. 
Looking again at Esquisses d'un Progamme, it seems that programme has currently little relation to Whitehead's; but a 1983 letter from Grothendieck to the writer,  reprinted as Problem 16.1.29 of Nonabelian Algebraic Topology, may suggest that despite his interest in the 2-d van Kampen theorem,  the lack of progress with the issues he there raises indicates a limitation of this writer.
Grothendieck was very interested at one point in the idea I once conveyed to him that  $n$-fold groupoids model homotopy $n$-types. But this is not true as stated even for $n=2$,  since $2$-fold groupoids can be much more complicated than crossed modules over groupoids, which are a good model of homotopy $2$-types, and are equivalent to a special kind of double groupoid. 
Added 18/04/2017: A final remark is that in my work with Higgins the cubical aspect is essential, and analogous results have not been obtained by simplicial methods.  However the work with Loday does use also advanced simplicial methods for the proof of the main result. In both cases, the cubical methods are used to express multiple compositions, which are tricky simplicially. 
