Elektrine lite

← Feed

@tao@mathstodon.xyz

2026-07-26 19:12 UTC

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.

Replies (3)

  • @O@mathstodon.xyz 2026-07-27 01:12

    @tao@mathstodon.xyz how would this differ from computationally fimding a counterexample and not truly understanding why it's truly happening? Or that it took us more to understand why the counterexample given by Fable 5 to the Jordanian conjecture is happening, similar to your last Blogpost? There's many problems that were proven without us truly understanding what actually happened, more often than not in counterexamples.

    Open ##4595752

  • @number_muncher@mathstodon.xyz 2026-07-27 01:52

    @tao@mathstodon.xyz It's fine if the informal status is "open" but if you just say "status", then it should definitely be "proved" instead of "open".

    Open ##4595753

  • @theking@mathstodon.xyz 2026-07-27 15:08

    @tao@mathstodon.xyz hmm I feel like "undigested" would be a better term. So like "proven (undigested)" or "disproven (undigested)". Also is there a search query to show such problems? It doesn't look like the search query let's you do Boolean operators.

    Open ##4595755