Rendered at 15:48:37 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
Mithriil 12 minutes ago [-]
Very interesting. I think it needs to be clear that the fundamental theories (dependent type theory) is very much grounded. It's at the practical implementation of Lean4 that the critic aims at.