I ask Bing Chat to write Lean 4 ZFC (Part 1 of ?)

Bing Chat seems to know Lean 4, in particular build 4.0.0-nightly-2023-04-20. I ask it "Please write the ZF set axioms in Lean 4 including all necessary imports and declarations." It gives me back

There are a couple of problems with this: There is no set_theory package, and I'm asking it to define set theory from scratch, not import it. So, deleting the import and the name space, what do we get? Syntax problems right from the get-go:

So, before actually trying to learn Lean (which is very hard, actually) and Lean 4 (which is totally new), let's see if Bing Chat knows better:

This doesn't work either, so I ask a followup:

It doesn't tell me how to add a universe declaration, so...

Still no joy.

What to do?

Gosh. It turns out, I do have some other questions.

I'm tearing my hair out now. Let's call this Part 1. I will go RTFM and come back and see if I know enough Lean 4 after that to guide Lean 4 into giving me an answer that type checks, for one line, and then maybe even for the whole set of axioms a single correct answer.