The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

Disclaimer: do not feed the troll.

On 26/10/2012 00:25, Jonas Oberhauser wrote:
> That friend didn't buy it, so I decided to formalize the proof that if
> unconditional love only starts after the other person somehow loves you,
> then either you love the other person unconditionally from the start
> (from the beginning of time, so to speak) or you never will.

Drugs are bad, mkay?

(More seriously, I would like to have any fallacious theorem like 
Gödel/Descartes ontological existence of God formalized in any 
trustworthy theorem prover to see which exact definition you need to 
prove such theorems. Anyway, as « all you need is love », that implies 
in particular:

Theorem : love -> False.

Thus, « Come back Grothendieck, they've become crazy! »)

Uninformatively yours,
PMP