% part07a_theory.tex — Part VII (theory half): algorithms and data structures, computational complexity, programming
% languages, compilers, formal verification, software engineering. Agent G (Theory Specialist), 2026-11-03.
% The director merges this file with part07b_security.tex into Part VII. Every corpus number is a macro of
% tables/numbers.tex (prefix \Thy..., appended by tables/make_numbers.py, Agent G block) or appears in a generated table
% (tables/make_tables.py, tables_part07a). Sources: results/graph/category_counts_yearly.csv, category_flows_yearly.csv,
% category_cooccurrence_yearly.csv; results/econometrics/breaks.csv; literature_synthesis/landmarks/{theory,software_pl}_*;
% literature_synthesis/agent_G/{claims,contributions,open_problems}.csv and review.md. Bibliography: references.bib and
% references_part07a.bib (65 entries, each resolved by one live lookup; references_verification_part07a.csv).

\section{Scope, evidence and reading rules for the theory half}
\label{sec:thy-scope}

This half of Part~VII reviews six categories of the taxonomy: algorithms and data structures, computational
complexity, programming languages, compilers, formal verification and software engineering (the areas
\emph{theory} and \emph{software\_pl} of the ontology, Section~\ref{sec:p2-ontology}). It has two objects. The
first is the research itself: what the baseline period established in these categories, what the window added,
and where the additions are contested. The second is the instrument: the corpus statistics for the six
categories and, above all, the automatically selected landmark candidates, which in these areas turn out to
measure the bibliographic record more than the research it records. The two objects cannot be separated,
because the landmark list is the protocol's channel from corpus to synthesis, and in the theory and software
areas that channel is obstructed in ways that are themselves findings.

Three reading rules apply. First, no full text was read. Every statement about a work rests on its metadata
(title, venue, type, year, identifiers) or on the abstract recorded in OpenAlex, and the text says which; where
an abstract is the source, the phrase ``the abstract reports'' is used deliberately. Second, works available
only as arXiv postings are preprints and are described as such, whatever their later fate. Third, the
structural-change statistics are read as the protocol prescribes (Section~\ref{sec:m-structural}): the November
2022 boundary is a reference date, the placebo distribution is the test, and nothing below attributes a change
to any single event. The categories are small relative to the AI categories of Part~V (their combined primary
share in 2025 is under ten per cent of the corpus), so the statistics are those of minorities inside a
corpus whose growth is set elsewhere.

The section proceeds from the instrument to the field. Section~\ref{sec:thy-landmarks} audits the landmark
candidates; Section~\ref{sec:thy-statistics} reports the six categories' volume, structural-change and
composition statistics; Sections~\ref{sec:thy-algorithms} to~\ref{sec:thy-se} review the categories; and
Section~\ref{sec:thy-synthesis} draws the conclusions that Part~X and Part~XI inherit.

\section{The landmark candidates: an audit}
\label{sec:thy-landmarks}

The protocol selects landmarks as the works with the highest field-normalised 36-month citation score
(NCS36, Section~\ref{sec:m-citations}) within each primary category, with a floor of fifteen per category, plus
the 200 most cited works overall; for 2025--2026 works the 12-month window replaces the 36-month one
(Section~\ref{sec:data-core}). The theory area contributed \ThyLandTheoryN{} candidates and the software area
\ThyLandSoftwarePlN{}, twenty-five per category, of the \SelectionLandmarks{} landmarks of the whole corpus.
Before any of the \ThyAuditN{} can be called a landmark, the list has to be audited, and the audit is the first
result of this section (Table~\ref{tab:theory_landmark_audit}). Each candidate received one of eight verdicts
from its metadata and, where available, its abstract: an in-scope research contribution
(\ThyAuditVerdictInScopeResearch{} candidates), an in-scope survey or report (\ThyAuditVerdictInScopeSurvey{}),
a misclassified work outside the category and outside the theory and software scope
(\ThyAuditVerdictMisclassified{}), a thesis (\ThyAuditVerdictDissertation{}), a classic re-deposited under a
recent record date (\ThyAuditVerdictReprintMisdated{}), a textbook or chapter (\ThyAuditVerdictTextbook{}), a
metaphor-based metaheuristic (\ThyAuditVerdictMetaheuristic{}) or a duplicate record
(\ThyAuditVerdictDuplicate{}). Fewer than one candidate in five is a research contribution inside its
category, and only \ThyAuditInScopeResearchPost{} of those are post-period works. Four mechanisms account
for the rest.

\input{tables/tab_theory_landmark_audit}

\paragraph{Identifier collisions.}
\ThyAuditIdCollision{} candidates carry OpenAlex identifiers that, resolved against the live database on
3~November 2026, return a different work. The record titled ``Exploiting Generative AI to Scale up Intelligent
Tutoring Systems'', with the DOI of an ITP~2023 paper, resolves to \emph{Attention Is All You Need}; the abstract
stored for it in the corpus is that of \emph{MizAR~60 for Mizar~50}, which is what the DOI denotes
\citep{jakubuv2023mizar}; its 36-month citation count in the corpus is that of the Transformer paper, which is
why it ranks first in the whole software area. The ECOOP~2025 paper on functionality-specific
vulnerabilities \citep{chen2025apiss} resolves to the graph-convolutional-network preprint; the SEA~2024
paper on learned branching for maximum independent set \citep{langedal2024mis} to GraphSAGE; the WADS~2025
Kd-tree paper \citep{pham2025kdtree} to the variational-autoencoder preprint; the SAIA~2024 robustness
framework \citep{awadid2025robust} to the adversarial-training preprint of Madry and co-authors; an
ESEM~2026 record \citep{naqvi2026bigger} to the Codex paper; and a DX~2024 answer-set-programming paper
\citep{klampfl2024asp} to an unrelated preprint. In every case the recorded citation window matches the other
work's count.\footnote{Raw responses in \texttt{literature\_synthesis/agent\_G/verification\_lookups\_raw.txt}.
The mechanism (identifier merging or reuse between the snapshot of 14~October 2026 and the live database) is
inferred; the consequence, that the citation windows of these records belong to other works, is observed.} The
four top-ranked candidates of the software area and the top-ranked candidate of the theory area owe their rank
to citations that are not theirs. The same check should be run on the other areas' lists before Part~IX uses
them.

\paragraph{Generic-title chapters.}
Chapters titled ``Introduction to Algorithms'' (2020, 2021, 2023), ``Particle Swarm Optimization'' (2019),
``Introduction to Software Testing'' (2021), ``Introduction to Graph Theory'' (2023), and Royce's 1970 paper on
managing large software developments reprinted in a 2021 anthology, carry hundreds to thousands of citations in
their windows, and live lookups confirm the counts. The plausible reading, offered as an interpretation, is
that citations intended for the canonical work are attributed to a same-titled chapter by the indexer's
reference matching. Whatever the mechanism, a chapter of a 2023 undergraduate textbook is not a landmark of
2023 research.

\paragraph{Re-deposited classics.}
\ThyAuditVerdictReprintMisdated{} records are works whose record date is the date of a deposit, reprint or
re-posting rather than of the work. Dijkstra's 1959 note on two problems in connexion with graphs appears as a
2022 ACM Books chapter; Turing's 1936 paper as a 2021 MIT Press chapter; the 1994 survey of decidability for
Petri nets as a 2024 arXiv posting; Lynch and Tuttle's introduction to input/output automata as a 2026 journal
article \citep{lynch2026ioautomata}; the \emph{egg} equality-saturation paper \citep{willsey2021egg} as a 2026
research highlight \citep{willsey2026eggcacm}; doctoral theses of the early 2000s as 2026 repository records;
three theses of the L4/seL4 verification school as 2022 records; and the 2018 conference paper on online
algorithms with machine-learned predictions as a 2024 arXiv posting. Because the year field is the deposit year,
these records enter the post period: \ThyLandTheoryDatedTwentysix{} of the \ThyLandTheoryN{} theory candidates
and \ThyLandSoftwarePlDatedTwentysix{} of the \ThyLandSoftwarePlN{} software candidates are dated 2026, a year
of which the corpus holds ten months.

\paragraph{Lexical misclassification and small cells.}
\ThyAuditVerdictMisclassified{} candidates are outside the theory and software scope altogether. The
computational-complexity list contains \ThyAuditComputationalComplexityMisclassified{} such works of its
\ThyAuditComputationalComplexityN{}: technology-acceptance models of mobile learning, PLS-SEM studies of
small enterprises and of students' well-being, a Routledge volume on complexity theory in the social sciences,
a review of fringe-projection profilometry, captured by the word ``complexity''. The compilers list contains
\ThyAuditCompilersMisclassified{}, captured by ``just-in-time'' (adaptive interventions in mental health),
``compiling'' (a guide to literature reviews) and ``polyhedral'' (power-system dispatch). The
programming-languages list includes a Nature paper on Calabi--Yau manifolds in black-hole scattering. The
classifier's per-category precision, estimated on the validation sample (Section~\ref{sec:m-validation}), is
the right place to quantify this; what the landmark list shows is the interaction between imprecision and
normalisation. NCS36 divides a work's citations by the expectation for its category, year and type
(Section~\ref{sec:m-citations}); cells of theses or of non-computing articles are small and lightly cited, so a
thesis with a handful of citations, or a social-science article with a hundred, obtains a normalised score that
no STOC paper of the same year can match. \ThyAuditVerdictDissertation{} of the \ThyAuditN{} candidates are
theses.

What survives is a set of \ThyAuditVerdictInScopeResearch{} research works and \ThyAuditVerdictInScopeSurvey{}
surveys or reports, listed in Table~\ref{tab:theory_landmarks_discussed}. They are reviewed below with the
pre-2022 lineage of Part~II and with the window's results that the ranking does not see: the major theoretical
results of 2022--2025 are absent from the candidate list and enter this review through verified bibliographic
records, not through the corpus ranking. Open problem~G-P1 of Part~X states the correction: type filters,
live re-resolution of identifiers and venue priors at the selection stage, evaluated against a
specialist-labelled sample.

\input{tables/tab_theory_landmarks_discussed}

\section{Volume, structural change and composition}
\label{sec:thy-statistics}

\subsection{Growth in absolute terms, decline in relative terms}

Table~\ref{tab:theory_counts} gives the yearly counts of works carrying each category (multi-label) and of
works whose primary category it is; Table~\ref{tab:theory_summary} summarises growth and structural change.
The multi-label counts grew in every category after 2022. Between 2023 and 2025 the compound annual growth was
\ThyCagrMultilabelSoftwareEngineeringPostPct\% for software engineering,
\ThyCagrMultilabelComputationalComplexityPostPct\% for computational complexity,
\ThyCagrMultilabelCompilersPostPct\% for compilers, \ThyCagrMultilabelAlgorithmsPostPct\% for algorithms,
\ThyCagrMultilabelFormalVerificationPostPct\% for formal verification and
\ThyCagrMultilabelProgrammingLanguagesPostPct\% for programming languages, against
\ThyCagrMultilabelSoftwareEngineeringBaselinePct\%, \ThyCagrMultilabelComputationalComplexityBaselinePct\%,
\ThyCagrMultilabelCompilersBaselinePct\%, \ThyCagrMultilabelAlgorithmsBaselinePct\%,
\ThyCagrMultilabelFormalVerificationBaselinePct\% and \ThyCagrMultilabelProgrammingLanguagesBaselinePct\%
between 2018 and 2022. The acceleration is real but not specific: the corpus-wide multi-label growth rose from
\ThyCagrMultilabelTotalBaselinePct\% to \ThyCagrMultilabelTotalPostPct\% over the same periods, so the six
categories accelerated with the corpus rather than within it. Measured by primary-label share, every category
lost ground between 2018 and 2025: algorithms from \ThySharePrimaryAlgorithmsTwoZeroOneEightPct\% to
\ThySharePrimaryAlgorithmsTwoZeroTwoFivePct\%, software engineering from
\ThySharePrimarySoftwareEngineeringTwoZeroOneEightPct\% to \ThySharePrimarySoftwareEngineeringTwoZeroTwoFivePct\%,
formal verification from \ThySharePrimaryFormalVerificationTwoZeroOneEightPct\% to
\ThySharePrimaryFormalVerificationTwoZeroTwoFivePct\%, programming languages from
\ThySharePrimaryProgrammingLanguagesTwoZeroOneEightPct\% to \ThySharePrimaryProgrammingLanguagesTwoZeroTwoFivePct\%,
computational complexity from \ThySharePrimaryComputationalComplexityTwoZeroOneEightPct\% to
\ThySharePrimaryComputationalComplexityTwoZeroTwoFivePct\% and compilers from
\ThySharePrimaryCompilersTwoZeroOneEightPct\% to \ThySharePrimaryCompilersTwoZeroTwoFivePct\%. The theory and
software categories are growing and shrinking at once: more works, a smaller fraction of a corpus whose growth
is set by the AI categories of Part~V.

\input{tables/tab_theory_counts}

Two cautions attach to these numbers. The post-period growth rate spans two years and is exposed to the
indexing lag of the most recent year (Section~\ref{sec:m-truncation}); the primary-label counts for 2025 are
the last complete ones. And the file \texttt{results/bibliometrics/cagr\_by\_category.csv}, from which
Table~\ref{tab:cagr} is generated, reports primary counts for these categories about three times smaller than
those of the graph counts file (algorithms in 2018: \ThyCagrfileAlgorithmsNTwoZeroOneEight{} against
\ThyCountAlgorithmsTwoZeroOneEightPrimary{}), so it predates the current classification; its growth rates are
not used here, and the discrepancy is recorded for the reproducibility audit.\footnote{The generator
\texttt{bibliometrics/04\_diversity\_cagr.py} reads \texttt{category\_counts\_yearly.csv}; re-running it on the
current counts resolves the discrepancy. Until then, Table~\ref{tab:cagr} and Table~\ref{tab:theory_summary}
disagree for these six rows.}

\subsection{Structural change at the reference date}

The interrupted-time-series slope change at December 2022 is positive for all six primary-label series and
significant with HAC standard errors (Section~\ref{sec:m-its}): \ThyBreakAlgorithmsChatgptSlopePct\% per month
for algorithms, \ThyBreakComputationalComplexityChatgptSlopePct\% for computational complexity,
\ThyBreakProgrammingLanguagesChatgptSlopePct\% for programming languages,
\ThyBreakCompilersChatgptSlopePct\% for compilers, \ThyBreakFormalVerificationChatgptSlopePct\% for formal
verification and \ThyBreakSoftwareEngineeringChatgptSlopePct\% for software engineering. The placebo test
(Section~\ref{sec:m-placebo}) does not confirm any of them at the five per cent level: the share of
baseline-period pseudo-events whose slope statistic exceeds the observed one is
\ThyBreakAlgorithmsPlaceboSlopeP{} for algorithms, \ThyBreakComputationalComplexityPlaceboSlopeP{} for
computational complexity, \ThyBreakSoftwareEngineeringPlaceboSlopeP{} for software engineering,
\ThyBreakCompilersPlaceboSlopeP{} for compilers, \ThyBreakFormalVerificationPlaceboSlopeP{} for formal
verification and \ThyBreakProgrammingLanguagesPlaceboSlopeP{} for programming languages. The two theory
categories are closest to the threshold; none crosses it. A slope change that pseudo-events of the baseline
reproduce at these rates is a feature of series that were already accelerating, not of the reference date.

\input{tables/tab_theory_summary}

The level changes point the other way in five categories. At December 2022 the level fell by
\ThyBreakFormalVerificationChatgptLevelPct\% for formal verification ($p = \ThyBreakFormalVerificationChatgptLevelP$),
\ThyBreakComputationalComplexityChatgptLevelPct\% for computational complexity
($p = \ThyBreakComputationalComplexityChatgptLevelP$), \ThyBreakAlgorithmsChatgptLevelPct\% for algorithms
($p = \ThyBreakAlgorithmsChatgptLevelP$), \ThyBreakProgrammingLanguagesChatgptLevelPct\% for programming
languages and \ThyBreakCompilersChatgptLevelPct\% for compilers (both not significant); only software
engineering shows a positive level change (\ThyBreakSoftwareEngineeringChatgptLevelPct\%,
$p = \ThyBreakSoftwareEngineeringChatgptLevelP$), and it is also the only category with a significant positive
level change at the GPT-4 date (\ThyBreakSoftwareEngineeringGptFourLevel{},
$p = \ThyBreakSoftwareEngineeringGptFourLevelP$; Section~\ref{sec:m-altdates}). The negative level changes
are at least partly the seasonality of proceedings dates in categories dominated by conferences, and the
alternative-date estimates for the o1 date (\ThyBreakComputationalComplexityOOneLevel{} for computational
complexity, $p = \ThyBreakComputationalComplexityOOneLevelP$) show how sensitive a level estimate is to where
the window is cut. The Bai--Perron procedure (Section~\ref{sec:m-bp}) dates a single break at
\ThyBreakAlgorithmsBpBreaksBic{} for algorithms, computational complexity and compilers, two breaks for
programming languages (\ThyBreakProgrammingLanguagesBpBreaksBic{}) and formal verification
(\ThyBreakFormalVerificationBpBreaksBic{}), and one at \ThyBreakSoftwareEngineeringBpBreaksBic{} for software
engineering: the data-driven dates fall in spring 2023 for the three categories with a single break, which is
after the reference date and before the GPT-4 release had been indexed, and they say nothing about cause.

\subsection{Vocabulary moves, citations do not}

Composition is where the window is visible. Table~\ref{tab:theory_llm_cooccurrence} reports, for each
category and year, the number of works that the multi-label classifier also assigns to the LLM category and
their share of the category. Between 2022 and 2025 that share rose from
\ThyCoocSoftwareEngineeringLlmTwoZeroTwoTwoPct\% to \ThyCoocSoftwareEngineeringLlmTwoZeroTwoFivePct\% in
software engineering, from \ThyCoocProgrammingLanguagesLlmTwoZeroTwoTwoPct\% to
\ThyCoocProgrammingLanguagesLlmTwoZeroTwoFivePct\% in programming languages, from
\ThyCoocCompilersLlmTwoZeroTwoTwoPct\% to \ThyCoocCompilersLlmTwoZeroTwoFivePct\% in compilers, from
\ThyCoocFormalVerificationLlmTwoZeroTwoTwoPct\% to \ThyCoocFormalVerificationLlmTwoZeroTwoFivePct\% in formal
verification, and from \ThyCoocAlgorithmsLlmTwoZeroTwoTwoPct\% to \ThyCoocAlgorithmsLlmTwoZeroTwoFivePct\% in
both algorithms and computational complexity. The gradient runs from the code-facing categories to the
mathematical ones, and it is a gradient of vocabulary: co-classification is a lexical and topical signal
(Section~\ref{sec:m-classification}), not a measure of method adoption.

\input{tables/tab_theory_llm_cooccurrence}

Citation flows are more conservative. In the post period, software-engineering works direct
\ThyFlowSoftwareEngineeringToLlmPostPct\% of their categorised references to works of the LLM category,
computational complexity \ThyFlowComputationalComplexityToLlmPostPct\%, compilers
\ThyFlowCompilersToLlmPostPct\%, programming languages \ThyFlowProgrammingLanguagesToLlmPostPct\%, formal
verification \ThyFlowFormalVerificationToLlmPostPct\% and algorithms \ThyFlowAlgorithmsToLlmPostPct\%; the
within-category shares barely moved (algorithms \ThyFlowAlgorithmsToAlgorithmsBaselinePct\% to
\ThyFlowAlgorithmsToAlgorithmsPostPct\%, software engineering
\ThyFlowSoftwareEngineeringToSoftwareEngineeringBaselinePct\% to
\ThyFlowSoftwareEngineeringToSoftwareEngineeringPostPct\%, formal verification
\ThyFlowFormalVerificationToFormalVerificationBaselinePct\% to
\ThyFlowFormalVerificationToFormalVerificationPostPct\%).\footnote{Flows are aggregated from
\texttt{results/graph/category\_flows\_yearly.csv} over citing years 2018--2022 (baseline) and 2023--2026
(post) and are shares of the references that fall inside the categorised corpus (Section~\ref{sec:m-citgraph}).
The LLM category is young, which depresses its share of cited works mechanically; the comparison with the
co-classification shares is therefore indicative, not a test.} Two flow changes deserve notice. The
self-citation share of computational complexity fell from
\ThyFlowComputationalComplexityToComputationalComplexityBaselinePct\% to
\ThyFlowComputationalComplexityToComputationalComplexityPostPct\% while its references to human--computer
interaction rose from \ThyFlowComputationalComplexityToHciBaselinePct\% to
\ThyFlowComputationalComplexityToHciPostPct\%; given the candidate list of
Section~\ref{sec:thy-landmarks}, this is more plausibly the category's contamination by social-science works
than a change in theoretical research, and it is recorded as a contested reading. Inbound citations to formal
verification from computer vision doubled, from \ThyInflowFormalVerificationFromComputerVisionBaselinePct\% to
\ThyInflowFormalVerificationFromComputerVisionPostPct\% of the category's inbound references, which is
consistent with the neural-network verification literature reviewed in Section~\ref{sec:thy-fv} being cited by
robustness work; no paper-level breakdown tests this.

\section{Algorithms and data structures}
\label{sec:thy-algorithms}

\subsection{What the window established}

The category's largest results are not in the candidate list, and the first task of the review is to say what
they are, from verified records. Maximum flow and minimum-cost flow were brought to almost-linear time
\citep{chen2022maxflow}, closing a line of work that had run through interior-point methods and dynamic graph
data structures for a decade. Single-source shortest paths with negative weights were brought to near-linear
time by a combinatorial algorithm \citep{bernstein2022negative}, a result republished in the \emph{Journal of
the ACM} and \emph{Communications of the ACM} in 2025. The sorting barrier for directed single-source shortest
paths, the $\Omega(m + n \log n)$ cost that Dijkstra's algorithm with a priority queue cannot avoid, was
broken by a deterministic $O(m \log^{2/3} n)$ algorithm \citep{duan2025sorting}, the best paper of STOC~2025.
In data structures, the open-addressing bounds conjectured by Yao in 1985 were shown to be beatable: without
reordering, a greedy scheme achieves expected amortised probe complexity $O(\log^2 \delta^{-1})$ at load
$1 - \delta$, against the conjectured $\Theta(\delta^{-1})$ \citep{farachcolton2024openaddressing}. These
four results, from 2022 to 2025, are what a specialist would list first for the window; none has the citation
profile that the ranking rewards, because theoretical results are cited by a small community over long
horizons, and the 36-month window and the field normalisation are both calibrated on the behaviour of
applied categories.

What the corpus does record is the programme of \emph{algorithms with predictions}, which the baseline period
established and the window continued. The candidate list carries it through a 2024 arXiv re-posting of the 2018
conference paper on ski rental and non-clairvoyant scheduling with machine-learned predictions, whose
abstract describes algorithms that are ``oblivious to the performance of the predictor, improve with better
predictions, but do not degrade much if the predictions are poor''; the programme's canonical references are
the journal version of competitive caching with learned advice \citep{lykouris2021caching} and the overview in
\emph{Communications of the ACM} \citep{mitzenmacher2022predictions}. The formal object is a pair of
guarantees, consistency (the competitive ratio when the prediction is exact) and robustness (the ratio under
arbitrary error), with a trade-off between them; it is the point at which online algorithms and machine
learning meet without either giving up its guarantees, and it is the one place in the category where the
``learning'' vocabulary of the window names a theory rather than a tool. The fine-grained complexity programme
that organised algorithms research at the baseline (Section~\ref{sec:p2-theory}) is represented in the
bibliography by the ICM survey \citep{vassilevskawilliams2019finegrained} and by the parameterized-algorithms
monograph \citep{cygan2015parameterized}.

\subsection{What the candidate list contains}

Of the \ThyAuditAlgorithmsN{} algorithms candidates, \ThyAuditAlgorithmsInScopeResearch{} are research
contributions and none is misclassified; the rest are textbook chapters, re-deposited classics, theses and
metaheuristics. The two post-period research candidates are modest and both carry citation counts that belong
to other works: the WADS~2025 paper extends Kd-trees to Bregman divergences, shows that the triangle inequality
is not needed for correct pruning, and reports two orders of magnitude over linear search for
Kullback--Leibler nearest-neighbour queries in up to a hundred dimensions \citep{pham2025kdtree}; the SEA~2024
paper replaces the highest-degree branching rule of branch-and-reduce for maximum independent set with a graph
neural network \citep{langedal2024mis}. Both abstracts describe engineering contributions with experimental
evaluation, which is what algorithm engineering is; neither is the kind of result that defines the window.

The other research genre in the list is the metaphor-based metaheuristic: the Arithmetic Optimization Algorithm
\citep{abualigah2021aoa} and the Aquila Optimizer \citep{abualigah2021aquila} in 2021, and the artificial
lemming, glider snake, gray langur and starfish optimisers in 2025--2026, published in engineering and
AI-review journals and evaluated on CEC benchmark functions and constrained design problems. The abstracts share
a template, a natural metaphor mathematically modelled into exploration and exploitation phases and
``outperforming or matching'' a dozen earlier metaheuristics. The operational-research literature has argued
since \citet{sorensen2013metaphor} that the genre re-describes existing methods under new names and that its
benchmarks do not discriminate; the position was restated in a ``call for action'' \citep{aranha2021metaphor}
and substantiated for six widely cited algorithms, shown to be equivalent to or special cases of earlier
methods \citep{camachovillalon2022exposing}. The corpus does not adjudicate this dispute; what it shows is
the genre's weight in the highly cited stratum of the algorithms category, where six of twenty-five candidates
belong to it and where the post-2022 research articles with the highest normalised scores are of this kind.
Whether the genre grows faster than the rest of the category and absorbs a growing share of its citations is an
open problem of Part~X (G-P7), answerable with a keyword-defined subseries.

\subsection{Algorithms discovered by learning systems}

Three Nature papers and one preprint report algorithms found by reinforcement learning or program search:
faster matrix-multiplication tensor decompositions for small sizes \citep{fawzi2022alphatensor}, shorter
sorting networks for short sequences, merged into a standard library \citep{mankowitz2023alphadev}, new
constructions for the cap-set problem and bin packing from evolved programs \citep{romeraparedes2024funsearch},
and, as a 2025 preprint, a coding agent that reports improvements on a collection of open mathematical and
algorithmic problems \citep{novikov2025alphaevolve}. All four are reports by the developers; the improvements
are on specific instances; and no independent reproduction or extension by the theory community appears in the
verified bibliography. The question these works pose to the category, whether search over programs changes how
algorithms are designed or only how constants are tuned, is one the corpus cannot answer at this granularity;
it is stated as open problem G-P9. The honest position is that the window's algorithmic breakthroughs were
obtained by people, and that the learned-discovery results are promising, contested in scope, and awaiting
replication.

\section{Computational complexity}
\label{sec:thy-complexity}

The category's statistics are the least trustworthy of the six: \ThyAuditComputationalComplexityMisclassified{}
of its \ThyAuditComputationalComplexityN{} candidates are outside computing, and the flow and co-occurrence
changes of Section~\ref{sec:thy-statistics} are to that extent artefacts. The two in-scope research candidates
are a STOC~2019 paper and a 2026 \emph{Theoretical Computer Science} article on SAT in spiking neural P systems
(no abstract). The STOC paper is a genuine landmark of the baseline: its abstract describes the reachability
problem for Petri nets as open since the 1960s, with Lipton's 1976 exponential-space lower bound unimproved, and
establishes a non-elementary lower bound \citep{czerwinski2019petri}. The story was completed within the
baseline period, when reachability in vector addition systems was shown Ackermann-complete
\citep{czerwinski2021ackermann,leroux2021notprimitive}, matching the upper bound of Leroux and Schmitz; the
window inherits a closed problem whose closure the corpus ranks below a technology-acceptance survey.

The window's own contribution to complexity theory that a specialist would name first is the simulation of
time $t$ in space $O(\sqrt{t \log t})$ \citep{williams2025sqrtspace}, which improves the Hopcroft--Paul--Valiant
simulation of 1975 after fifty years and implies, through a known argument, that there are problems solvable
in linear space that need nearly quadratic time on multitape machines; the paper is a STOC~2025 result
republished in the \emph{Journal of the ACM} in 2026. In additive combinatorics, the strong bounds for
three-term arithmetic progressions \citep{kelley2023threeap} brought the Roth-type exponent to a form conjectured
since Behrend. Neither appears in the candidate list; both enter through verified records, and the general
point is the one made for algorithms: results of this kind are cited slowly and by few, and a 36-month
field-normalised window does not see them.

The boundary with language models is where the category's co-classification share grew, yet the relevant
works are mostly classified elsewhere. The proof that transformers with logarithmic precision lie in uniform
$\mathrm{TC}^0$ \citep{merrill2023parallelism}, and the survey of what formal languages transformers can
express \citep{strobl2024survey}, bound what a single forward pass can compute and make the case that
chain-of-thought computation is where additional expressive power must come from; they are, in the verified
bibliography, the window's main contribution of complexity theory to the study of the models that dominate
Part~V. Whether such works are classified under computational complexity or under natural language processing
is an empirical question about the taxonomy (open problem G-P8). The remainder of the candidate list is
teaching material, including the fourth edition of the Kolmogorov-complexity monograph \citep{li2019kolmogorov}
and undergraduate chapters on complexity and on parameterized complexity, and re-deposited classics, including
Turing's 1936 paper and Wolfram's cellular-automata chapters.

\section{Programming languages}
\label{sec:thy-pl}

The baseline lineage was set out in Section~\ref{sec:p2-pl}: Rust and its semantic foundation
\citep{matsakis2014rust,jung2017rustbelt,jung2021saferust}, Lean~4 as a prover that is also a programming
language \citep{demoura2021lean4} with its mathematical library \citep{mathlib2020}, and the verified
artefacts CompCert \citep{leroy2009compcert} and seL4 \citep{klein2009sel4} that showed production software
can be proved correct. The candidate list records this lineage only obliquely, through three theses of the
L4/seL4 school re-deposited in 2022 (separation logic for programs in virtual memory, formal memory models for
C systems code, a verified multiprocessor kernel design), which the ranking places in the post period. In the
window the lineage continued with Verus \citep{lattuada2024verus}, a verification framework for Rust programs
presented at SOSP~2024, which treats the ownership discipline of the language as the foundation for
specification and proof rather than as an obstacle to them; the content of Verus is known here from its verified
title and venue only.

Of the \ThyAuditProgrammingLanguagesN{} candidates, \ThyAuditProgrammingLanguagesInScopeResearch{} are
research contributions. Two of them mark the entry of language models into the community's top venue in
2024. LLift \citep{li2024llift} combines static analysis with an LLM to find use-before-initialisation bugs in
the Linux kernel; its abstract reports post-constraint guidance of the path analysis, procedures for handling
``the unpredictable nature of LLMs'', and four previously unknown bugs acknowledged by the kernel community.
WhiteFox \citep{yang2024whitefox} is described by its abstract as the first white-box compiler fuzzer that uses
an LLM reading the source code of optimisations to generate test programs that exercise them, against
black- and grey-box fuzzing that lacks that information and symbolic execution that does not scale to a
compiler. Both papers report bugs found; neither reports a guarantee, and the abstracts do not claim one. The
natural comparison is with the two instruments that the compiler community built for correctness before the
window, Csmith's random differential testing, which found hundreds of bugs in production C compilers
\citep{yang2011csmith}, and Alive2's bounded translation validation of LLVM optimisations
\citep{lopes2021alive2}; whether LLM-generated tests can be combined with validation of that kind, so that the
share of reported bugs that are confirmed can be measured per optimisation pass, is open problem G-P4. The
third research candidate, ZEUS \citep{kalra2018zeus}, is the baseline representative of program analysis for a
new target: abstract interpretation and constrained Horn clauses applied to smart contracts, with an abstract
reporting that about 95\% of 22,400 contracts analysed were vulnerable. The universal fuzzer of
\citet{xia2024fuzz4all} and the LLM-based bug-reproduction study of \citet{kang2023fewshottesters} are the
software-engineering counterparts of the same move.

The category's vocabulary moved more than any except software engineering's: co-classification with the LLM
category reached \ThyCoocProgrammingLanguagesLlmTwoZeroTwoFivePct\% in 2025. Its references to LLM works are
\ThyFlowProgrammingLanguagesToLlmPostPct\%, and its structural ties are unchanged, with
\ThyFlowProgrammingLanguagesToFormalVerificationPostPct\% of its references going to formal verification and
\ThyFlowProgrammingLanguagesToSoftwareEngineeringPostPct\% to software engineering in the post period, against
\ThyFlowProgrammingLanguagesToFormalVerificationBaselinePct\% and
\ThyFlowProgrammingLanguagesToSoftwareEngineeringBaselinePct\% at the baseline. Programming languages is, in
the citation graph, the hinge between verification and engineering, and the window did not move the hinge.

\section{Compilers}
\label{sec:thy-compilers}

Compilers is the smallest of the six categories, \ThySharePrimaryCompilersTwoZeroTwoFivePct\% of primary labels
in 2025, and the most lexically contaminated after complexity. Its in-scope candidates nevertheless trace a
coherent line. At the baseline, MLIR \citep{lattner2021mlir} is the infrastructure whose abstract promises to
reduce ``the cost of building domain specific compilers'' and to connect existing ones; Tiramisu
\citep{baghdadi2019tiramisu} is a polyhedral compiler whose scheduling language separates algorithm, loop
transformation, data layout and communication so that one algorithm can target multicores, GPUs and
distributed machines; ExaStencils is a four-layer domain-specific language for multigrid solvers. Two surveys
establish that learned compiler heuristics are a programme older than the window: the \emph{Proceedings of the
IEEE} survey of machine learning in compiler optimisation \citep{wang2018mlcompiler} and the \emph{Computing
Surveys} review of autotuning, optimisation selection and phase ordering \citep{ashouri2018autotuning}, which
dates the first attempts to the mid-1990s. Three MIT and Delaware theses on learned optimisation selection and
on sparse tensor-algebra compilation complete the baseline picture.

The post-period candidates show the programme's change of scale. LLM4VV \citep{munley2024llm4vv} uses language
models to generate a validation test suite for directive-based parallel programming compilers (metadata only;
no abstract). LLM Compiler \citep{cummins2025llmcompiler} is a suite of foundation models built on Code Llama
and trained, per its abstract, on 546 billion tokens of LLVM intermediate representation and assembly, then
instruction-tuned to predict and emulate compiler behaviour; fine-tuned versions reach 77\% of the optimising
potential of an autotuning search for code size and disassemble x86-64 and ARM assembly back to LLVM-IR. The
preprint that preceded it \citep{cummins2023llmcompiler} framed the task as predicting optimisation-pass
sequences. The shift is from learning a heuristic inside a compiler, with features chosen by compiler writers,
to pre-training a model on the compiler's own artefacts; what the shift leaves open is the question that
compiler research has always had to answer last, correctness, which the field handled through differential
testing \citep{yang2011csmith} and translation validation \citep{lopes2021alive2} rather than through model
evaluation. Co-classification with the LLM category reached \ThyCoocCompilersLlmTwoZeroTwoFivePct\% in 2025;
references to LLM works are \ThyFlowCompilersToLlmPostPct\%, and the category's citations continue to go
first to computer architecture (\ThyFlowCompilersToComputerArchitecturePostPct\% of references in the post
period) and to itself. The deep-learning compiler stack recorded in the main bibliography, TVM, Triton and
PyTorch~2 \citep{chen2018tvm,tillet2019triton,ansel2024pytorch2}, and the image-processing DSL that preceded
it \citep{ragankelley2013halide}, belong to Part~VI and are only noted here as the other post-2018 development
of the category.

\section{Formal verification}
\label{sec:thy-fv}

Formal verification has the most in-scope research candidates of the six
(\ThyAuditFormalVerificationInScopeResearch{} of \ThyAuditFormalVerificationN{}) and the clearest internal
structure, which the review follows: solvers and competitions, neural-network verification, verification of new
targets, learned theorem proving, and the theory of verification.

\paragraph{Solvers and competitions.}
cvc5 \citep{barbosa2022cvc5} is the system description of the SMT solver that succeeded CVC4, evaluated on all
SMT-LIB benchmarks against CVC4 and Z3; the Handbook of Satisfiability in its second edition
\citep{biere2021handbook} is the reference work, present twice in the candidate list under two records. The
SV-COMP~2024 report \citep{beyer2024svcomp} describes the largest edition of the software-verification
competition to that date, 76 tools from 34 teams on 30,300 verification tasks for C programs, with a second
track for witness validation and a new witness format. Competitions of this kind are the category's benchmark
culture, and they are a point of contrast with the benchmark culture of Part~V: the tasks are fixed programs
with fixed specifications, a tool's result is a proof or a counterexample that a validator checks, and the
score is not self-reported.

\paragraph{Neural-network verification.}
The baseline built a sub-field: Reluplex \citep{katz2017reluplex} extended the simplex method to ReLU
constraints; the 2018 symbolic-interval preprint in the candidate list argued, per its abstract, that existing
analyses ``struggle to scale beyond very small networks'' and proposed interval propagation that does;
DeepPoly \citep{singh2019deeppoly} introduced an abstract domain of floating-point polyhedra with intervals and
transformers for ReLU, sigmoid, tanh and maxpool, and reported the first proofs of robustness to rotations
with interpolation; Marabou \citep{katz2019marabou} packaged SMT-based verification as a framework accepting
TensorFlow models. The VNN-COMP report \citep{brix2023vnncomp} summarises the first three years of the
competition that organised the sub-field. The doubling of formal verification's inbound citations from
computer vision in the post period (Section~\ref{sec:thy-statistics}) is consistent with this literature being
cited by robustness work, and the sub-field is the main channel through which the category meets the
machine-learning categories; whether it has guarantees that survive the scale of the models of Part~V is not a
question these abstracts address.

\paragraph{New targets.}
VerX \citep{permenev2020verx} is described by its abstract as the first automated verifier of functional
properties of Ethereum smart contracts, combining reduction of temporal properties to reachability, a symbolic
execution engine for the Ethereum virtual machine, and delayed predicate abstraction, evaluated on 83
properties of 12 projects. The answer-set-programming monitor for automated driving \citep{klampfl2024asp}
and the theses on parametric and multi-objective Markov models represent runtime and probabilistic
verification; the Warwick thesis on model checking quantum protocols, re-deposited with a 2026 date, is a
baseline work of the previous decade.

\paragraph{Learned theorem proving.}
The abstract attached in the corpus to the ITP~2023 paper, under a wrong title (Section~\ref{sec:thy-landmarks}),
is the clearest statement in the candidate set of what machine learning has done for automated reasoning:
MizAR \citep{jakubuv2023mizar} proves about 60\% of the theorems of the Mizar Mathematical Library in the hammer
setting and 75\% when given the premises of the human proofs, through the E and Vampire provers with the ENIGMA
and Deepire learned guidance and an incremental loop that grows a corpus of millions of proofs while training
stronger systems on it. This is the saturation-prover line. The language-model line is represented by Baldur
\citep{first2023baldur}, which generates and repairs whole Isabelle proofs; by LeanDojo
\citep{yang2023leandojo} and DeepSeek-Prover \citep{xin2024deepseekprover}, both preprints, which report
retrieval-augmented and synthetic-data-trained provers on Lean benchmarks; and by the position paper on formal
mathematical reasoning as a frontier \citep{yang2024formalmath}, also a preprint. The figures these works
report are on different benchmarks, under different compute budgets, with the possibility of overlap between
training corpora and test theorems that the abstracts do not exclude; a benchmark of theorems posted after the
training cut-off, with proof checking rather than self-reported success, is the direction stated as open
problem G-P5. The machine-learned mathematics of Part~V, olympiad geometry \citep{trinh2024alphageometry} and
program search \citep{romeraparedes2024funsearch}, is adjacent but distinct: it produces objects that a human or
a checker then verifies, where the works above produce the proofs.

\paragraph{Theory of verification.}
Equality saturation as implemented in \emph{egg} \citep{willsey2021egg}, whose abstract describes e-graph
rewriting that ``only adds information'' and extraction by a user-supplied cost function, is a baseline result
republished as a research highlight in 2026; the quantitative interface automata of the CSL~2026 paper on reward
interfaces, whose abstract introduces multi-valued correctness requirements and best-effort satisfaction into
interface theories, is the one post-period research candidate of this kind.

The category's primary share halved between 2018 and 2025 while its multi-label count grew by eleven per cent
(Table~\ref{tab:theory_counts}). The arithmetic of the argmax assignment (Section~\ref{sec:m-score}) suggests
why: a work that carries a verification label and an AI or security label loses the primary label to the
larger category when the scores are close, so the primary series understates a category whose work is
increasingly done in combination. Measuring the share of works whose primary label switched, by co-assigned
category and year, is open problem G-P10.

\section{Software engineering}
\label{sec:thy-se}

Software engineering is where the window's change is largest, best documented, and most contested. Its
baseline was not AI-free (Section~\ref{sec:p2-pl}): the Codex models \citep{chen2021codex}, the
code-generation benchmarks \citep{austin2021mbpp}, the systematic evaluation of code models
\citep{xu2022codelms} and the first productivity assessment of neural code completion
\citep{ziegler2022copilot} precede the reference date, and the survey of machine-learning testing
\citep{zhang2022mltesting}, 144 papers on testing properties, components and workflows of learned systems,
shows the category already organised around learned software as an object of test. The window's surveys
reverse the direction of the relation. The survey of software testing with large language models
\citep{wang2024llmtesting} analyses 102 studies and reports, per its abstract, that test-case preparation and
program repair are the most common uses; the two systematic reviews of language models for software
engineering \citep{fan2023llm4se,hou2024llm4se} and the code-generation survey \citep{jiang2024codegensurvey}
map the same territory. Method papers from the main bibliography and the Part~VII-a bibliography give the
texture: program repair in the era of pre-trained models \citep{xia2023apr}, bug reproduction from reports
\citep{kang2023fewshottesters}, universal fuzzing \citep{xia2024fuzz4all}, and the agentic setting defined by
SWE-bench \citep{jimenez2024swebench} and SWE-agent \citep{yang2024sweagent}, both preprints, in which a model
is asked to resolve a GitHub issue end to end. Among the candidates, APISS \citep{chen2025apiss} retrieves
functionality-equivalent APIs through LLM embeddings to migrate proof-of-concept exploits, and a 2026 paper
proposes a multi-scale temporal model for just-in-time defect prediction; both are method contributions judged
from their abstracts.

\paragraph{Productivity: two findings that need reconciling.}
The most cited post-period empirical candidate reports three randomised field experiments at Microsoft,
Accenture and an unnamed Fortune~100 company, run by the firms in the course of business, in which a random
subset of 4,867 developers received an AI coding assistant; the pooled estimate is a 26.08\% increase in
completed tasks with a standard error of 10.3\%, each experiment being ``noisy'' on its own, and less
experienced developers adopting more and gaining more \citep{cui2026genaiwork}. The earlier controlled
experiment on a single task reported a larger speed-up \citep{peng2023copilot}, and the field studies of
generative AI at work outside software \citep{brynjolfsson2023genaiwork,noy2023productivity,dellacqua2023jagged}
report the same pattern of larger gains for less experienced workers. Against these stands a 2025 randomised
trial preprint in which experienced open-source developers working on repositories they maintain took longer
to complete issues with AI tools than without \citep{becker2025metr}. The two findings are not contradictory
once population and outcome are distinguished: enterprise developers completing assigned tasks versus expert
maintainers resolving issues in mature codebases they know well, and tasks completed versus time per issue.
But the reconciliation is a reading of two abstracts, the second of a preprint, and the design that would
settle it, a preregistered multi-site trial stratified by experience and repository maturity with time-to-merge
and defect rate as joint outcomes, has not been run (open problem G-P3). The user studies of how programmers
interact with code-generating models \citep{barke2023groundedcopilot,vaithilingam2022expectation,liang2024usability}
supply the mechanism, acceleration mode against exploration mode, that any such trial would need to measure.

\paragraph{Security of generated code.}
The security evaluations agree with one another. Copilot's suggestions were found vulnerable at a substantial
rate in 2022 \citep{pearce2022asleep}; the CCS~2023 user study found that participants with an AI assistant
wrote less secure code and believed it more secure \citep{perry2023insecure}; and the ICPEC~2025 study in the
candidate list, evaluating three open models on a filtered Big-Vul subset with eight CWE categories, reports
``a sharp contrast between high detection rates and markedly poor classification accuracy''
\citep{gasparlopes2025vuln}. High detection or completion paired with poor fine-grained security reasoning is
the consistent pattern across three designs, and it is the category's clearest negative result about the
models.

\paragraph{The statistics.}
Software engineering has the highest co-classification with the LLM category of the six
(\ThyCoocSoftwareEngineeringLlmTwoZeroTwoFivePct\% of its works in 2025, from
\ThyCoocSoftwareEngineeringLlmTwoZeroTwoTwoPct\% in 2022), the largest post-period growth
(\ThyCagrMultilabelSoftwareEngineeringPostPct\% per year), the only positive level change at the reference
date and the only significant positive level change at the GPT-4 date (Section~\ref{sec:thy-statistics}).
Its references to LLM works are \ThyFlowSoftwareEngineeringToLlmPostPct\% in the post period, from
\ThyFlowSoftwareEngineeringToLlmBaselinePct\%, and inbound citations from the LLM category are
\ThyInflowSoftwareEngineeringFromLlmPostPct\% of its inbound references. Whether a vocabulary shift of this
size is a method shift, that is, whether the works co-classified with LLM cite LLM method papers at a higher
rate than the category's baseline, can be tested on the knowledge graph of Part~III once method nodes are
extracted for the high-priority set; it is open problem G-P2. The research-software case of the Astropy
project \citep[in the candidate list;][]{collberg2016repeatability} and the reproducibility literature of
Part~IX are the other side of the same category, and the only part of it where the window changed nothing
visible.

\section{Synthesis}
\label{sec:thy-synthesis}

Three conclusions follow, in decreasing order of evidential strength.

The first is about the instrument. In the theory and software areas the automatically selected landmark
candidates do not identify landmarks: \ThyAuditVerdictInScopeResearch{} of \ThyAuditN{} are in-scope research
works, \ThyAuditIdCollision{} carry citation windows that belong to other works, and the rest are chapters with
generic titles, re-deposited classics, theses in small normalisation cells and lexical misclassifications. The
defects are identifiable and partly correctable at the selection stage, and the audit table
(Table~\ref{tab:theory_landmark_audit}) should accompany any use of the list; the major theoretical results of
the window, almost-linear flow, near-linear negative-weight shortest paths, the directed sorting barrier,
optimal open addressing, square-root-space simulation and the 3-progression bounds, are invisible to a
36-month field-normalised ranking and were brought into this review through verified records. The same
blindness will affect any bibliometric answer to RQ3 and RQ7 for these categories.

The second is about the statistics. The six categories grew in absolute terms and declined in relative terms
after 2022; their slope changes at the reference date are positive but not distinguishable from pseudo-events
in the baseline; their vocabulary moved toward language models in proportion to their distance from
mathematics; and their citation behaviour moved little. For RQ2 the answer is that none of the six is among
the categories with structural change that survives the placebo test, and for RQ5 that the relationship with
the foundation-model categories changed in what these works say far more than in what they cite.

The third is about the research. The substantive developments of the window are of two kinds that the corpus
treats very differently. Theoretical results were obtained by people, at the rate and in the venues of the
previous decade, and are cited accordingly. The entry of language models into verification, program analysis,
compiler testing and software engineering is visible in the co-classification statistics and in the abstracts
of the in-scope candidates, and it is where the open problems lie: guarantees for learned program analysis and
compiler testing (G-P4), comparability of learned provers (G-P5), the productivity effect on experienced
developers (G-P3), and the distinction between a vocabulary and a method (G-P2). What this half of Part~VII
can say with confidence is which of these questions the corpus can answer with its present instruments, and
which it cannot.