The comments have already given the answers, but let me assemble them here with my account of the story.

When Scholze first posted the Liquid Tensor Experiment, it was quickly identified (by both Peter and Reid, somewhat independently I think) that Breen–Deligne resolutions would be the largest input
in terms of prerequisites that needed to be formalised. Back then, I had no idea what these resolutions were, or how to prove that they existed. But they were needed for the statement of Theorem 9.4, which seemed to be a very natural first milestone to aim for.

So I set out to formalise the statement of the existence of Breen–Deligne resolutions, with the expectation that we would never prove the result in Lean, but just assume it as a black box. Let me recalll the statement:

**Theorem (Breen–Deligne).** For an abelian group $A$, there exists a resolution of the form
$$ \dots → \bigoplus_{j = 0}^{n_i} ℤ[A^{r_{i,j}}] → \dots → ℤ[A^2] → ℤ[A] → A → 0 $$
that is functorial in $A$.

*On the proof.* See appendix to Section IV of Condensed.pdf. As Reid remarked in the comments, the proof relies on the fact that stable homotopy groups of spheres are finitely generated. ∎

(Aside: for the proof of Theorem 9.4, we really need a version that applies to *condensed* abelian groups $A$, so in practice we want to abstract to abelian sheaves.)

In the rest of the Lecture notes, Scholze often uses a somewhat different form of the above resolution, by assuming $n_i = 1$ and effectively dropping all the $\bigoplus$'s. I think this was done mostly for presentational reasons.

I did the same thing when I axiomatized Breen–Deligne resolutions in Lean. So really, they weren't axiomatized at all. I don't know of any reason to expect that there exists a *resolution* with the property that $n_i = 1$ for all $i$, but I also don't see any reason why there shouldn't. Anyway, I needed a name for the axioms that I did put into Lean, and I chose *Breen–Deligne package* for that.

So what is that exactly? Well, a functorial map $ℤ[A^m] → ℤ[A^n]$ is just a formal sum of matrices with coefficients in $ℤ$. So as a first approximation, we record

- the natural numbers $r_j = r_{1,j}$ (since $n_i = 1$);
- for every $j$, a formal sum of $(r_{j+1}, r_j)$-matrices with coefficients in $ℤ$.

But we need one more property of Breen–Deligne resolutions: if $C(A)$ denotes the complex, then there are two maps induced by addition. There is the map $σ \colon C(A^2) → C(A)$ that comes from the functoriality of $C$ applied to the addition map $A^2 → A$. But there is also the map $π \colon C(A^2) → C(A)$ that comes from addition in the objects of the complex. (All objects are of the form $ℤ[A^k]$ and we can simply add elements of these free abelian groups.) The final axiom of a Breen–Deligne package is

- there is a functorial homotopy between $σ$ and $π$.

While playing around with the axioms, I noticed that I could write down inductively a somewhat non-trivial example of such a package. When I discussed this example with Peter, he suggested that it might in fact be suitable as a replacement for Breen–Deligne resolutions in all applications in his lecture notes so far. Several months later we found out that I had rediscovered MacLane's $Q'$-construction. So, let's denote by $Q'$ the complex corresponding to the example package. The following result is, as far as I know, original:

**Lemma.** Let $A$ and $B$ be (condensed) abelian groups. If $\text{Ext}^i(Q'(A),B) = 0$ for all $i ≥ 0$, then $\text{Ext}^i(A,B) = 0$ for all $i ≥ 0$.

*Proof.* I've written up a proof sketch on Zulip (public archive of that thread). ∎

We are in the process of formalizing the necessary homological algebra to verify the proof in Lean. It's the last major milestone left to complete the challenge in Peter's original blogpost. After that, we mostly need some glue. See this blogpost for an update on the formalisation effort. (Edit: see also https://math.commelin.net/files/LTE.pdf for a more precise roadmap of what remains to be done to complete the challange.) Once everything is done, it should all be written up in some paper.

So now, let me turn to the question

is it sufficient to consider this default example, or is there a real need to consider all possible examples?

It is indeed sufficient to consider this default example. The reasons for working with the abstract concept of Breen–Deligne packages are

- historical: I had formalised the statement of Theorem 9.4 and some other material in terms of BD packages before I realised that this default example was indeed sufficient for our purposes.
- practical: as Remy points out in the comments, it is (i) helpful to abstract away concrete details into a conceptual object, and (ii) there is a chance that there might be better examples leading to better constants.

What would be really interesting is an example of a BD package that gives *resolutions* instead of merely functorial complexes. It is known that the $Q'$ construction is not a resolution. Indeed, one can easily show inductively that $H_i(Q'(ℤ))$ contains a copy of $ℤ^{2^i}$. With more work (relying again on abstract homotopy theory), Peter gave a proof that $Q'(A) ≅ Q'(A)^{⊕2}[-1] ⊕ ℤ ⊗_{\mathbb S} A$ on Zulip (public archive).

whichresolution, making it hard to formalise. Moreover, Commelin e.a. in LTE realised you don't actually need a resolution, just something slightly weaker. The main advantage is that it is now much easier to construct a very hands on example (Def. 2.13), but ultimately the theory does not rely on which example you work with (exactly like how a choice of projective resolution does not matter in the end). $\endgroup$7more comments