5 ms·
> 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 l
by interiorchurch 2y ago
> 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 2y agoThis is not true. If the right abstractions are used, proofs in Lean for example can be quite readable and concise.