2026-09-26 19:01 UTC
@eevee@slime.global @zzzeek@fosstodon.org @hynek@mastodon.social if I could put a finer point on this, that's not exactly what I'm saying, although the functional output of what I'm saying is the same. Specifically, verification can be cheaper than performing the task sometimes, but the aggregate of A) doing the verification *every* time (you can't skip any instances!) and B) _investigating failed verifications_, re-doing the work in those cases, and C) maintenance of the verification loop itself
is indeed *more* work than the work.
Replies (1)
-
@glyph@mastodon.social 2026-09-26 19:02
@eevee@slime.global @zzzeek@fosstodon.org @hynek@mastodon.social You can see how this played out in the recent Lean scandal. Lots of promising math research results. Crazy breakthroughs, proofs beyond human comprehension. Except, oops, we know that in at least one instance, what it actually discovered as *a bug in the verifier* because it was throwing inputs at the verifier that humans would never attempt because they were nonsensical confabulations. Lean was not built to check arbitrary untrusted random nonsense.