2026-09-26 19:02 UTC
@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.
Replies (1)
-
@glyph@mastodon.social 2026-09-26 19:03
@eevee@slime.global @zzzeek@fosstodon.org @hynek@mastodon.social so now, every result that it produced is suspect. even if 99% of the results are actually correct, a human has to re-do all the proofs, and the human has to re-do the proofs *independently, without a machine verifier* because the verifier is not actually built to verify this kind of proof, and the steps in the proof are both very complex and also surrounded by valid work and are *much harder* than human work to check