Claims

../

1949_01_01_erdos: Erdős's 1949 Theorem 1: for some c > 0 and infinitely many d, more than c phi(d) reduced classes mod d have least prime above (1 + c) phi(d) log d; refereed.

2026_07_25_han: KyungMin Han's candidate proof, with GPT 5.6 Pro, that for all large q a positive proportion of reduced classes have least prime above (1 + c) phi(q) log q, by second and third moments of primes in classes; not reviewed.

2026_09_28_li: Shisheng Li's Lean 4 development of September 2026, found with GPT-6 and formalized with Claude, proves the formal-conjectures statement of Problem 971 by a moment route; announced in the site's thread; unreviewed.

---