What are good examples of April fools jokes in the proving assistant community?

Every community can have inside jokes among it, and April Fool’s jokes are a common variety, but proof assistants are particularly susceptible to April Fool’s jokes. They have strong guarantees of correctness so one could claim both that these claims are wrong or that one found irrefutable proof of something crazy. More so, they are very labor-intensive, making one possibly overly excited for claimed magical tools which speed up the field.

What are some good April Fool’s day jokes about proof assistants?

For those whose might vote to close this, let me at least say there is precedence for this question. Also this question is not itself a April Fool’s joke. :)

One answer per joke please. Keep it to the subject of this website. Provide a link if possible. I assume this will be made community wiki.

To derive avril1, we have used an interdisciplinary approach that combines concepts that are ordinarily considered to be unrelated. We have also used various definitions outside of their normal domains. This is called "thinking outside of the box." For example, the imaginary constant $$i$$ is certainly not a function. But the definition of a function value, df-fv, allows us to substitute any legal class expression for its class variable $$F$$, and $$i$$ is a legal class expression. Therefore $$( i  1 )$$ is also a legal class expression, and in fact it can be shown to be equal the empty set, which is the value of "meaningless" instances of df-fv, as shown for example by theorem ndmfv`.