fix: aggregate proved/disproved/solved README counts are not exact-status links

README.md

@@ -25,11 +25,11 @@ Several of the problems have received assistance from various AI tools.  A list
 <!-- TABLE:START -->
 There are 1217 problems in total, of which
 - [106](https://teorth.github.io/erdosproblems/?prize=yes) are attached to a monetary prize.
-- [330](https://teorth.github.io/erdosproblems/?status=proved) have been proved.
+- 330 have been proved.
   - [120](https://teorth.github.io/erdosproblems/?status=proved+%28Lean%29) of these proofs have been formalized in [Lean](https://lean-lang.org/).
-- [132](https://teorth.github.io/erdosproblems/?status=disproved) have been disproved.
+- 132 have been disproved.
   - [62](https://teorth.github.io/erdosproblems/?status=disproved+%28Lean%29) of these disproofs have been formalized in [Lean](https://lean-lang.org/).
-- [93](https://teorth.github.io/erdosproblems/?status=solved) have been otherwise solved.
+- 93 have been otherwise solved.
   - [23](https://teorth.github.io/erdosproblems/?status=solved+%28Lean%29) of these solutions have been formalized in [Lean](https://lean-lang.org/).
 - [3](https://teorth.github.io/erdosproblems/?status=not+provable) appear to be open, but cannot be proven from the axioms of ZFC. (not provable)
 - 4 appear to be open, but cannot be disproven from the axioms of ZFC. (not disprovable)

scripts/generate_readme.py

@@ -295,11 +295,14 @@ def build_table(rows):
     lines = []
     lines.append(f"There are {len(rows)} problems in total, of which")
     lines.append(f"- {filter_link(count_prize(rows), 'prize', 'yes')} are attached to a monetary prize.")
-    lines.append(f"- {filter_link(count_proved(rows)+count_proved_lean(rows), 'status', 'proved')} have been proved.")
+    # Aggregate proved/disproved/solved counts mix ordinary + Lean statuses; the
+    # site filter is exact-match only, so linking to ?status=proved would omit
+    # "proved (Lean)" rows. Keep aggregates as plain text; link the Lean subcounts.
+    lines.append(f"- {count_proved(rows)+count_proved_lean(rows)} have been proved.")
     lines.append(f"  - {filter_link(count_proved_lean(rows), 'status', 'proved (Lean)')} of these proofs have been formalized in [Lean](https://lean-lang.org/).")
-    lines.append(f"- {filter_link(count_disproved(rows)+count_disproved_lean(rows), 'status', 'disproved')} have been disproved.")
+    lines.append(f"- {count_disproved(rows)+count_disproved_lean(rows)} have been disproved.")
     lines.append(f"  - {filter_link(count_disproved_lean(rows), 'status', 'disproved (Lean)')} of these disproofs have been formalized in [Lean](https://lean-lang.org/).")
-    lines.append(f"- {filter_link(count_solved(rows)+count_solved_lean(rows), 'status', 'solved')} have been otherwise solved.")
+    lines.append(f"- {count_solved(rows)+count_solved_lean(rows)} have been otherwise solved.")
     lines.append(f"  - {filter_link(count_solved_lean(rows), 'status', 'solved (Lean)')} of these solutions have been formalized in [Lean](https://lean-lang.org/).")
     lines.append(f"- {filter_link(count_not_provable(rows), 'status', 'not provable')} appear to be open, but cannot be proven from the axioms of ZFC. (not provable)")
     lines.append(f"- {count_not_disprovable(rows)} appear to be open, but cannot be disproven from the axioms of ZFC. (not disprovable)")