Auslander's formula shows that any abelian category \mathsf C is equivalent to the category of coherent functors on \mathsf C modulo the Serre subcategory of all effaceable functors. We establish a derived version of this equivalence. This amounts to showing that the homotopy category of injective objects of some appropriate Grothendieck abelian category (the category of ind-objects of \mathsf C ) is compactly generated and that the full subcategory of compact objects is equivalent to the bounded derived category of \mathsf C . The same approach shows for an arbitrary Grothendieck abelian category that its derived category and the homotopy category of injective objects are well-generated triangulated categories. For sufficiently large cardinals \alpha we identify their \alpha -compact objects and compare them.