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.