RE: https://mathstodon.xyz/@johncarlosbaez/115677835220476940 My post on Axiom Math had major errors, which I've tried to correct in the new version below. It was not Axiom Math but another company, Harmonic, that first used AI to solve some Erdős problems! Harmonic's program is called Aristotle. As of today Harmonic's news page claims: "And just recently, a beta version of Aristotle was used to solve and formally verify multiple open Erdos problems, which had been unsolved for decades." https://harmonic.fun/news Two are the problems discussed below. For the third, #480, Aristotle found a trivial proof by exploiting a formalization error. So, I now feel Business Insider was misleading when they wrote "Axiom, which recently said it solved two Erdős math problems that eluded mathematicians for decades, announced a $64 million seed round in September." even if perhaps Axiom has redone these proofs. But I certainly should have checked the reality more carefully before coming out with my article, especially given the rather dramatic conclusions I jumped to. I was quite confused. The head of Axiom Math clarified these issues here: https://mathstodon.xyz/@carina1248@mastodon.social/115679850066865211 I would not be surprised if I haven't completely gotten to the bottom of what's going on in this story, but this is my current understanding, and I apologize for getting some big things wrong before.