Post #2780910
2026-03-02 12:58 UTC
@mevenlennonbertrand@lipn.info My god…
Here's the thread for the record: https://rocq-prover.zulipchat.com/#narrow/channel/237977-Rocq-users/topic/Proof.20of.20false.20found.20by.20Opus.204.2E6.20and.20mxdys.20.28bbchallenge.29/with/576655078
Replies (1)
-
@mevenlennonbertrand@lipn.info 2026-03-02 13:16
@jeanas@mathstodon.xyz I mean, it's not *very* surprising: here Claude is basically used as a very powerful fuzzer to put huge stress on a part of the code that experts were already very suspicious about. It's quite impressive it managed to actually find something, and even more that part of its explanation were reasonable. But I think we were kind of expecting this was going to happen at some point? At least I've been mentioning this possibility in MetaRocq-adjacent propaganda for a while.