REVIEW 4 major objections 4 minor 13 references
In between myth and reality: AI for math -- a case study in category theory
T0 review · 4 major / 4 minor · reviewed 2026-08-16 · deepseek-v4-flash
Pith's one-line read This paper argues that two leading AI systems can handle only the existence half of a category-theory proof, failing at uniqueness and at retrieving the definition.
desk verdict The paper's central claim that o3-mini produced a valid partial proof does not survive a close reading of its own appendix; the Grok analysis is solid, but the main conclusion is unsupported. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the inclusion system: a pair of broad subcategories $(I,E)$ of a category $\mathcal{C}$ such that $I$ is a partial order and every arrow factors uniquely as an abstract surjection followed by an abstract inclusion. The benchmark problem is the theorem that a cospan of abstract inclusions that has a pullback has a unique pullback whose legs are also abstract inclusions. The proof machinery against which the AI outputs are measured consists of the uniqueness of those factorizations, the Diagonal Fill-in property, and the mono property of abstract inclusions; this gives the author a compact, known-correct yardstick that is not readily available as a published solution.
What would settle it
Run the same exercise with a systematic prompt grid—for example, 20 phrasings and 10 trials per system—logging every transcript; if any trial returns a correct definition of inclusion system and a complete, correct proof of both existence and uniqueness of the pullback, the paper's central claim that specific prompts and repeated trials make no significant difference would be falsified.
Extended reading notes
Core claim
On the paper's own terms, the discovery is that a non-mainstream but well-documented concept and a clean exercise reveal a sharp, structured gap in current AI mathematical capability. One system recovered a recognizable but incomplete version of the inclusion-system definition, wrote formulas that mixed two composition conventions and did not parse, and produced a proof that was valid in outline for the existence half but only gestured at the uniqueness half. The other system produced a definition with crucial parts missing and a derived property stated incorrectly, then built its proof on that faulty foundation, so its reasoning was compromised from the start. The author concludes that, modulo language and notation, the first system provided a valid solution to the first part of the problem and that both outputs were relatively useless for the uniqueness part.
Load-bearing premise
The conclusion rests on the assertion that the particular prompts and repeated trials the author used gave both AI systems a fair enough chance, so that their failures reflect the systems themselves rather than bad luck with phrasing.
Editorial extensions
If this is right
- Mathematicians should treat any definition or stated result recalled by an AI system as unverified and check it against the literature; the paper found retrieval of the key concept to be the most unreliable step.
- For proof problems of this shape, AI assistance can supply a credible existence or construction half but not the uniqueness half, so a human must still carry the verification end.
- Developers of math-oriented AI systems should add a meta-level layer that checks the coherence of notation and mathematical language, since one system's mixed composition conventions made some formulas unparseable.
- Users should combine soft AI with deductive verification tools rather than rely on a language model alone; the paper recommends first-order theorem provers for formal checks.
- Competition-style high scores do not transfer to research-style tasks; the paper treats its result as consistent with the much lower success rate reported for research-level benchmarks.
Reading between the lines
- If this single-case pattern holds broadly, the near-term role of general-purpose language models in mathematics is a proof-sketch generator whose every line must be independently verified, with the uniqueness or verification part of a proof being exactly where human effort remains decisive.
- A testable extension would measure how well current models recover definitions stated in narrative prose rather than in formal definition blocks; the paper's evidence suggests recall degrades sharply in that setting.
- Re-running the same benchmark with a system that first loads a vetted definition from a formal library and then proves would separate failures of data gathering from failures of reasoning, a distinction the paper deliberately leaves entangled.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper reports a case study evaluating two AI systems, o3-mini and Grok-3, on a graduate-level exercise in inclusion systems: proving that in any category with an inclusion system, a cospan of abstract inclusions that has a pullback has a unique pullback consisting of abstract inclusions. The author first gives a reference solution, then analyzes the two verbatim AI transcripts under three headings (data gathering, mathematical language, reasoning), and concludes that o3-mini produced a valid proof of the existence part modulo language and notation issues but not of the uniqueness part, while Grok failed from the start because it gave a corrupted definition of inclusion system. The paper closes with recommendations for AI developers and for working mathematicians.
Significance. The concrete, verbatim transcripts are a useful artifact, and the documented failures in definition retrieval and notational consistency are credible and worth recording. In particular, the criticism of Grok's definition (making pullback-stability part of the definition and confusing 'exists' with 'any') and the criticism of o3-mini's notation errors are directly checkable from the appendices and are convincing. However, the central evaluation of o3-mini's reasoning is not supported by the exhibited transcript, and the absence of a rubric, inter-rater reliability, and prompt/trial logs limits the generality of the conclusions. If the assessment of o3-mini's proof were corrected, the paper would be a modest but honest qualitative case study; as written, its main empirical claim is not established.
major comments (4)
- [§3.3, second paragraph] The claim that o3-mini 'factored the diagonal of the starting pullback square rather than one of the sides' is contradicted by Appendix A, where the transcript factors the two projections p and q, i.e., the displayed equations p = e_p ∘ i_p and q = e_q ∘ i_q are exactly factorizations of the two sides of the pullback cone. The section's description therefore does not match the reproduced evidence, so the evaluation is not anchored to the output the reader is asked to inspect.
- [Appendix A, Step 1] The inference that e_p and e_q are isomorphisms is not licensed by Definition 2.1. The uniqueness of factorization applies to factorizations of the same arrow as an E-morphism followed by an I-morphism; to compare the factorizations of i∘p and j∘q and to identify their I-parts, one needs (i∘e_p) and (j∘e_q) to be E-morphisms, which the axioms do not assert. The proof explicitly relies on the phrase 'in many formulations one can prove (or assume)', which §3.2 itself singles out as unacceptable imprecision. Thus the claimed valid first-half proof is not established by the transcript.
- [Appendix A, Step 2] Replacing p and q by i_p and i_q does not produce a pullback cone. The arrows i_p and i_q have different source objects (the intermediate objects introduced by the factorizations), so they do not form a cone over the original cospan, and isomorphic modifications of the legs do not preserve commutativity unless the isomorphism is compatible with the square. The statement that 'isomorphic modifications of the legs do not affect the commutativity' is therefore false as written.
- [§3, methodology paragraph, and §4] The assertion that 'specific prompts and repeated trials did not make any significant difference' is load-bearing for the conclusion that the observed failures are representative, but the paper reports no prompt variants, no trial counts, and no success/failure logs. This should either be documented with the protocol or explicitly downgraded to an anecdotal observation. Without such data, the robustness of the central claim is unverified.
minor comments (4)
- [Abstract and throughout] There are numerous typographical slips, such as 'direct ion', 'o f', 'diference', and inconsistent hyphenation of 'cospan'/'co-span'; a careful copyedit is needed.
- [§3.2] The text refers to 'formulas (1) and (2)' and '(3)' and '(4)', but the equations in Appendix A are not numbered in the reproduced transcript, which makes the cross-reference difficult to follow.
- [§2.2, final uniqueness step] The human solution's uniqueness argument is compressed: it says that by the universal property and by uniqueness of factorizations one gets two mediating inclusions that are inverse, but the details of why the mediating arrows are inclusions and why they are identity are not shown. Since this is the reference solution against which the AI outputs are judged, a fully detailed proof would strengthen the paper.
- [§4, recommendations] The statement that 'any non-human system is bound to hit the wall of what we call understanding' is a philosophical assertion rather than a conclusion of this experiment; it should be clearly labeled as the author's viewpoint.
Circularity Check
Minor self-referential benchmark, but no load-bearing circularity: the evaluation rests on reproduced transcripts and objective failures.
-
other
[Section 1 (methodology, item 2) and Section 2 (The problem); Definition 2.1]
"we thought of involving a simple categorical concept that, on the one hand is not that standard, but on the other hand appears in a significant number of books or articles. Such a concept is that of inclusion system. ... We chose the following exercise from [1]"
The benchmark problem and the correctness standard are taken from the author's own monograph [1] and from the author's own Definition 2.1 of inclusion systems, so the AI output is judged against the author's own framework. This is a self-referential design element, but it is not load-bearing for the central conclusion: the paper reproduces the o3-mini transcript, and the decisive failures (non-parsing formulas (1)-(2), nonsensical formulas (4), and the two-phrase expediting of the uniqueness half) are objectively visible without accepting the author's preferred proof. The self-reference therefore lowers the independence of the benchmark slightly but does not force the result.
full rationale
No fitted parameter is renamed as a prediction, and no claimed mathematical derivation reduces by construction to its inputs. The human solution in Section 2.2 is a standard exercise proof using the stated Definition 2.1 and a cited diagonal fill-in property; the AI evaluation is an empirical judgment about two reproduced transcripts, not a derivation from the benchmark. The only self-referential element is that the benchmark problem is selected from the author's own monograph [1] and the standard of correctness is the author's own definition of inclusion systems. This is a minor self-citation in the experimental design, but it is not load-bearing because the most serious AI failures are objective: malformed formulas, a missing uniqueness proof, and Grok's incorrect definition. A separate correctness risk, not a circularity, is that Section 3.3's description that o3-mini 'factored the diagonal of the starting pullback square' does not match Appendix A, which factors the two sides p and q; this inconsistency affects the evidentiary support for the positive evaluation but does not make the argument circular.
Assumptions & free parameters
assumptions (2)
- domain assumption The standard definition of inclusion systems is the one given in the author's monograph and in Diaconescu et al. (1993)
- domain assumption The AI transcripts in Appendices A and B are genuine, unedited outputs of the two systems
Cite this review
Pith. "Pith review of In between myth and reality: AI for math -- a case study in category theory." pith.science (2026). https://pith.science/paper/5GAIXH56
@misc{pith2026250413360,
author = {Pith},
title = {Pith review of: In between myth and reality: AI for math -- a case study in category theory},
year = {2026},
howpublished = {\url{https://pith.science/paper/5GAIXH56}},
note = {Machine review of arXiv:2504.13360}
}
read the original abstract
Recently, there is an increasing interest in understanding the performance of AI systems in solving math problems. A multitude of tests have been performed, with mixed conclusions. In this paper we discuss an experiment we have made in the direction of mathematical research, with two of the most prominent contemporary AI systems. One of the objective of this experiment is to get an understanding of how AI systems can assist mathematical research. Another objective is to support the AI systems developers by formulating suggestions for directions of improvement.
Reference graph
Works this paper leans on
-
[1]
Diaconescu, R.: Institution-independent Model Theory . Birkh ¨auser (2025). Second, Ex- tended edition
work page 2025
-
[2]
Diaconescu, R., Goguen, J., Stefaneas, P .: Logical supp ort for modularisation. In: G. Huet, G. Plotkin (eds.) Logical Environments, pp. 83–130. Cambri dge (1993). Proceedings of a Workshop held in Edinburgh, Scotland, May 1991
work page 1993
-
[3]
arXiv:2411.04872v5 [cs.AI] (2024)
Elliot Glazer et al.: FrontierMath: a benchmark for eval uating advanced mathematical reasoning in AI. arXiv:2411.04872v5 [cs.AI] (2024)
arXiv 2024
-
[4]
Mac Lane, S.: Categories for the Working Mathematician, second edn. Springer (1998)
work page 1998
-
[5]
URL https://openai.com/index/learning-to-reason-with-ll ms/
OpenAI: Learning to reason with LLMs. URL https://openai.com/index/learning-to-reason-with-ll ms/
- [6]
-
[7]
Oxford University P ress (2016)
Penrose, R.: The Emperor’s New Mind. Oxford University P ress (2016)
work page 2016
- [8]
Show all 13 references
-
[9]
Schulz, S., Cruanes, S., Vukmirovic, P .: Faster, higher , stronger: E 2.3. In: P . Fontaine (ed.) Automated Deduction – CADE 27, Lecture Notes in Computer Science , vol. 11716, pp. 495–507. Springer (2019)
2019
-
[10]
In: Automated Deduction, LNCS, vol
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Sud a, M.., Wischnewski, P .: SPASS version 3.5. In: Automated Deduction, LNCS, vol. 5663, pp. 140–145 (2009)
2009
-
[11]
inclusion-morphisms
xAI: Grok-3. https://grok3ai.org A The o3-mini output LetC be a category equipped with an inclusion system—that is, a fa ctorization system (/u1D438, /u1D43C) where the “inclusion-morphisms” in /u1D43Care thought of as “abstract inclusions” (for example, there is at most one a...
-
[12]
Existence: There exists a pullback /u1D443with /u1D45D1 : /u1D443→ /u1D434and /u1D45D2 : /u1D443→ /u1D435both in /u1D43C
-
[13]
consisting of abstract inclusions
Uniqueness: This pullback is unique up to isomorphism, and any such pull back has its projection morphisms in /u1D43C. Since pullbacks are always unique up to isomorphism in a cate gory (when they exist), the key task is to show that the pullback of this co-span has projecti o...
Reviewed August 16, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.