Posts tagged automated proofs
Why I don't trust Lean code from AI
Oct 10 2026, 00:41
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...Some thoughts about "automated theorem searching"
Jun 27 2016, 01:02
Let me begin by giving a spoiler warning. If you haven't watched "The Prisoner" you might be spoiled about one of the episodes. Not that matters, for a show from nearly 40 years ago, but you should definitely watch it. It is a wonderful show. And even if you haven't watched it, it's just one episode, not the whole show. So you can keep on reading.
So, I'm fashionably late to the party (with some good excuse, see my previous post), but after the recent 200 terabytes proof for the coloring of Pythagorean triples, the same old questions are raised about whether or not at some point computers will be better than us in finding new theorems, and proving them too.
Continue reading...