@mevenlennonbertrand@lipn.info
Post #4231616
2026-07-28 13:53 UTC
Lean. One kernel bug. In the darkest type theory. All external checkers affected. Learn why this matters in the AI age.
Replies (2)
-
@mevenlennonbertrand@lipn.info 2026-07-28 13:55
I'm not very good at this, am I?
-
@mio@shrimp.mio19.uk 2026-07-30 12:49
@mevenlennonbertrand@lipn.info I am thinking about proving the properties of a proof assistant in a proof assistant