[jmpetroske]

The reason Hilbert failed is because it’s mathematically impossible (Gödels incompleteness theorem).

[ur-whale]

> because it’s mathematically impossible

I guess the Lean devs can all pack and go home then. Also: how could they possibly miss Gödel's theorem, how careless of them.

[jmpetroske]

Look, you’re taking my response out of context. I’m just stating that the reason Hilbert failed is not that he didn’t have a computer. Lean devs aren’t trying to do what Hilbert was.