What was already known
Laderman supplied an upper bound of 23. Wang and subsequent work obtained lower bounds of 20 and 21 over F₂; Rudich and Rousseau raised the relevant lower bound to 22. Exact rank 23 is a stronger field-specific statement than Ivanov’s lower bound of 21 over every field.
What changed and why it matters
The result would close a longstanding fixed-format operation-count problem over F₂ and integer coefficients. Its exhaustive certificate computation is a different contribution from an all-field lower bound or an asymptotic exponent improvement.
The AI contribution
The paper’s Use of AI tools section says generative AI helped find and prove the results, write the programs and Lean formalization, and draft the text. Tomar remains the human author; the source does not document enough detail to infer autonomous discovery or assign a specific model.
Limitations
The result does not determine the exact rank over Q, C or F₃, and does not determine border rank over F₂. The largest certificate checks use native_decide and depend on the Lean compiler and runtime in addition to the kernel. Reported sample interpreter checks do not remove that dependency for every batch. AIProofWatch has not regenerated the multi-million-batch search, rebuilt Lean or audited the certificate coverage. Preprint; no independent human peer review claimed.
Verification evidence
Evidence labels show what supports the claim. Importance rates its impact if correct.
Author claim
The version-1 paper states exact rank, preceding bounds and the compiled-checking qualification.
Accessible artifact / proof
Pinned programs, certificate recipes, Lean code and trust assumptions are available.
Formal checking
Author-reported Lean proof with large native_decide certificate checks; not reproduced by AIProofWatch.
Checker: Tejasvi Singh Tomar project: Lean plus compiled certificate evaluation (reported)
Scope: R22B.rank_ge_23 and R22B.rank_eq_23 over F₂, depending on native evaluation for the largest checks and the prior rank-22 development.
Basis: Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Correction and publication history
Daily primary-source follow-up on the new all-field rank lead found this distinct exact F₂ result. No equivalent contribution in complete local/live records; preserve its stronger compiled-code trust assumptions.
Read this published revision