Why I don't trust Lean code from AI

So, I wrote a post about why I am not nearly impressed with OpenAI's preprint regarding the Partition Principle. But that is not nearly the whole story. Let me tell you one more thing. I saw a few people who commented on my previous posts through various social posts and reposts. Many of them were understanding of the plight of mathematicians. Some were trying to make the following point: I claimed that I did not (nor I intend to) read the Lean proof generated by ChatGPT. Some people felt like this is a deal breaker, like this is a reason to disregard everything else I had to offer, because I will not accept this bit of code. Continue reading...