Pith. sign in

REVIEW 3 major objections 3 minor 75 references

This paper claims that language models, embedded in a workflow of generation followed by expert verification, can already produce proof candidates that resolve live research-level problems in Banach space theory—five open problems are claim

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 18:10 UTC pith:5ILWC6ZE

load-bearing objection Five serious Banach-space theorems with an AI-provenance wrapper; the first four look coherent, but the flagship P5 is missing its technical core and the AI claim is not independently checkable. the 3 major comments →

arxiv 2607.17388 v1 pith:5ILWC6ZE submitted 2026-07-19 math.FA cs.AI

Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory

Antonio Acuaviva , Pablo Acuaviva This is my paper
classification math.FA cs.AI MSC 46B2046B2546B2847B0168T2068T4268T50
keywords AI-assisted mathematicslarge language modelsmathematical discoveryproof verificationBanach space theorytoroidal separationCalkin algebraprimary factorization
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper is trying to establish that current language model systems can do genuine research-level mathematical work, not merely solve exercises, when their outputs are subsequently checked, repaired, and rewritten by human experts. It makes this concrete by presenting five Banach-space theorems whose proof ideas and proof architectures were produced by a model and then human-verified: a toroidal separation theorem for complex normed spaces, a unital Banach algebra that cannot be realized as a Calkin algebra, a duality between strict cosingularity and strict singularity for separable range spaces, a basis-valued refinement of the standard weakly compact factorization theorem, and primariness of Lp(L1). A sympathetic reader would take the contribution as twofold: five previously open problems are claimed resolved, and the workflow itself is offered as evidence that AI-assisted mathematical exploration can be useful at scale when verification remains firmly in human hands.

Core claim

The paper's concrete mathematical discovery is a set of five theorem claims, each generated essentially by a language model and then checked and edited by human experts. Theorem 5.1 states that every infinite-dimensional complex normed space contains unit vectors whose toroidal distances—the infimum of distances after multiplying by unimodular scalars—are all at least 1+epsilon for some epsilon>0. Theorem 6.1 constructs a unital Banach algebra that is not Banach-algebra isomorphic to B(X)/K(X) for any Banach space X. Theorem 7.2 proves that, when the range space is separable, an operator is strictly cosingular if and only if its adjoint is strictly singular. Theorem 8.1 shows that every weak

What carries the argument

The carrying mechanism is a two-stage workflow: model-driven proof search produces candidate proofs and proof architectures, and human experts verify cited results, patch gaps, and rewrite the exposition. Within the individual proofs, the load-bearing devices are reusable mathematical constructions—most notably a rapid flat-block alternative that converts failure of toroidal separation into bounded twisted partial sums of almost-flat blocks; a preadjoint extraction lemma that manufactures weak-star closed witnesses from separable range spaces; a bridge theorem that turns two-sided finite-rank approximation into factorization through a reflexive space with a Schauder basis; and faithful Haar

Load-bearing premise

The argument stands or falls on the completeness of the authors' own post-generation human verification: if any misapplied external result or hidden gap escaped that check, the affected theorem—and the broader demonstration that current models can do serious mathematical work—would collapse.

What would settle it

The decisive test is an independent formalization of the five theorem proofs in an interactive proof assistant; the first step that cannot be derived, or a cited lemma whose hypotheses are not met, would falsify the corresponding theorem. A direct counterexample to any of the five statements—for example, an infinite-dimensional complex normed space whose unit sphere contains no toroidally (1+epsilon)-separated sequence for any epsilon>0—would settle the matter even more quickly.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • If the five proofs are correct, five previously open problems in Banach space theory become theorems, including the toroidal separation question and primariness of Lp(L1).
  • The verification bottleneck becomes the central constraint: generating plausible arguments is now easier than confirming them, so formal proof assistants and structured verification platforms become natural next steps.
  • The automated literature-search pipeline could accelerate the closure of many small unaddressed open problems by extracting them from papers and generating proof candidates at scale.
  • The paper's incentive discussion implies that mathematical communities may need disclosure norms that evaluate results by mathematical content rather than by whether an AI contributed, to avoid penalizing honest AI-assisted work.
  • The same workflow is likely transferable to any field where experts can verify and contextualize generated arguments, meaning the phenomenon is not specific to Banach space theory.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If independent formal verification later confirms the five proofs, the paper would stand as evidence that general-purpose language models can contribute genuinely new mathematics, not merely reorganize known arguments—a shift with consequences for peer review and research training.
  • A natural testable extension would be to run the same model-plus-human-verification workflow on a fresh batch of open problems in a different subfield and compare success rates against human-only attempts under matched effort.
  • The P5 technique of compressing arbitrary operators to diagonal multipliers on carefully chosen faithful Haar systems may transfer to other mixed-norm and bi-parameter spaces beyond Lp(L1).
  • The paper itself notes that the raw P5 output was not a complete proof and required substantial human reorganization, which suggests that current systems are best used as generators of proof architecture rather than as autonomous theorem prover.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 3 minor

Summary. The paper claims that current large language models, when embedded in a human-in-the-loop workflow, can already produce serious proof candidates in research-level mathematics, and it supports this claim with five solved problems in Banach space theory. Part 2 contains the mathematical treatments: a toroidal Elton–Odell theorem (Theorem 5.1), the existence of unital Banach algebras not isomorphic to any Calkin algebra (Theorem 6.1), a converse of Pełczyński's duality theorem for strictly cosingular operators under separability (Theorem 7.2), a weakly compact factorization theorem through a reflexive space with a Schauder basis (Theorem 8.1), and a claimed proof that L_p(L_1) is primary for 1<p<∞ (Theorem 9.1). The paper also announces an automated pipeline for extracting and solving open problems, but the corresponding sections are not included in the review copy. The central epistemic claim is that the final proofs were generated essentially by the model and then verified and edited by the authors.

Significance. If the five theorems are correct, this is a significant mathematical contribution independent of the AI provenance: Theorems 5.1, 6.1, 7.2 and 8.1 solve natural open questions, and Theorem 9.1 would settle a prominent open case in the primarity programme of Lechner–Motakis–Müller–Schlumprecht. The paper is also unusual in that it attempts a documented, self-critical account of AI-assisted proof generation. The available P1–P4 arguments are detailed and internally coherent; I checked P3 line-by-line and made structural checks of P1, P2 and P4, and found no internal error. The main limitations are that the flagship P5 proof is incomplete in the submitted text and that the provenance claim is not independently testable because no raw outputs or repository identifier are provided.

major comments (3)
  1. [§9.1, Theorem 9.31] The proof of the central P5 result is not present in the review copy. Theorem 9.31 is asserted to reduce arbitrary operators on X_00 to product Haar multipliers, and the text explicitly says the required 'formal statements and proofs' of the construction claims are given in Section 10; the scalar-compression conclusion is deferred to Section 11. Neither section is included. Since Theorem 9.1 is derived from Theorem 9.31 and the quoted LMMS scalar-compression theorem, the flagship claim of the paper cannot currently be verified. This is not a routine reference to the literature: Section 2.1 states that the raw P5 output 'could not be regarded as a complete proof as it stood' and that human repair involved reorganizing the proof and making arguments precise. The missing sections must be supplied in full before the result can be assessed.
  2. [§2.1, provenance] The provenance claim is load-bearing for the paper's stated purpose. The text says 'The original AI outputs can be found on the project website,' but no URL, repository identifier, or stable archive is given, and no raw outputs or interaction logs are included. The paper also records that the model 'misattributed a theorem, cited a result imprecisely, or made a small error' and that Problem 5 required substantial human reassembly. Without access to the raw outputs and a precise account of which parts are model-generated and which parts are human-written, the headline claim that current models 'generated key ideas and proofs for five new results' is not independently testable. The authors should provide a permanent link to the outputs and a per-problem description of human intervention.
  3. [Part 3 and Abstract] The Abstract announces 'an automated system that searches the literature for open problems and attempts solutions at scale,' and the Contents list Part 3 as 'Technical and methodological considerations' and 'Selected results from the automated pipeline.' These sections are absent from the submitted text. The automated-pipeline component is therefore unsupported. If the paper is intended to include both components, the missing material must be supplied; otherwise the Abstract and Section 1.1 overstate the scope of the manuscript.
minor comments (3)
  1. [§2.1 and §5] The repeated reference to 'the project website' without a URL should be replaced by a permanent identifier or an appendix containing the raw outputs. This is especially important because the second P1 proof is said to be available only there.
  2. [Contents and §9] The numbering is confusing: Section 10 appears both as 'Technical and methodological considerations' in Part 3 and as 'Technical claims for the multiplier reduction construction' within Problem 5. The duplication should be removed and the P5 deferred material should be placed inside the P5 chapter with unambiguous numbering.
  3. [§9.2, Theorem 9.8] The passage explaining why the LMMS theorem applies to L_p(L_1) is compressed: it cites [52, Theorem 2.10] on unboundedness of Capon's projection and then states 'Consequently...' the scalar compression holds. A more explicit argument, or a pointer to the exact statement in [52], would help the reader verify the applicability of the quoted theorem.

Circularity Check

0 steps flagged

No significant circularity: the five theorem derivations are new and grounded in external cited results; the provenance claim is self-reported but not a reduction of outputs to inputs.

full rationale

The mathematical derivation chain in each of the five problem papers is self-contained in the relevant sense: conclusions are not obtained by definitional equivalence with their inputs. P1 builds toroidally separated sequences from external ingredients (James distortion, [12, Lemma 3.1], [43, Lemma 2.4]) and rules out the flat-block obstruction; P2 constructs algebras and proves non-realizability via density and matrix-unit/shift obstructions rather than assuming the target; P3 proves a preadjoint extraction lemma from separability and standard duality; P4 combines DFJP interpolation with the cited Johnson–Rosenthal–Zippin basisification result; P5 reduces arbitrary operators to product Haar multipliers and invokes the external LMMS scalar-compression theorem. No step fits a parameter to the conclusion and then calls it a prediction, and no load-bearing uniqueness or reduction is imported from the authors' own prior work; the only self-citation ([6]) is background. The paper concedes that the raw Problem 5 output was incomplete and required human reorganization, and the provenance claim is self-reported rather than independently verified, but that is an evidence/reliability limitation, not circularity. Missing Sections 10 and 11 are gaps, not circular reductions. Consequently the correct finding is no significant circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 10 axioms · 3 invented entities

Pure-mathematics paper: no data fitting. The proofs rest on a stack of prior results taken as given (DFJP interpolation, JRZ stabilization, Semenov-Uksusov, LMMS scalar compression, Rosenthal's dichotomy theorems, James distortion) plus the paper's own empirical premise that the proofs were AI-generated and then correctly verified by the authors. No free parameters in the fitting sense; constants such as the epsilon/3 splits in Theorem 9.31 are proof parameters, not fitted values.

axioms (10)
  • standard math Zorn's lemma (existence of maximal proper closed two-sided ideals, Lemma 6.5)
    Used in both P2 constructions to obtain topologically simple quotient algebras B/M.
  • domain assumption James' distortion theorem (P1, Lemma 5.3)
    Transfers toroidally separated sequences from c0/ell1 to any space containing an isomorphic copy.
  • domain assumption Rosenthal's ell1 theorem (Dor's complex version) and Rosenthal's c0 theorem (P1, Section 7)
    Provide the structural dichotomy reducing the nonreflexive case to a strongly summing basic sequence.
  • domain assumption Asymptotically monotone selection [12, Lemma 3.1] and [43, Lemma 2.4] (P1, Lemma 5.7)
    The flat-block alternative (Prop 5.6) is applied only after passing to asymptotically monotone block bases; these two cited results are not reproved.
  • domain assumption DFJP interpolation theorem (P4, Theorem 8.3, [26])
    The bridge theorem's reflexive space Z is the DFJP interpolation space for the weakly compact set K; the construction is imported verbatim.
  • domain assumption Johnson-Rosenthal-Zippin finite-dimensional stabilization, [47, Cor 4.12(a)] (P4, Theorem 8.4)
    Converts the FDD of Z into a complemented embedding into a reflexive space with a Schauder basis; proof sketched, the constant-K stabilization is cited.
  • domain assumption Semenov-Uksusov multiplier theorem, [68, Theorem 3] (P5, Theorem 9.6)
    The L1 multiplier norm equivalence ||Ma|| approx ||a||_W + ||a||_infinity is the quantitative backbone of the inner-coordinate bounds in P5.
  • domain assumption LMMS scalar compression [52, Theorem 2.3] (P5, Theorem 9.8)
    After the multiplier reduction (Thm 9.31), the final scalar-compression step is imported wholesale from Lechner-Motakis-Muller-Schlumprecht.
  • ad hoc to paper Provenance premise: raw LLM outputs were essentially correct up to human verification and editing (Section 2.1)
    The meta-claim ('AI generated proofs for five new results') depends on this; it is asserted, raw outputs are said to be on an unspecified project website, and it is not independently checkable from the text.
  • standard math Standard duality/geometric theorems: Hahn-Banach, closed range theorem, Krein-Smulian, Eberlein-Smulian, Mazur, Banach-Alaoglu, Baire-one properties
    Used throughout: P3 (closed range theorem, finite-dim Goldstine-type Lemma 7.5), P4 (Baire-one Lemma 8.7, Mazur tail-convexification Lemma 8.8), P5 (Krein-Smulian, compactness arguments).
invented entities (3)
  • Leavitt-type quotient algebra A_kappa (P2, first proof) no independent evidence
    purpose: Unital topologically simple Banach algebra of density c^+ carrying a countable matrix-unit system with ell1-type first row; shown not isomorphic to any Calkin algebra.
    Not postulated as a black box: L_kappa, rho, B_kappa, M, A_kappa are explicitly constructed and Lemmas 6.4-6.10 prove the properties used; evidence is internal to the paper, hence independent_evidence=false by the schema's definition.
  • Shift quotient algebra A_lambda on c0(Gamma^<omega), lambda = beth_omega (P2, second proof) no independent evidence
    purpose: Topologically simple algebra of density lambda whose shift relations force a copy of c0 in any realizing X, contradicting simplicity of Q(X).
    Explicitly constructed with all properties proved; the objects sigma_j, tau_j in A_lambda are defined and their estimates proved in Lemmas 6.11-6.15; evidence is internal, hence false by the schema's definition.
  • Faithful Haar systems and random Haar blocks (P5) no independent evidence
    purpose: Scattered dyadic-tree-indexed systems used to compress arbitrary operators on X00 to product-Haar multipliers with small off-diagonal part.
    Definitions 9.12-9.15 and 9.17-9.23 construct these objects; the probabilistic estimates (Props 9.20, Lemmas 9.25-9.30) are proved rather than assumed; evidence is internal, hence false by the schema's definition.

pith-pipeline@v1.3.0-alltime-deepseek · 65636 in / 34870 out tokens · 345065 ms · 2026-08-01T18:10:08.511249+00:00 · methodology

0 comments
read the original abstract

We investigate the capacity of current language models to contribute to mathematical research. In Banach space theory, AI systems generated key ideas and proofs for five new results, which were then verified and refined by humans. We also developed an automated system that searches the literature for open problems and attempts solutions at scale. Our results show both the potential of language models for mathematical discovery and the continuing importance of expert verification.

Figures

Figures reproduced from arXiv: 2607.17388 by Antonio Acuaviva, Pablo Acuaviva.

Figure 1
Figure 1. Figure 1: Operational view of the automatic proof￾discovery pipeline. Candidate setup builds the target queue; agent work consults run memory, makes a packet or attempt note, and passes the result to human review. important because open questions, theorem environments, definitions, and references can be located more reliably in source form than from PDF text extraction. The second box, source signals, is a deliberat… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

75 extracted references · 31 canonical work pages

  1. [1]

    Abouzaid, A

    M. Abouzaid, A. J. Blumberg, M. Hairer, J. Kileel, T. G. Kolda, P. D. Nelson, D. Spielman, N. Srivastava, R. Ward, S. Weinberger, and L. Williams,First Proof, arXiv:2602.05192, 2026

    arXiv 2026

  2. [2]

    Abouzaid, N

    M. Abouzaid, N. Srivastava, R. Ward, and L. Williams,First Proof Second Batch, arXiv:2606.18119, 2026

    Pith/arXiv arXiv 2026

  3. [3]

    Abrams and G

    G. Abrams and G. Aranda Pino,The Leavitt path algebra of a graph, J. Algebra 293 (2005), no. 2, 319–334.doi:10.1016/j.jalgebra.2005.07.028

    work page doi:10.1016/j.jalgebra.2005.07.028 2005

  4. [4]

    Abrams, P

    G. Abrams, P. Ara, and M. Siles Molina,Leavitt Path Algebras, Lecture Notes in Mathematics 2191, Springer, London, 2017.doi:10.1007/978-1-4471-7344-1

    doi:10.1007/978-1-4471-7344-1 2017

  5. [5]

    Achim et al.,Aristotle: IMO-level automated theorem proving,arXiv:2510.01346, 2025

    T. Achim et al.,Aristotle: IMO-level automated theorem proving,arXiv:2510.01346, 2025

    Pith/arXiv arXiv 2025

  6. [6]

    Acuaviva,Primariness of the spacesℓp(C(K))for1≤p≤∞,arXiv:2605.29854 [math.FA], 2026

    A. Acuaviva,Primariness of the spacesℓp(C(K))for1≤p≤∞,arXiv:2605.29854 [math.FA], 2026

    Pith/arXiv arXiv 2026

  7. [7]

    Albiac and N

    F. Albiac and N. J. Kalton,Topics in Banach Space Theory, 2nd ed., Graduate Texts in Mathematics 233, Springer, 2016.doi:10.1007/978-3-319-31557-7

    doi:10.1007/978-3-319-31557-7 2016

  8. [8]

    Androulakis and K

    G. Androulakis and K. Beanland,Descriptive set theoretic methods applied to strictly singular and strictly cosingular operators, Quaest. Math. 31 (2008), no. 2, 151–161. doi:10.2989/qm.2008.31.2.4.476

    work page doi:10.2989/qm.2008.31.2.4.476 2008

  9. [9]

    P. Ara, M. A. Moreno, and E. Pardo,Nonstable K-theory for graph algebras, Algebr. Represent. Theory 10 (2007), no. 2, 157–178.doi:10.1007/s10468-006-9044-z

    work page doi:10.1007/s10468-006-9044-z 2007

  10. [10]

    S. A. Argyros and R. G. Haydon,A hereditarily indecomposableL∞-space that solves the scalar-plus-compact problem, Acta Math.206(2011), no. 1, 1–54.doi:10.1007/ s11511-011-0058-y

    2011

  11. [11]

    S. A. Argyros, V. Kanellopoulos, and K. Tyros,Higher order spreading models, Fund. Math. 221 (2013), no. 1, 23–68.doi:10.4064/fm221-1-2

    work page doi:10.4064/fm221-1-2 2013

  12. [12]

    C. S. Barroso,A note on asymptotically monotone basic sequences and well-separated sets,arXiv:1902.10857, 2019

    Pith/arXiv arXiv 1902

  13. [13]

    C. S. Barroso and V. Ferreira,Retraction methods and fixed point free maps on unit balls, J. Fixed Point Theory Appl.28(2026), Paper No. 51.doi:10.1007/ s11784-026-01310-x

    2026

  14. [14]

    C. S. Barroso,Hölder-contractive mappings, nonlinear extension problem and fixed point free results, J. Math. Anal. Appl.528(2023), no. 1, Paper No. 127521.doi: 10.1016/j.jmaa.2023.127521

    arXiv 2023

  15. [15]

    Baudier and G

    F. Baudier and G. Lancien,Tight embeddability of proper and stable metric spaces, Anal. Geom. Metr. Spaces3(2015), no. 1, 140–156.doi:10.1515/agms-2015-0010

    work page doi:10.1515/agms-2015-0010 2015

  16. [16]

    Beanland,Davis, Figiel, Johnson and Pełczyński factorization through spaces with a bases, MathOverflow, Question 240472, 2016

    K. Beanland,Davis, Figiel, Johnson and Pełczyński factorization through spaces with a bases, MathOverflow, Question 240472, 2016. Permanent link

    2016

  17. [17]

    Beanland,Strictly singular operators and their adjoints, MathOverflow, Question 98449, 2012

    K. Beanland,Strictly singular operators and their adjoints, MathOverflow, Question 98449, 2012. Permanent link

    2012

  18. [18]

    Beauzamy and J.-T

    B. Beauzamy and J.-T. Lapreste,Modèles étalés des espaces de Banach, Travaux en Cours, Hermann, Paris, 1984. Online version (1983)

    1984

  19. [19]

    Benyamini and Y

    Y. Benyamini and Y. Sternfeld,Spheres in infinite-dimensional normed spaces are Lipschitz contractible, Proc. Amer. Math. Soc.88(1983), no. 3, 439–445.doi:10. 1090/s0002-9939-1983-0699410-7

    1983

  20. [20]

    1, 71–97.doi:10.4064/sm8604-11-2016

    B.deMendonçaBraga,Asymptotic structure and coarse Lipschitz geometry of Banach spaces, Studia Math.237(2017), no. 1, 71–97.doi:10.4064/sm8604-11-2016

    work page doi:10.4064/sm8604-11-2016 2017

  21. [21]

    Brunel and L

    A. Brunel and L. Sucheston,OnB-convex Banach spaces, Math. Systems Theory7 (1974), no. 4, 294–299.doi:10.1007/BF01795947

    work page doi:10.1007/bf01795947 1974

  22. [22]

    Capon,Primarité deLp(X), Trans

    M. Capon,Primarité deLp(X), Trans. Amer. Math. Soc.276(1983), no. 2, 431–487. doi:10.2307/1999061. References 139

    work page doi:10.2307/1999061 1983

  23. [23]

    D. Chen, E. Chen, K. Lau, K. Ono, and J. Zhang,Parity ofk-differentials in genus zero and one,arXiv:2602.03722, 2026

    Pith/arXiv arXiv 2026

  24. [24]

    L. Chen, Z. Liu, W. He, and B. Dong,Iteris: Agentic research loops for computational mathematics,arXiv:2606.02484, 2026

    Pith/arXiv arXiv 2026

  25. [25]

    E. Chen, K. Ono, and J. Zhang,Reciprocals of partition polynomials,arXiv:2605. 21718, 2026

    2026

  26. [26]

    W. J. Davis, T. Figiel, W. B. Johnson, and A. Pełczyński,Factoring weakly compact operators, J. Functional Analysis 17 (1974), 311–327.doi:10.1016/0022-1236(74) 90044-5

    work page doi:10.1016/0022-1236(74 1974

  27. [27]

    Diestel and J

    J. Diestel and J. J. Uhl, Jr.,Vector Measures, Mathematical Surveys, No. 15, Amer- ican Mathematical Society, Providence, RI, 1977.doi:10.1090/surv/015

    doi:10.1090/surv/015 1977

  28. [28]

    Dodos,Banach Spaces and Descriptive Set Theory: Selected Topics, Lecture Notes in Mathematics 1993, Springer, Berlin, 2010.doi:10.1007/978-3-642-12153-1

    P. Dodos,Banach Spaces and Descriptive Set Theory: Selected Topics, Lecture Notes in Mathematics 1993, Springer, Berlin, 2010.doi:10.1007/978-3-642-12153-1

    work page doi:10.1007/978-3-642-12153-1 1993

  29. [29]

    Dodos and V

    P. Dodos and V. Ferenczi,Some strongly bounded classes of Banach spaces, Fund. Math. 193 (2007), no. 2, 171–179.doi:10.4064/fm193-2-5

    work page doi:10.4064/fm193-2-5 2007

  30. [30]

    L. E. Dor,On sequences spanning a complexℓ 1 space, Proc. Amer. Math. Soc.47 (1975), no. 2, 515–516.doi:10.1090/S0002-9939-1975-0358308-X

    work page doi:10.1090/s0002-9939-1975-0358308-x 1975

  31. [31]

    J. S. Ellenberg, C. S. Fraser-Taliente, T. R. Harvey, K. Srivastava, and A. V. Suther- land,Generative Modeling for Mathematical Discovery,arXiv:2503.11061, 2025

    Pith/arXiv arXiv 2025

  32. [32]

    Elton and E

    J. Elton and E. Odell,The unit ball of every infinite-dimensional normed linear space contains a(1 +ε)-separated sequence, Colloq. Math. 44 (1981), no. 1, 105–109. doi:10.4064/cm-44-1-105-109

    work page doi:10.4064/cm-44-1-105-109 1981

  33. [33]

    Epoch AI,FrontierMath: Benchmarking AI against advanced mathematical research, Project page, accessed 19 July 2026

    2026

  34. [34]

    Feng et al.,Aletheia tackles FirstProof autonomously,arXiv:2602.21201, 2026

    T. Feng et al.,Aletheia tackles FirstProof autonomously,arXiv:2602.21201, 2026

    arXiv 2026

  35. [35]

    Feng et al.,Towards autonomous mathematics research,arXiv:2602.10177, 2026

    T. Feng et al.,Towards autonomous mathematics research,arXiv:2602.10177, 2026

    arXiv 2026

  36. [36]

    Figiel, W

    T. Figiel, W. B. Johnson, and L. Tzafriri,On Banach lattices and spaces having local unconditional structure, with applications to Lorentz function spaces, J. Approxima- tion Theory 13 (1975), 395–412.doi:10.1016/0021-9045(75)90023-4

    work page doi:10.1016/0021-9045(75)90023-4 1975

  37. [37]

    Freeman, E

    D. Freeman, E. Odell, B. Sari, and B. Zheng,On spreading sequences and asymptotic structures, Trans. Amer. Math. Soc. 370 (2018), no. 10, 6933–6953.doi:10.1090/ tran/7189

    2018

  38. [38]

    Galvin and K

    F. Galvin and K. Prikry,Borel sets and Ramsey’s theorem, J. Symbolic Logic 38 (1973), 193–198.doi:10.2307/2272055

    work page doi:10.2307/2272055 1973

  39. [39]

    Georgiev, J

    B. Georgiev, J. Gómez-Serrano, T. Tao, and A. Z. Wagner,Mathematical exploration and discovery at scale,arXiv:2511.02864, 2025

    Pith/arXiv arXiv 2025

  40. [40]

    Ghoussoub, B

    N. Ghoussoub, B. Maurey, and W. Schachermayer,Slicings, selections and their ap- plications, Canadian J. Math. 44 (1992), 483–504.doi:10.4153/CJM-1992-031-6

    work page doi:10.4153/cjm-1992-031-6 1992

  41. [41]

    Glazer et al.,FrontierMath: A benchmark for evaluating advanced mathematical reasoning in AI,arXiv:2411.04872, 2024

    E. Glazer et al.,FrontierMath: A benchmark for evaluating advanced mathematical reasoning in AI,arXiv:2411.04872, 2024

    Pith/arXiv arXiv 2024

  42. [42]

    K. R. Goodearl,Leavitt path algebras and direct limits, Contemp. Math. 480 (2009), 165–187.doi:10.1090/conm/480/09374

    work page doi:10.1090/conm/480/09374 2009

  43. [43]

    Hájek, T

    P. Hájek, T. Kania, and T. Russo,Symmetrically separated sequences in the unit sphere of a Banach space, J. Funct. Anal. 275 (2018), no. 11, 3148–3168.doi:10. 1016/j.jfa.2018.01.008

    2018

  44. [44]

    Horváth and T

    B. Horváth and T. Kania,Unital Banach algebras not isomorphic to Calkin algebras of separable Banach spaces, Proc. Amer. Math. Soc.149(2021), no. 11, 4781–4787. doi:10.1090/proc/15589

    work page doi:10.1090/proc/15589 2021

  45. [45]

    R. C. James,Uniformly non-square Banach spaces, Ann. of Math. (2) 80 (1964), 542–550.doi:10.2307/1970663

    work page doi:10.2307/1970663 1964

  46. [46]

    Jin et al.,Toward generalist autonomous research via hypothesis-tree refinement, arXiv:2606.11926, 2026

    J. Jin et al.,Toward generalist autonomous research via hypothesis-tree refinement, arXiv:2606.11926, 2026. 140 References

    Pith/arXiv arXiv 2026

  47. [47]

    W. B. Johnson, H. P. Rosenthal, and M. Zippin,On bases, finite dimensional decom- positions and weaker structures in Banach spaces, Israel J. Math. 9 (1971), 488–506. doi:10.1007/BF02771464

    work page doi:10.1007/bf02771464 1971

  48. [48]

    Ju et al.,Automated conjecture resolution with formal verification,arXiv:2604

    H. Ju et al.,Automated conjecture resolution with formal verification,arXiv:2604. 03789, 2026

    2026

  49. [49]

    M. I. Kadec and A. Pełczyński,Bases, lacunary sequences and complemented subspaces in the spacesL p, Studia Math. 21 (1962), 161–176.doi:10.4064/ sm-21-2-161-176

    1962

  50. [50]

    Kania,Toroidal separation in complex normed space, preprint, 2026

    T. Kania,Toroidal separation in complex normed space, preprint, 2026

    2026

  51. [51]

    Lechner, P

    R. Lechner, P. Motakis, P. F. X. Müller, and T. Schlumprecht,The spaceL1(Lp) is primary for1< p <∞, Forum Math. Sigma 10 (2022), Paper No. e32, 36 pp. doi:10.1017/fms.2022.25

    work page doi:10.1017/fms.2022.25 2022

  52. [52]

    Lechner, P

    R. Lechner, P. Motakis, P. F. X. Müller, and T. Schlumprecht,Multipliers on bi- parameter Haar system Hardy spaces, Math. Ann. 390 (2024), no. 4, 5669–5752. doi:10.1007/s00208-024-02887-9

    work page doi:10.1007/s00208-024-02887-9 2024

  53. [53]

    Chris Lu, Cong Lu, R. T. Lange, J. Foerster, J. Clune, and D. Ha,The AI Scientist: Towards fully automated open-ended scientific discovery,arXiv:2408.06292, 2024

    Pith/arXiv arXiv 2024

  54. [54]

    Mitchener et al.,Kosmos: An AI Scientist for autonomous discovery,arXiv: 2511.02824, 2025

    L. Mitchener et al.,Kosmos: An AI Scientist for autonomous discovery,arXiv: 2511.02824, 2025

    Pith/arXiv arXiv 2025

  55. [55]

    Motakis,Separable spaces of continuous functions as Calkin algebras, J

    P. Motakis,Separable spaces of continuous functions as Calkin algebras, J. Amer. Math. Soc.37(2024), no. 1, 1–37.doi:10.1090/jams/1024

    work page doi:10.1090/jams/1024 2024

  56. [56]

    Motakis and A

    P. Motakis and A. Pelczar-Barwacz,Reflexive Calkin algebras, J. Eur. Math. Soc., published online first, 2025.doi:10.4171/JEMS/1709

    work page doi:10.4171/jems/1709 2025

  57. [57]

    Motakis and D

    P. Motakis and D. Puglisi,The compact operators onc0 as a Calkin algebra, Pure Appl. Funct. Anal.10(2025), no. 4, 945–966.arXiv:2403.04137

    Pith/arXiv arXiv 2025

  58. [58]

    Motakis, D

    P. Motakis, D. Puglisi, and A. Tolias,Algebras of diagonal operators of the form scalar-plus-compact are Calkin algebras, Michigan Math. J.69(2020), no. 1, 97–152. doi:10.1307/MMJ/1574845272

    arXiv 2020

  59. [59]

    Motakis, D

    P. Motakis, D. Puglisi, and D. Zisimopoulou,A hierarchy of Banach spaces withC(K) Calkin algebras, Indiana Univ. Math. J.65(2016), no. 1, 39–67. Journal page

    2016

  60. [60]

    Novikov et al.,AlphaEvolve: A coding agent for scientific and algorithmic discov- ery,arXiv:2506.13131, 2025

    A. Novikov et al.,AlphaEvolve: A coding agent for scientific and algorithmic discov- ery,arXiv:2506.13131, 2025

    Pith/arXiv arXiv 2025

  61. [61]

    Pełczyński,On strictly singular and strictly cosingular operators

    A. Pełczyński,On strictly singular and strictly cosingular operators. I. Strictly singu- lar and strictly cosingular operators inC(S)-spaces, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 13 (1965), 31–36. MR0177300

    1965

  62. [62]

    Pełczyński,Any separable Banach space with the bounded approximation property is a complemented subspace of a Banach space with a basis, Studia Math

    A. Pełczyński,Any separable Banach space with the bounded approximation property is a complemented subspace of a Banach space with a basis, Studia Math. 40 (1971), 239–243.doi:10.4064/sm-40-3-239-243

    work page doi:10.4064/sm-40-3-239-243 1971

  63. [63]

    Peyronnet, F

    A. Peyronnet, F. Gloeckle, and A. Hayat,LemmaBench: A live, research-level bench- mark to evaluate LLM capabilities in mathematics,arXiv:2602.24173, 2026

    Pith/arXiv arXiv 2026

  64. [64]

    Romera-Paredes et al.,Mathematical discoveries from program search with large language models, Nature 625 (2024), 468–475.doi:10.1038/s41586-023-06924-6

    B. Romera-Paredes et al.,Mathematical discoveries from program search with large language models, Nature 625 (2024), 468–475.doi:10.1038/s41586-023-06924-6

    doi:10.1038/s41586-023-06924-6 2024

  65. [65]

    H. P. Rosenthal,A characterization of Banach spaces containingℓ1, Proc. Nat. Acad. Sci. U.S.A. 71 (1974), no. 6, 2411–2413.doi:10.1073/pnas.71.6.2411

    work page doi:10.1073/pnas.71.6.2411 1974

  66. [66]

    H. P. Rosenthal,A characterization of Banach spaces containingc0, J. Amer. Math. Soc. 7 (1994), no. 3, 707–748.doi:10.1090/S0894-0347-1994-1242455-4

    work page doi:10.1090/s0894-0347-1994-1242455-4 1994

  67. [67]

    Schmitt et al.,IMProofBench: Benchmarking AI on research-level mathematical proof generation,arXiv:2509.26076, 2025

    J. Schmitt et al.,IMProofBench: Benchmarking AI on research-level mathematical proof generation,arXiv:2509.26076, 2025

    Pith/arXiv arXiv 2025

  68. [68]

    E. M. Semenov and S. N. Uksusov,Multipliers of the Haar series, Siberian Math. J. 53 (2012), no. 2, 310–315.doi:10.1134/S0037446612020139

    work page doi:10.1134/s0037446612020139 2012

  69. [69]

    Stegall,Functions of the first Baire class with values in Banach spaces, Proc

    C. Stegall,Functions of the first Baire class with values in Banach spaces, Proc. Amer. Math. Soc. 111 (1991), 981–991.doi:10.1090/S0002-9939-1991-1019283-7

    work page doi:10.1090/s0002-9939-1991-1019283-7 1991

  70. [70]

    Talponen,Constructions of sequential spaces,arXiv:0905.0812, 2009

    J. Talponen,Constructions of sequential spaces,arXiv:0905.0812, 2009. References 141

    Pith/arXiv arXiv 2009

  71. [71]

    Tarbard,Operators on Banach spaces of Bourgain–Delbaen type, D.Phil

    M. Tarbard,Operators on Banach spaces of Bourgain–Delbaen type, D.Phil. thesis, University of Oxford, 2013.doi:10.5287/ora-8n7rzq1ny

    work page doi:10.5287/ora-8n7rzq1ny 2013

  72. [72]

    Tomforde,Uniqueness theorems and ideal structure for Leavitt path algebras, J

    M. Tomforde,Uniqueness theorems and ideal structure for Leavitt path algebras, J. Algebra 318 (2007), no. 1, 270–299.doi:10.1016/j.jalgebra.2007.01.031

    work page doi:10.1016/j.jalgebra.2007.01.031 2007

  73. [73]

    Yamada, R

    Y. Yamada, R. T. Lange, Cong Lu, S. Hu, Chris Lu, J. Foerster, J. Clune, and D. Ha,The AI Scientist-v2: Workshop-level automated scientific discovery via agentic tree search,arXiv:2504.08066, 2025

    Pith/arXiv arXiv 2025

  74. [74]

    J. M. Zhang, C. Petrui, K. Nikolić, and F. Tramèr,RealMath: A continuous bench- mark for evaluating language models on research-level mathematics, inAdvances in Neural Information Processing Systems 38, Datasets and Benchmarks Track, 2025. Proceedings page

    2025

  75. [75]

    Zheng et al.,AI co-mathematician: Accelerating mathematicians with agentic AI, arXiv:2605.06651, 2026

    D. Zheng et al.,AI co-mathematician: Accelerating mathematicians with agentic AI, arXiv:2605.06651, 2026. School of Mathematical Sciences, Fylde College, Lancaster University, LA1 4YF, United Kingdom Email address:ahacua@gmail.com Institute of Computer Science, University of Bern, Neubrückstrasse 10, 3012 Bern, Switzerland Email address:pablohacuaviva@gmail.com

    Pith/arXiv arXiv 2026