Anatomical Review of Automated Mathematics: Verification, Understanding, and Proof Reuse. Distinguishing Formal Correctness from Conceptual Progress in AI-Driven Mathematical Research

Abstract

This paper presents a detailed anatomical review of Bloch and Noguer i Alonso's (2026) framework for automated mathematics, which seeks to separate formal correctness, faithful formalisation, and mathematical understanding. The original work responds to the September–October 2026 controversies surrounding large-scale AI-generated formal mathematics, notably OpenAI's Navier–Stokes announcement and subsequent manuscript releases. It proposes an auditable acceptance and alignment protocol, a conditional model of proof transmission via factorisation, an analysis of search on formal proof states with subgoal advantages, and a reproducible source-level protocol for measuring declaration-level reuse, executed as a pilot on the openai/math repository. The present review evaluates the technical precision and institutional sensitivity of these proposals, identifies strengths and limitations, situates the work among at least ten competing or complementary approaches in automated theorem proving and the philosophy of mathematical practice, and examines the ontological and epistemological verticals that structure its central themes. Possible extensions are outlined. The contribution is a critical synthesis that neither endorses formal verification as a complete account of mathematical progress nor dismisses the value of careful measurement and status separation.