7
$\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.

Improve this question
$\endgroup$

3 Answers 3

Reset to default
13
$\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.

Improve this answer
$\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$
    – Luiz Martins
    Commented Apr 1, 2022 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

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ the mixed use of "prim" and "prime" gives it away :) $\endgroup$
    – Hagen von Eitzen
    Commented Apr 1, 2022 at 20:51
9
$\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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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