2026-07-28 13:58 UTC
RE: https://lipn.info/@mevenlennonbertrand/116997917683191056
Scary. Also makes a case for funding fundamental type theory research in the age of AI
Replies (1)
-
@mevenlennonbertrand@lipn.info 2026-07-28 14:07
@TaliaRinger@mathstodon.xyz I think type theorists would consider this as rather applied type theory :p But fully agreed! On the positive side (and to toot my own horn a bit) we have not been idle: https://metarocq.github.io/ is the most mature project in the area, but https://github.com/digama0/lean4lean and https://github.com/jespercockx/agda-core/ are also busy, and there's a lot of more fundamental research happening as well to prepare for these project's next steps. The age of verified kernels is coming!