diff --git a/AGENTS.md b/AGENTS.md
index 7a4eaf60..db7dcf64 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -119,7 +119,7 @@ Target: `formal/SilverSight/HachimojiN8.lean` — provable by `native_decide` on
 | Bind.lean | Complete | 0 |
 | PIST/Spectral.lean | Complete | 0 |
 | PIST/FisherRigidity.lean | Complete | 0 |
-| CoreFormalism/ChentsovFinite.lean | In Progress | 8 |
+| CoreFormalism/ChentsovFinite.lean | In Progress | 5 |
 
 ## FisherRigidity — Parabola Focal-Chord to Fisher-Rao Bridge