Re: undefined #2 Post by tsterin » Thu, Mar 05, 2026, 4:40 PM UTC Opus 4.6 finds proofs of false in Rocq and Lean kernels.