That seems to have been more of a sensationalized joke. Even your link has a disclaimer in it now. Read this chat from the researcher who did this:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
It's not at all a joke ... that's a severe misunderstanding of the context.
It's not at all a joke ... that's a severe misunderstanding of the context.