ChatGPT Gaslighted Me: a Poem
Bob Rubbens


One morning the ChatGPT
Decided to go gaslight me

I had wrote ... (c (ChurchNat × ChurchNat) succ_hist (c, c)) ...
And got stuck, passing c cyclicly.

I directed myself at ChatGPT
And asked, “In the context of church encoding, is the predecessor
function typable in dependent type theory?”

“Short answer: it depends on impredicativity.”
It lectured me studiously

“Define ∀A:Type. (A → A) → A → A as C”
“Then pred : C → C does not type predicatively”

“Assuming impredicavitity”
“The classic term λn f x.  n  (λr i.  i (r f))  (λf. x)  (λu. u) is
typable, most possibly

“But mind you, evaluating it is costly
”Resolve this with additional machinery”

Distraught, I knew, woe is me
This is too much complexity

To the Lean prover zulip I flee’d
And asked for a little mercy

“Oh please, community, give me”
“The insight to this problem that is key”

Then, a wise mathematician decreed,
“Maybe you meant to write
c (ChurchNat × ChurchNat) succ_hist (zero, zero)?”