Post #4119488

The Erdos problems repository at https://github.com/teorth/erdosproblems initially tracked such data as whether a given Erdos problem was considered "open" or "solved" (with some other technical variants such as "decidable" or "falsifiable" which I will ignore here). Later on, we also added additional subcategories such as "solved (Lean)" which indicated their formalization status. In response to the recent (and likely enduring) phenomenon of AI-generated proofs that have been formalized in Lean, but not digested enough to be accepted by a human expert, we have now decoupled the formal status and informal status of the problems. We now have an inaugural example #1112 of a problem with the counterintuitive status of "open (Lean)"; there is a verifiable formal solution to the problem, but no human digestion of the solution has yet occurred, so the problem remains open in the informal sense. This problem will likely soon be joined by many others as the site continues to update.