Comment by interiorchurch

> As a layman who's only familiar with Hilbert's work as it pertains to Godel and CS, I'm curious what makes expressing these proofs using some sort of formal logic so difficult.

For one thing, they'd be much longer, and likely not human-readable.