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

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

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.