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

[golol]

This is not true. If the right abstractions are used, proofs in Lean for example can be quite readable and concise.