If you want to drive crazy a SOTA AI then you ask it about existing Lean proofs of the undecidability of beta equivalence in untyped lambda beta calculus with no eta.

They'll try to evade from the constraints of the question but you can politely and to the point nudge them back to the original question.

Many things to learn from that, even about human proofs. For example that the BLC proof of Scott theorem establishes the undecidability of beta equivalence under normal order reduction. This is perfectly OK for equivalence of closed terms which have a normal form, but it is not the original question.

You can sooth them by explaining that in the pair (LLM, Lean) the weak link is Lean, not them.