I ask Bing Chat to write Lean 4 ZFC (Part 1 of ?)
https://www.asme.org/topics-resources/content/the-humanlike-ipal-robot

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

No alt text provided for this image

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:

No alt text provided for this image

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:

No alt text provided for this image

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

No alt text provided for this image

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

No alt text provided for this image

Still no joy.

No alt text provided for this image

What to do?

No alt text provided for this image

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

No alt text provided for this image

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.

No alt text provided for this image
https://i0.kym-cdn.com/photos/images/facebook/000/017/668/Mao_RTFM_vectorize_by_cmenghi.png

要查看或添加评论,请登录

Lars Warren Ericson的更多文章

社区洞察

其他会员也浏览了