logoalt Hacker News

traestoday at 8:32 AM1 replyview on HN

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


Replies

jibaltoday at 9:36 AM

It's not at all a joke ... that's a severe misunderstanding of the context.

show 1 reply