Post #4208534

@0xabad1dea@infosec.exchange many many years ago, i filed quite a few issues against coqchk, Rocq's proof checker. it had a lot of unsafe code. (I wanted to put theorems on the Ethereum blockchain so that they self-reward the people who find them.) anyway, although my issues were eventually resolved and coqchk is better as a result (I filed some of the fix PRs!), i was eventually pointed to a previous experiment, which basically concluded with humans proving False quite a few times