Fake foreign words can sometimes take a life of their own, see e.g. https://en.wikipedia.org/wiki/List_of_pseudo-French_words_in... https://en.wikipedia.org/wiki/List_of_pseudo-German_words_in...

My favorite coffee name so far is definitely Urino Decaffeinato

The first link is terrible. “Voir dire” is not pseudo-French, it’s an archaic expression from old Norman French (a lot of such phrases ended up in English legal language). Also, “nom de plume” is used commonly in French.

>Urino Decaffeinato

I think I was drinking that this morning.

that doesn't sound very tasty, but to each their own I guess.

Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as large trees, a tiny subset of which needs to be made explicit to convey the confidence the rest could be written out (if ever needed).

Does that presuppose that it's computationally expensive to verify proofs? If so, isn't that kind of unrealistic?

Verifying fully formalized proofs is cheap. What is expensive is to produce such formalized proofs. More precisely, to formalize a proof written in a typical math paper is extremely time-consuming and not so informative (that's why it's almost never done in practice).

Ah, cheers. :)

But doesn't that bring us full-circle to Buzzard's point? Isn't that why he's saying, "Hey gang, let's do math with machines." in the first place?