I've heard Leslie Lamport put forth that estimate as well. It might even be right, but if his example of Kelley's oversight in proving the Cantor-Schroeder-Bernstein is at all representative, it's not necessarily cause for alarm.

I'm not a model theorist, but from the Zentralblatt review: "The author’s intended audience for this high level introduction to model theory is graduate students contemplating research in model theory, graduate students in logic, and mathematicians who are not logicians but who are in areas where model theory has interesting applications." The first edition is from 2002. You might just have a look. In general, you might get better response to your question if you say what books you've already looked at, what topics you studied, etc. Of course model theory is quite a big field...

$Tc \to c$ is necessarily an isomorphism, so $Tc \cong c$, or $c$ is a "fixed point" of the endofunctor $T$. For example, for the binary trees example, the structure map $Tc = 1 + c \times c \to c$ assigns to the element of $1$ the trivial tree without children, and to a pair of trees $(t, t')$ the tree whose root has left-child = root of $t$, and right-child = root of $t'$. (Notice that in this example, there is no monad structure at hand -- although I'd have to think to show that none exists.) The inverse $c \to Tc = 1 + c \times c$ takes a tree and deconstructs it into its left, right pair.

The notion of algebra of an endofunctor is very well-known in category theory, especially those aspects of category theory that touch on data types. Here a $T$-algebra for an endofunctor $T: C \to C$ is just an object $c$ of $C$ together with a map $Tc \to c$, with no other assumptions. Especially significant is whether initial $T$-algebras can be constructed, and many data types arise in just this way. For example, the initial algebra of the endofunctor defined by $T(c) = 1 + c \times c$ is the data type of binary trees. An old result of Lambek is: for $c$ initial, the structure map (cont.)

I don't see any mention of monad structure (and in any case I wouldn't know how that would go), but it is a polynomial endofunctor on groupoids. So maybe you want to know what is the category of algebras in the endofunctor sense?

Agreed; very good answer. I particularly agree that that's probably how most mistakes get caught: not by nose-to-the-grindstone checks of logical correctness, but by having sensitive mathematical noses that detect when something smells just a little bit fishy. Human intuition is so much faster than human logic. Moreover, you have to develop the inner quietude to listen to those whisperings (especially when it comes to catching your own mistakes!).

Rota is a great story-teller, but generally speaking people should fact-check him on his pronouncements.

This was in response to your second paragraph: "Also, I wish there is literature about the common proof techniques and tricks one uses in the current research" -- it seemed to me Marker's book fits that description.

The Calkin-Wilf representation gives an explicit bijection between positive rationals and the set $T$ of nodes in the infinite binary tree, but I'm not seeing a clean and natural bijection $T \cong T \times T$. There is of course a natural bijection $T \cong T^2 + 1$, and Andreas Blass (in his Seven Trees in One article) observed that this could be exploited to yield a natural bijection $T \cong T^7$. So if you had asked for a natural bijection $\mathbb{Q}_+ \cong \mathbb{Q}_+^7$, then this might just work. :-D

Have you looked at David Marker's book?

This looks very much like existence of a nonprincipal ultrafilter on $\mathbb{N}$, which cannot be proven in ZF. (But is far weaker than AC of course.)

When I clicked on the link, the answer I saw had nothing to do with tetrahedra, but with the prime number theorem. Not sure what is going on.

@FrancoisZiegler My command of French is not sufficient to read the text without some assistance, but it is very interesting and it does seem consonant with what I thought I understood from reading the essays by McLarty and Corry. And so I think I will make an edit to my answer, acknowledging your references. Just one note with regard to the commentary below my answer: it is noted that Weil was present at the 43rd meeting in 1957 (after he announced his retirement in 1956) in which they are discussing a possible Theory of Categories (for Bourbaki) -- see page 26 of 44 of the pdf.

@FrancoisZiegler Thanks. I haven't looked into this reference, and thus I don't know whether it is consonant or not with the conclusions drawn by McLarty and Corry. If it is not, then I don't see how I would smoothly integrate it into my answer -- but I am happy meanwhile to upvote your comment for visibility's sake.

@ZachTeitler There is one issue that remains to be clarified: whether the modulus function is regarded as a function mapping to $\mathbb{C}$ or to $\mathbb{R}$. This is not a pedantic distinction because it's not clear that OP wants to include the standard inclusion $\mathbb{R} \hookrightarrow \mathbb{C}$ as part of the underlying signature of the theory. I think my main question is whether, in the absence of allowing direct images, composition of definable functions would be admitted as definable. (Allowing only Boolean combinations of definable sets is pretty weak and constraining.)