---
title: "ChatGPT Gaslighted Me: a Poem"
author: Bob Rubbens
publish_timestamp: 2025-10-09T09:23:03+02:00
state: published
template: post.mako
id: 5b39d2f0-a0cd-4db7-a375-e25c257cebdb
---

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."](./transcript)\
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)`?"](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Church.20numeral.20subtraction/near/543265722)