@Pashhur The blueprint does contain a lot of material (such as classical Calderon-Zygmund theory) that is quite standard in this area, and Thiele is one of the leading world experts in the subject and has not to my knowledge published anything with major errors in it. Furthermore, the blueprint is already rather more detailed than a traditional math paper, even if it has not yet been properly formalized. So I think there is a reasonable a priori probability to expect that the arguments are largely correct. That said, the formalization effort, despite being only a day or two old, has already uncovered some minor issues in the blueprint (a (k) should have been a (k+1) in one of the lemmas, for instance): https://leanprover.zulipchat.com/#narrow/stream/442935-Carleson/topic/Outstanding.20Tasks.2C.20V1