Reading Ravenel's "green book", I wonder about his question on p.15 "that the spectrum MU may be constructed somehow using formal group law theory without using complex manifolds or vector bundles. Perhaps the corresponding infinite loop space is the classifying space for some category defined in terms of formal group laws. Infinite loop space theorists, where are you?". What is the state of things on that now?

As far as I know, there is still no such interpretation. The closest I've heard is some rumored (but unpublished) work in derived algebraic geometry interpreting MU as some kind of representing object. Such a construction of MU in terms of formal group data be very welcome (probably even more now than when Ravenel wrote the green book). EDIT: Some elaboration. We do know a lot about MU. We know that it has an orientation (Chern classes for vector bundles), and in it's universal for this property. It's not then extremely suprising that we get a formal group law from the tensor product for line bundles, but the fact that MU carries a universal formal group law, and that MU ^ MU carries a universal pair of isomorphic formal group laws, is surprising. At this point it's something we observe algebraically. Even Lurie's definition of derived formal group laws, assuming I understand correctly, is geared to construct formal group laws objects in derived algebraic geometry carrying a connection to the formal group law data that we already know is there on the spectrum level, and hence ties it to the story we already knew for MU implicitly. Some reasons these days we might want to know how to construct MU from formal group law data:



To elaborate on Tyler's comment (and please correct my inaccuracies), the idea is that the moduli space of DERIVED onedimensional formal group laws (defined appropriately  roughly formal group laws in which rings are replaced with Eoo ring spectra) is an affine derived scheme, which is the spectrum (in sense of AG) of the spectrum (in the sense of AT) MU. This is a derived version of Quillen's theorem that the formal group law of MU is the universal formal group law. If I remember correctly Jacob Lurie said this is fairly obvious. It's the natural analog of the (much harder) theorem of Lurie's that the moduli stack of derived elliptic curves (roughly, versions of elliptic curves with structure sheaves given by Eoo ring spectra) is representable by a derived enhancement of the moduli of ordinary elliptic curves (the coordinate ring given by the canonical line bundle is then TMF). Another example of the philosophy is Tyler's work with Mark Behrens. But this one is supposed to be easier and less useful (more formal). If you take the moduli STACK of derived formal groups, then the global sections of the structure sheaf are just the sphere I think  this is a version of the AdamsNovikov spectral sequence. Anyway the idea is to reinterpret the QuillenMoravaRavenelDevinatzHopkinsSmith.. picture for the stable category via formal group laws as describing the algebraic geometry of the derived moduli stack of formal groups. 


There is a very easy theorem along much weaker but related lines in Adams's "Stable Homotopy and Generalized Homology." I refer to Lemma 4.6 of section II. It isn't written quite like this, but essentially it says that if E is a complex orientable spectrum together with a complex orientation $x \in E^{2}(\mathbf{C}P^{\infty})$ then there is a unique (up to homotopy) map of ring spectra $MU \rightarrow E$ taking the fixed (better fix one) complex orientation of $MU$ to the given complex orientation of $E$. This doesn't build $MU$ out of formal group laws of course, but it shows $MU$ has this universal property for complex oriented cohomology theories, and this book was around of course when Ravenel wrote the green book. It does seem like with the modern point of view these ideas should yield a construction out of complex oriented theories if not quite out of formal group laws. 

