Comment Comment by tsterin Opus 4.6 finds proofs of false in Rocq and Lean kernels. parent tsterin 8 months ago