“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 Lea”
- #social
- #mastodon
- #self-published