Solution (in retrospect this should’ve been posted a few years earlier):

let

’Na’ = box N contains angry frog

’Ng’ = N gold

’Nf’ = N’s inscription false

’Nt’ = N’s inscription true

consistent states must have 1f 2t or 1t 2f, and 1a 2g or 1g 2a

then:

1a 1t, 2g 2f ⇒ 1t, 2f

1a 1f, 2g 2t ⇒ 1f, 2t

1g 1t, 2a 2f ⇒ 1t, 2t

1g 1f, 2a 2t ⇒ 1f, 2f

Depends on how much of a superintelligence, how implemented. I wouldn’t be surprised if somebody got far superhuman theorem-proving from a mind that didn’t generalize beyond theorems. Presuming you were asking it to prove old-school fancy-math theorems, and not to, eg, arbitrarily speed up a bunch of real-world computations like asking it what GPT-4 would say about things, etc.