6
$\begingroup$

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.

$\endgroup$

3 Answers 3

12
$\begingroup$

I don't know if Falso itself was "released" on April 1st, but an implementation of it Isabelle/HOLF was. Of course, this is a very powerful proof assistant and it is a shame that an implementation of it was released on April 1st and thus not taken seriously by the PL community.

$\endgroup$
1
  • 4
    $\begingroup$ Dude, I was struggling a lot with a specific theorem. Tried reasoing about it in Falso, and solved it in a day! Thank you for the link! $\endgroup$ Apr 1 at 21:58
10
$\begingroup$

Brunhilde/Rhein 2015, as announced on the Isabelle mailing list was a fully working German translation of Isabelle/HOL, including keywords. It also came with a homepage, example documents and suggestive screenshots such as this one:

The square root of two in German

$\endgroup$
1
  • 4
    $\begingroup$ the mixed use of "prim" and "prime" gives it away :) $\endgroup$ Apr 1 at 20:51
8
$\begingroup$
  • Metamath has a list of April fool theorems.

An excerpt of the explanations:

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.