Post #544665

2026-03-02 11:55 UTC

The time has come: Claude is able to poke holes in the dark corners of Rocq&#39;s kernel and come up with proofs of False! The days of &quot;our reasonable users use the unreasonable features only in reasonable ways so it&#39;s ok to have them&quot; really are over. Can&#39;t wait until someone vibe codes a complicated proof without looking too closely at it (since it&#39;s been checked by the kernel, it must be fine!) only to later realise it was actually bogus and such a bug without the agent saying so...

Replies (5)

@jesper@agda.club 2026-03-02 13:16

@mevenlennonbertrand well at least with Agda you probably don't need to burn as many GPU cycles to find a proof of false, so you could consider it to be more ecological alternative.

Open ##1101303
@jeanas@mathstodon.xyz 2026-03-02 12:58

@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

Open ##2780910
@cosmo@mathstodon.xyz 2026-03-03 09:27

@mevenlennonbertrand@lipn.info here is a full account of what was found (collaboration between Opus 4.6 and rocq experts): - 3 proofs of false from bugs in the guard checker - 2 proofs of false from bugs in the module system (the second one uses Girard's paradox) - 1 proof of false from a bug in `conversion.ml` - 1 proof of false from a bug in `discharge.ml` (using Hurkens' paradox) - 1 anomaly from a bug in `conversion.ml` - 2 bugs in `cClosure.ml` - 1 bug in `mod_declarations.ml`

Open ##2780916
@MartinEscardo@mathstodon.xyz 2026-03-04 22:09

@mevenlennonbertrand@lipn.info Just waiting to see what will happen when somebody prompts Claude about Agda. I am not going to do it myself.

Open ##2780917
@cosmo@mathstodon.xyz 2026-03-05 16:44

@mevenlennonbertrand@lipn.info I wrote a short summary about the proofs of false found in Rocq and Lean: https://tristan.st/blog/in_search_of_falsehood

Open ##2780918