spb/wp44_uqo

1% part07a_theory.tex — Part VII (theory half): algorithms and data structures, computational complexity, programming2% languages, compilers, formal verification, software engineering. Agent G (Theory Specialist), 2026-11-03.3% The director merges this file with part07b_security.tex into Part VII. Every corpus number is a macro of4% tables/numbers.tex (prefix \Thy..., appended by tables/make_numbers.py, Agent G block) or appears in a generated table5% (tables/make_tables.py, tables_part07a). Sources: results/graph/category_counts_yearly.csv, category_flows_yearly.csv,6% category_cooccurrence_yearly.csv; results/econometrics/breaks.csv; literature_synthesis/landmarks/{theory,software_pl}_*;7% literature_synthesis/agent_G/{claims,contributions,open_problems}.csv and review.md. Bibliography: references.bib and8% references_part07a.bib (65 entries, each resolved by one live lookup; references_verification_part07a.csv).910\section{Scope, evidence and reading rules for the theory half}11\label{sec:thy-scope}1213This half of Part~VII reviews six categories of the taxonomy: algorithms and data structures, computational14complexity, programming languages, compilers, formal verification and software engineering (the areas15\emph{theory} and \emph{software\_pl} of the ontology, Section~\ref{sec:p2-ontology}). It has two objects. The16first is the research itself: what the baseline period established in these categories, what the window added,17and where the additions are contested. The second is the instrument: the corpus statistics for the six18categories and, above all, the automatically selected landmark candidates, which in these areas turn out to19measure the bibliographic record more than the research it records. The two objects cannot be separated,20because the landmark list is the protocol's channel from corpus to synthesis, and in the theory and software21areas that channel is obstructed in ways that are themselves findings.2223Three reading rules apply. First, no full text was read. Every statement about a work rests on its metadata24(title, venue, type, year, identifiers) or on the abstract recorded in OpenAlex, and the text says which; where25an abstract is the source, the phrase ``the abstract reports'' is used deliberately. Second, works available26only as arXiv postings are preprints and are described as such, whatever their later fate. Third, the27structural-change statistics are read as the protocol prescribes (Section~\ref{sec:m-structural}): the November282022 boundary is a reference date, the placebo distribution is the test, and nothing below attributes a change29to any single event. The categories are small relative to the AI categories of Part~V (their combined primary30share in 2025 is under ten per cent of the corpus), so the statistics are those of minorities inside a31corpus whose growth is set elsewhere.3233The section proceeds from the instrument to the field. Section~\ref{sec:thy-landmarks} audits the landmark34candidates; Section~\ref{sec:thy-statistics} reports the six categories' volume, structural-change and35composition statistics; Sections~\ref{sec:thy-algorithms} to~\ref{sec:thy-se} review the categories; and36Section~\ref{sec:thy-synthesis} draws the conclusions that Part~X and Part~XI inherit.3738\section{The landmark candidates: an audit}39\label{sec:thy-landmarks}4041The protocol selects landmarks as the works with the highest field-normalised 36-month citation score42(NCS36, Section~\ref{sec:m-citations}) within each primary category, with a floor of fifteen per category, plus43the 200 most cited works overall; for 2025--2026 works the 12-month window replaces the 36-month one44(Section~\ref{sec:data-core}). The theory area contributed \ThyLandTheoryN{} candidates and the software area45\ThyLandSoftwarePlN{}, twenty-five per category, of the \SelectionLandmarks{} landmarks of the whole corpus.46Before any of the \ThyAuditN{} can be called a landmark, the list has to be audited, and the audit is the first47result of this section (Table~\ref{tab:theory_landmark_audit}). Each candidate received one of eight verdicts48from its metadata and, where available, its abstract: an in-scope research contribution49(\ThyAuditVerdictInScopeResearch{} candidates), an in-scope survey or report (\ThyAuditVerdictInScopeSurvey{}),50a misclassified work outside the category and outside the theory and software scope51(\ThyAuditVerdictMisclassified{}), a thesis (\ThyAuditVerdictDissertation{}), a classic re-deposited under a52recent record date (\ThyAuditVerdictReprintMisdated{}), a textbook or chapter (\ThyAuditVerdictTextbook{}), a53metaphor-based metaheuristic (\ThyAuditVerdictMetaheuristic{}) or a duplicate record54(\ThyAuditVerdictDuplicate{}). Fewer than one candidate in five is a research contribution inside its55category, and only \ThyAuditInScopeResearchPost{} of those are post-period works. Four mechanisms account56for the rest.5758\input{tables/tab_theory_landmark_audit}5960\paragraph{Identifier collisions.}61\ThyAuditIdCollision{} candidates carry OpenAlex identifiers that, resolved against the live database on623~November 2026, return a different work. The record titled ``Exploiting Generative AI to Scale up Intelligent63Tutoring Systems'', with the DOI of an ITP~2023 paper, resolves to \emph{Attention Is All You Need}; the abstract64stored for it in the corpus is that of \emph{MizAR~60 for Mizar~50}, which is what the DOI denotes65\citep{jakubuv2023mizar}; its 36-month citation count in the corpus is that of the Transformer paper, which is66why it ranks first in the whole software area. The ECOOP~2025 paper on functionality-specific67vulnerabilities \citep{chen2025apiss} resolves to the graph-convolutional-network preprint; the SEA~202468paper on learned branching for maximum independent set \citep{langedal2024mis} to GraphSAGE; the WADS~202569Kd-tree paper \citep{pham2025kdtree} to the variational-autoencoder preprint; the SAIA~2024 robustness70framework \citep{awadid2025robust} to the adversarial-training preprint of Madry and co-authors; an71ESEM~2026 record \citep{naqvi2026bigger} to the Codex paper; and a DX~2024 answer-set-programming paper72\citep{klampfl2024asp} to an unrelated preprint. In every case the recorded citation window matches the other73work's count.\footnote{Raw responses in \texttt{literature\_synthesis/agent\_G/verification\_lookups\_raw.txt}.74The mechanism (identifier merging or reuse between the snapshot of 14~October 2026 and the live database) is75inferred; the consequence, that the citation windows of these records belong to other works, is observed.} The76four top-ranked candidates of the software area and the top-ranked candidate of the theory area owe their rank77to citations that are not theirs. The same check should be run on the other areas' lists before Part~IX uses78them.7980\paragraph{Generic-title chapters.}81Chapters titled ``Introduction to Algorithms'' (2020, 2021, 2023), ``Particle Swarm Optimization'' (2019),82``Introduction to Software Testing'' (2021), ``Introduction to Graph Theory'' (2023), and Royce's 1970 paper on83managing large software developments reprinted in a 2021 anthology, carry hundreds to thousands of citations in84their windows, and live lookups confirm the counts. The plausible reading, offered as an interpretation, is85that citations intended for the canonical work are attributed to a same-titled chapter by the indexer's86reference matching. Whatever the mechanism, a chapter of a 2023 undergraduate textbook is not a landmark of872023 research.8889\paragraph{Re-deposited classics.}90\ThyAuditVerdictReprintMisdated{} records are works whose record date is the date of a deposit, reprint or91re-posting rather than of the work. Dijkstra's 1959 note on two problems in connexion with graphs appears as a922022 ACM Books chapter; Turing's 1936 paper as a 2021 MIT Press chapter; the 1994 survey of decidability for93Petri nets as a 2024 arXiv posting; Lynch and Tuttle's introduction to input/output automata as a 2026 journal94article \citep{lynch2026ioautomata}; the \emph{egg} equality-saturation paper \citep{willsey2021egg} as a 202695research highlight \citep{willsey2026eggcacm}; doctoral theses of the early 2000s as 2026 repository records;96three theses of the L4/seL4 verification school as 2022 records; and the 2018 conference paper on online97algorithms with machine-learned predictions as a 2024 arXiv posting. Because the year field is the deposit year,98these records enter the post period: \ThyLandTheoryDatedTwentysix{} of the \ThyLandTheoryN{} theory candidates99and \ThyLandSoftwarePlDatedTwentysix{} of the \ThyLandSoftwarePlN{} software candidates are dated 2026, a year100of which the corpus holds ten months.101102\paragraph{Lexical misclassification and small cells.}103\ThyAuditVerdictMisclassified{} candidates are outside the theory and software scope altogether. The104computational-complexity list contains \ThyAuditComputationalComplexityMisclassified{} such works of its105\ThyAuditComputationalComplexityN{}: technology-acceptance models of mobile learning, PLS-SEM studies of106small enterprises and of students' well-being, a Routledge volume on complexity theory in the social sciences,107a review of fringe-projection profilometry, captured by the word ``complexity''. The compilers list contains108\ThyAuditCompilersMisclassified{}, captured by ``just-in-time'' (adaptive interventions in mental health),109``compiling'' (a guide to literature reviews) and ``polyhedral'' (power-system dispatch). The110programming-languages list includes a Nature paper on Calabi--Yau manifolds in black-hole scattering. The111classifier's per-category precision, estimated on the validation sample (Section~\ref{sec:m-validation}), is112the right place to quantify this; what the landmark list shows is the interaction between imprecision and113normalisation. NCS36 divides a work's citations by the expectation for its category, year and type114(Section~\ref{sec:m-citations}); cells of theses or of non-computing articles are small and lightly cited, so a115thesis with a handful of citations, or a social-science article with a hundred, obtains a normalised score that116no STOC paper of the same year can match. \ThyAuditVerdictDissertation{} of the \ThyAuditN{} candidates are117theses.118119What survives is a set of \ThyAuditVerdictInScopeResearch{} research works and \ThyAuditVerdictInScopeSurvey{}120surveys or reports, listed in Table~\ref{tab:theory_landmarks_discussed}. They are reviewed below with the121pre-2022 lineage of Part~II and with the window's results that the ranking does not see: the major theoretical122results of 2022--2025 are absent from the candidate list and enter this review through verified bibliographic123records, not through the corpus ranking. Open problem~G-P1 of Part~X states the correction: type filters,124live re-resolution of identifiers and venue priors at the selection stage, evaluated against a125specialist-labelled sample.126127\input{tables/tab_theory_landmarks_discussed}128129\section{Volume, structural change and composition}130\label{sec:thy-statistics}131132\subsection{Growth in absolute terms, decline in relative terms}133134Tables~\ref{tab:theory_counts} and~\ref{tab:theory_counts_primary} give the yearly counts of works carrying each category135(multi-label) and of works whose primary category it is; Table~\ref{tab:theory_summary} summarises growth and136Table~\ref{tab:theory_breaks} the structural-change estimates.137The multi-label counts grew in every category after 2022. Between 2023 and 2025 the compound annual growth was138\ThyCagrMultilabelSoftwareEngineeringPostPct\% for software engineering,139\ThyCagrMultilabelComputationalComplexityPostPct\% for computational complexity,140\ThyCagrMultilabelCompilersPostPct\% for compilers, \ThyCagrMultilabelAlgorithmsPostPct\% for algorithms,141\ThyCagrMultilabelFormalVerificationPostPct\% for formal verification and142\ThyCagrMultilabelProgrammingLanguagesPostPct\% for programming languages, against143\ThyCagrMultilabelSoftwareEngineeringBaselinePct\%, \ThyCagrMultilabelComputationalComplexityBaselinePct\%,144\ThyCagrMultilabelCompilersBaselinePct\%, \ThyCagrMultilabelAlgorithmsBaselinePct\%,145\ThyCagrMultilabelFormalVerificationBaselinePct\% and \ThyCagrMultilabelProgrammingLanguagesBaselinePct\%146between 2018 and 2022. The acceleration is real but not specific: the corpus-wide multi-label growth rose from147\ThyCagrMultilabelTotalBaselinePct\% to \ThyCagrMultilabelTotalPostPct\% over the same periods, so the six148categories accelerated with the corpus rather than within it. Measured by primary-label share, every category149lost ground between 2018 and 2025: algorithms from \ThySharePrimaryAlgorithmsTwoZeroOneEightPct\% to150\ThySharePrimaryAlgorithmsTwoZeroTwoFivePct\%, software engineering from151\ThySharePrimarySoftwareEngineeringTwoZeroOneEightPct\% to \ThySharePrimarySoftwareEngineeringTwoZeroTwoFivePct\%,152formal verification from \ThySharePrimaryFormalVerificationTwoZeroOneEightPct\% to153\ThySharePrimaryFormalVerificationTwoZeroTwoFivePct\%, programming languages from154\ThySharePrimaryProgrammingLanguagesTwoZeroOneEightPct\% to \ThySharePrimaryProgrammingLanguagesTwoZeroTwoFivePct\%,155computational complexity from \ThySharePrimaryComputationalComplexityTwoZeroOneEightPct\% to156\ThySharePrimaryComputationalComplexityTwoZeroTwoFivePct\% and compilers from157\ThySharePrimaryCompilersTwoZeroOneEightPct\% to \ThySharePrimaryCompilersTwoZeroTwoFivePct\%. The theory and158software categories are growing and shrinking at once: more works, a smaller fraction of a corpus whose growth159is set by the AI categories of Part~V.160161\input{tables/tab_theory_counts}162\input{tables/tab_theory_counts_primary}163164Two cautions attach to these numbers. The post-period growth rate spans two years and is exposed to the165indexing lag of the most recent year (Section~\ref{sec:m-truncation}); the primary-label counts for 2025 are166the last complete ones. And the file \texttt{results/bibliometrics/cagr\_by\_category.csv}, from which167Table~\ref{tab:cagr} is generated, reports primary counts for these categories about three times smaller than168those of the graph counts file (algorithms in 2018: \ThyCagrfileAlgorithmsNTwoZeroOneEight{} against169\ThyCountAlgorithmsTwoZeroOneEightPrimary{}), so it predates the current classification; its growth rates are170not used here, and the discrepancy is recorded for the reproducibility audit.\footnote{The generator171\texttt{bibliometrics/04\_diversity\_cagr.py} reads \texttt{category\_counts\_yearly.csv}; re-running it on the172current counts resolves the discrepancy. Until then, Table~\ref{tab:cagr} and Table~\ref{tab:theory_summary}173disagree for these six rows.}174175\input{tables/tab_theory_summary}176177\subsection{Structural change at the reference date}178179The interrupted-time-series slope change at December 2022 is positive for all six primary-label series and180significant with HAC standard errors (Section~\ref{sec:m-its}): \ThyBreakAlgorithmsChatgptSlopePct\% per month181for algorithms, \ThyBreakComputationalComplexityChatgptSlopePct\% for computational complexity,182\ThyBreakProgrammingLanguagesChatgptSlopePct\% for programming languages,183\ThyBreakCompilersChatgptSlopePct\% for compilers, \ThyBreakFormalVerificationChatgptSlopePct\% for formal184verification and \ThyBreakSoftwareEngineeringChatgptSlopePct\% for software engineering. The placebo test185(Section~\ref{sec:m-placebo}) does not confirm any of them at the five per cent level: the share of186baseline-period pseudo-events whose slope statistic exceeds the observed one is187\ThyBreakAlgorithmsPlaceboSlopeP{} for algorithms, \ThyBreakComputationalComplexityPlaceboSlopeP{} for188computational complexity, \ThyBreakSoftwareEngineeringPlaceboSlopeP{} for software engineering,189\ThyBreakCompilersPlaceboSlopeP{} for compilers, \ThyBreakFormalVerificationPlaceboSlopeP{} for formal190verification and \ThyBreakProgrammingLanguagesPlaceboSlopeP{} for programming languages. The two theory191categories are closest to the threshold; none crosses it. A slope change that pseudo-events of the baseline192reproduce at these rates is a feature of series that were already accelerating, not of the reference date.193194\input{tables/tab_theory_breaks}195196The level changes point the other way in five categories. At December 2022 the level fell by197\ThyBreakFormalVerificationChatgptLevelPct\% for formal verification ($p = \ThyBreakFormalVerificationChatgptLevelP$),198\ThyBreakComputationalComplexityChatgptLevelPct\% for computational complexity199($p = \ThyBreakComputationalComplexityChatgptLevelP$), \ThyBreakAlgorithmsChatgptLevelPct\% for algorithms200($p = \ThyBreakAlgorithmsChatgptLevelP$), \ThyBreakProgrammingLanguagesChatgptLevelPct\% for programming201languages and \ThyBreakCompilersChatgptLevelPct\% for compilers (both not significant); only software202engineering shows a positive level change (\ThyBreakSoftwareEngineeringChatgptLevelPct\%,203$p = \ThyBreakSoftwareEngineeringChatgptLevelP$), and it is also the only category with a significant positive204level change at the GPT-4 date (\ThyBreakSoftwareEngineeringGptFourLevel{},205$p = \ThyBreakSoftwareEngineeringGptFourLevelP$; Section~\ref{sec:m-altdates}). The negative level changes206are at least partly the seasonality of proceedings dates in categories dominated by conferences, and the207alternative-date estimates for the o1 date (\ThyBreakComputationalComplexityOOneLevel{} for computational208complexity, $p = \ThyBreakComputationalComplexityOOneLevelP$) show how sensitive a level estimate is to where209the window is cut. The Bai--Perron procedure (Section~\ref{sec:m-bp}) dates a single break at210\ThyBreakAlgorithmsBpBreaksBic{} for algorithms, computational complexity and compilers, two breaks for211programming languages (\ThyBreakProgrammingLanguagesBpBreaksBic{}) and formal verification212(\ThyBreakFormalVerificationBpBreaksBic{}), and one at \ThyBreakSoftwareEngineeringBpBreaksBic{} for software213engineering: the data-driven dates fall in spring 2023 for the three categories with a single break, which is214after the reference date and before the GPT-4 release had been indexed, and they say nothing about cause.215216\subsection{Vocabulary moves, citations do not}217218Composition is where the window is visible. Table~\ref{tab:theory_llm_cooccurrence} reports, for each219category and year, the number of works that the multi-label classifier also assigns to the LLM category and220their share of the category. Between 2022 and 2025 that share rose from221\ThyCoocSoftwareEngineeringLlmTwoZeroTwoTwoPct\% to \ThyCoocSoftwareEngineeringLlmTwoZeroTwoFivePct\% in222software engineering, from \ThyCoocProgrammingLanguagesLlmTwoZeroTwoTwoPct\% to223\ThyCoocProgrammingLanguagesLlmTwoZeroTwoFivePct\% in programming languages, from224\ThyCoocCompilersLlmTwoZeroTwoTwoPct\% to \ThyCoocCompilersLlmTwoZeroTwoFivePct\% in compilers, from225\ThyCoocFormalVerificationLlmTwoZeroTwoTwoPct\% to \ThyCoocFormalVerificationLlmTwoZeroTwoFivePct\% in formal226verification, and from \ThyCoocAlgorithmsLlmTwoZeroTwoTwoPct\% to \ThyCoocAlgorithmsLlmTwoZeroTwoFivePct\% in227both algorithms and computational complexity. The gradient runs from the code-facing categories to the228mathematical ones, and it is a gradient of vocabulary: co-classification is a lexical and topical signal229(Section~\ref{sec:m-classification}), not a measure of method adoption.230231\input{tables/tab_theory_llm_cooccurrence}232\input{tables/tab_theory_llm_cooccurrence_counts}233234Citation flows are more conservative. In the post period, software-engineering works direct235\ThyFlowSoftwareEngineeringToLlmPostPct\% of their categorised references to works of the LLM category,236computational complexity \ThyFlowComputationalComplexityToLlmPostPct\%, compilers237\ThyFlowCompilersToLlmPostPct\%, programming languages \ThyFlowProgrammingLanguagesToLlmPostPct\%, formal238verification \ThyFlowFormalVerificationToLlmPostPct\% and algorithms \ThyFlowAlgorithmsToLlmPostPct\%; the239within-category shares barely moved (algorithms \ThyFlowAlgorithmsToAlgorithmsBaselinePct\% to240\ThyFlowAlgorithmsToAlgorithmsPostPct\%, software engineering241\ThyFlowSoftwareEngineeringToSoftwareEngineeringBaselinePct\% to242\ThyFlowSoftwareEngineeringToSoftwareEngineeringPostPct\%, formal verification243\ThyFlowFormalVerificationToFormalVerificationBaselinePct\% to244\ThyFlowFormalVerificationToFormalVerificationPostPct\%).\footnote{Flows are aggregated from245\texttt{results/graph/category\_flows\_yearly.csv} over citing years 2018--2022 (baseline) and 2023--2026246(post) and are shares of the references that fall inside the categorised corpus (Section~\ref{sec:m-citgraph}).247The LLM category is young, which depresses its share of cited works mechanically; the comparison with the248co-classification shares is therefore indicative, not a test.} Two flow changes deserve notice. The249self-citation share of computational complexity fell from250\ThyFlowComputationalComplexityToComputationalComplexityBaselinePct\% to251\ThyFlowComputationalComplexityToComputationalComplexityPostPct\% while its references to human--computer252interaction rose from \ThyFlowComputationalComplexityToHciBaselinePct\% to253\ThyFlowComputationalComplexityToHciPostPct\%; given the candidate list of254Section~\ref{sec:thy-landmarks}, this is more plausibly the category's contamination by social-science works255than a change in theoretical research, and it is recorded as a contested reading. Inbound citations to formal256verification from computer vision doubled, from \ThyInflowFormalVerificationFromComputerVisionBaselinePct\% to257\ThyInflowFormalVerificationFromComputerVisionPostPct\% of the category's inbound references, which is258consistent with the neural-network verification literature reviewed in Section~\ref{sec:thy-fv} being cited by259robustness work; no paper-level breakdown tests this.260261\section{Algorithms and data structures}262\label{sec:thy-algorithms}263264\subsection{What the window established}265266The category's largest results are not in the candidate list, and the first task of the review is to say what267they are, from verified records. Maximum flow and minimum-cost flow were brought to almost-linear time268\citep{chen2022maxflow}, closing a line of work that had run through interior-point methods and dynamic graph269data structures for a decade. Single-source shortest paths with negative weights were brought to near-linear270time by a combinatorial algorithm \citep{bernstein2022negative}, a result republished in the \emph{Journal of271the ACM} and \emph{Communications of the ACM} in 2025. The sorting barrier for directed single-source shortest272paths, the $\Omega(m + n \log n)$ cost that Dijkstra's algorithm with a priority queue cannot avoid, was273broken by a deterministic $O(m \log^{2/3} n)$ algorithm \citep{duan2025sorting}, the best paper of STOC~2025.274In data structures, the open-addressing bounds conjectured by Yao in 1985 were shown to be beatable: without275reordering, a greedy scheme achieves expected amortised probe complexity $O(\log^2 \delta^{-1})$ at load276$1 - \delta$, against the conjectured $\Theta(\delta^{-1})$ \citep{farachcolton2024openaddressing}. These277four results, from 2022 to 2025, are what a specialist would list first for the window; none has the citation278profile that the ranking rewards, because theoretical results are cited by a small community over long279horizons, and the 36-month window and the field normalisation are both calibrated on the behaviour of280applied categories.281282What the corpus does record is the programme of \emph{algorithms with predictions}, which the baseline period283established and the window continued. The candidate list carries it through a 2024 arXiv re-posting of the 2018284conference paper on ski rental and non-clairvoyant scheduling with machine-learned predictions, whose285abstract describes algorithms that are ``oblivious to the performance of the predictor, improve with better286predictions, but do not degrade much if the predictions are poor''; the programme's canonical references are287the journal version of competitive caching with learned advice \citep{lykouris2021caching} and the overview in288\emph{Communications of the ACM} \citep{mitzenmacher2022predictions}. The formal object is a pair of289guarantees, consistency (the competitive ratio when the prediction is exact) and robustness (the ratio under290arbitrary error), with a trade-off between them; it is the point at which online algorithms and machine291learning meet without either giving up its guarantees, and it is the one place in the category where the292``learning'' vocabulary of the window names a theory rather than a tool. The fine-grained complexity programme293that organised algorithms research at the baseline (Section~\ref{sec:p2-theory}) is represented in the294bibliography by the ICM survey \citep{vassilevskawilliams2019finegrained} and by the parameterized-algorithms295monograph \citep{cygan2015parameterized}.296297\subsection{What the candidate list contains}298299Of the \ThyAuditAlgorithmsN{} algorithms candidates, \ThyAuditAlgorithmsInScopeResearch{} are research300contributions and none is misclassified; the rest are textbook chapters, re-deposited classics, theses and301metaheuristics. The two post-period research candidates are modest and both carry citation counts that belong302to other works: the WADS~2025 paper extends Kd-trees to Bregman divergences, shows that the triangle inequality303is not needed for correct pruning, and reports two orders of magnitude over linear search for304Kullback--Leibler nearest-neighbour queries in up to a hundred dimensions \citep{pham2025kdtree}; the SEA~2024305paper replaces the highest-degree branching rule of branch-and-reduce for maximum independent set with a graph306neural network \citep{langedal2024mis}. Both abstracts describe engineering contributions with experimental307evaluation, which is what algorithm engineering is; neither is the kind of result that defines the window.308309The other research genre in the list is the metaphor-based metaheuristic: the Arithmetic Optimization Algorithm310\citep{abualigah2021aoa} and the Aquila Optimizer \citep{abualigah2021aquila} in 2021, and the artificial311lemming, glider snake, gray langur and starfish optimisers in 2025--2026, published in engineering and312AI-review journals and evaluated on CEC benchmark functions and constrained design problems. The abstracts share313a template, a natural metaphor mathematically modelled into exploration and exploitation phases and314``outperforming or matching'' a dozen earlier metaheuristics. The operational-research literature has argued315since \citet{sorensen2013metaphor} that the genre re-describes existing methods under new names and that its316benchmarks do not discriminate; the position was restated in a ``call for action'' \citep{aranha2021metaphor}317and substantiated for six widely cited algorithms, shown to be equivalent to or special cases of earlier318methods \citep{camachovillalon2022exposing}. The corpus does not adjudicate this dispute; what it shows is319the genre's weight in the highly cited stratum of the algorithms category, where six of twenty-five candidates320belong to it and where the post-2022 research articles with the highest normalised scores are of this kind.321Whether the genre grows faster than the rest of the category and absorbs a growing share of its citations is an322open problem of Part~X (G-P7), answerable with a keyword-defined subseries.323324\subsection{Algorithms discovered by learning systems}325326Three Nature papers and one preprint report algorithms found by reinforcement learning or program search:327faster matrix-multiplication tensor decompositions for small sizes \citep{fawzi2022alphatensor}, shorter328sorting networks for short sequences, merged into a standard library \citep{mankowitz2023alphadev}, new329constructions for the cap-set problem and bin packing from evolved programs \citep{romeraparedes2024funsearch},330and, as a 2025 preprint, a coding agent that reports improvements on a collection of open mathematical and331algorithmic problems \citep{novikov2025alphaevolve}. All four are reports by the developers; the improvements332are on specific instances; and no independent reproduction or extension by the theory community appears in the333verified bibliography. The question these works pose to the category, whether search over programs changes how334algorithms are designed or only how constants are tuned, is one the corpus cannot answer at this granularity;335it is stated as open problem G-P9. The honest position is that the window's algorithmic breakthroughs were336obtained by people, and that the learned-discovery results are promising, contested in scope, and awaiting337replication.338339\section{Computational complexity}340\label{sec:thy-complexity}341342The category's statistics are the least trustworthy of the six: \ThyAuditComputationalComplexityMisclassified{}343of its \ThyAuditComputationalComplexityN{} candidates are outside computing, and the flow and co-occurrence344changes of Section~\ref{sec:thy-statistics} are to that extent artefacts. The two in-scope research candidates345are a STOC~2019 paper and a 2026 \emph{Theoretical Computer Science} article on SAT in spiking neural P systems346(no abstract). The STOC paper is a genuine landmark of the baseline: its abstract describes the reachability347problem for Petri nets as open since the 1960s, with Lipton's 1976 exponential-space lower bound unimproved, and348establishes a non-elementary lower bound \citep{czerwinski2019petri}. The story was completed within the349baseline period, when reachability in vector addition systems was shown Ackermann-complete350\citep{czerwinski2021ackermann,leroux2021notprimitive}, matching the upper bound of Leroux and Schmitz; the351window inherits a closed problem whose closure the corpus ranks below a technology-acceptance survey.352353The window's own contribution to complexity theory that a specialist would name first is the simulation of354time $t$ in space $O(\sqrt{t \log t})$ \citep{williams2025sqrtspace}, which improves the Hopcroft--Paul--Valiant355simulation of 1975 after fifty years and implies, through a known argument, that there are problems solvable356in linear space that need nearly quadratic time on multitape machines; the paper is a STOC~2025 result357republished in the \emph{Journal of the ACM} in 2026. In additive combinatorics, the strong bounds for358three-term arithmetic progressions \citep{kelley2023threeap} brought the Roth-type exponent to a form conjectured359since Behrend. Neither appears in the candidate list; both enter through verified records, and the general360point is the one made for algorithms: results of this kind are cited slowly and by few, and a 36-month361field-normalised window does not see them.362363The boundary with language models is where the category's co-classification share grew, yet the relevant364works are mostly classified elsewhere. The proof that transformers with logarithmic precision lie in uniform365$\mathrm{TC}^0$ \citep{merrill2023parallelism}, and the survey of what formal languages transformers can366express \citep{strobl2024survey}, bound what a single forward pass can compute and make the case that367chain-of-thought computation is where additional expressive power must come from; they are, in the verified368bibliography, the window's main contribution of complexity theory to the study of the models that dominate369Part~V. Whether such works are classified under computational complexity or under natural language processing370is an empirical question about the taxonomy (open problem G-P8). The remainder of the candidate list is371teaching material, including the fourth edition of the Kolmogorov-complexity monograph \citep{li2019kolmogorov}372and undergraduate chapters on complexity and on parameterized complexity, and re-deposited classics, including373Turing's 1936 paper and Wolfram's cellular-automata chapters.374375\section{Programming languages}376\label{sec:thy-pl}377378The baseline lineage was set out in Section~\ref{sec:p2-pl}: Rust and its semantic foundation379\citep{matsakis2014rust,jung2017rustbelt,jung2021saferust}, Lean~4 as a prover that is also a programming380language \citep{demoura2021lean4} with its mathematical library \citep{mathlib2020}, and the verified381artefacts CompCert \citep{leroy2009compcert} and seL4 \citep{klein2009sel4} that showed production software382can be proved correct. The candidate list records this lineage only obliquely, through three theses of the383L4/seL4 school re-deposited in 2022 (separation logic for programs in virtual memory, formal memory models for384C systems code, a verified multiprocessor kernel design), which the ranking places in the post period. In the385window the lineage continued with Verus \citep{lattuada2024verus}, a verification framework for Rust programs386presented at SOSP~2024, which treats the ownership discipline of the language as the foundation for387specification and proof rather than as an obstacle to them; the content of Verus is known here from its verified388title and venue only.389390Of the \ThyAuditProgrammingLanguagesN{} candidates, \ThyAuditProgrammingLanguagesInScopeResearch{} are391research contributions. Two of them mark the entry of language models into the community's top venue in3922024. LLift \citep{li2024llift} combines static analysis with an LLM to find use-before-initialisation bugs in393the Linux kernel; its abstract reports post-constraint guidance of the path analysis, procedures for handling394``the unpredictable nature of LLMs'', and four previously unknown bugs acknowledged by the kernel community.395WhiteFox \citep{yang2024whitefox} is described by its abstract as the first white-box compiler fuzzer that uses396an LLM reading the source code of optimisations to generate test programs that exercise them, against397black- and grey-box fuzzing that lacks that information and symbolic execution that does not scale to a398compiler. Both papers report bugs found; neither reports a guarantee, and the abstracts do not claim one. The399natural comparison is with the two instruments that the compiler community built for correctness before the400window, Csmith's random differential testing, which found hundreds of bugs in production C compilers401\citep{yang2011csmith}, and Alive2's bounded translation validation of LLVM optimisations402\citep{lopes2021alive2}; whether LLM-generated tests can be combined with validation of that kind, so that the403share of reported bugs that are confirmed can be measured per optimisation pass, is open problem G-P4. The404third research candidate, ZEUS \citep{kalra2018zeus}, is the baseline representative of program analysis for a405new target: abstract interpretation and constrained Horn clauses applied to smart contracts, with an abstract406reporting that about 95\% of 22,400 contracts analysed were vulnerable. The universal fuzzer of407\citet{xia2024fuzz4all} and the LLM-based bug-reproduction study of \citet{kang2023fewshottesters} are the408software-engineering counterparts of the same move.409410The category's vocabulary moved more than any except software engineering's: co-classification with the LLM411category reached \ThyCoocProgrammingLanguagesLlmTwoZeroTwoFivePct\% in 2025. Its references to LLM works are412\ThyFlowProgrammingLanguagesToLlmPostPct\%, and its structural ties are unchanged, with413\ThyFlowProgrammingLanguagesToFormalVerificationPostPct\% of its references going to formal verification and414\ThyFlowProgrammingLanguagesToSoftwareEngineeringPostPct\% to software engineering in the post period, against415\ThyFlowProgrammingLanguagesToFormalVerificationBaselinePct\% and416\ThyFlowProgrammingLanguagesToSoftwareEngineeringBaselinePct\% at the baseline. Programming languages is, in417the citation graph, the hinge between verification and engineering, and the window did not move the hinge.418419\section{Compilers}420\label{sec:thy-compilers}421422Compilers is the smallest of the six categories, \ThySharePrimaryCompilersTwoZeroTwoFivePct\% of primary labels423in 2025, and the most lexically contaminated after complexity. Its in-scope candidates nevertheless trace a424coherent line. At the baseline, MLIR \citep{lattner2021mlir} is the infrastructure whose abstract promises to425reduce ``the cost of building domain specific compilers'' and to connect existing ones; Tiramisu426\citep{baghdadi2019tiramisu} is a polyhedral compiler whose scheduling language separates algorithm, loop427transformation, data layout and communication so that one algorithm can target multicores, GPUs and428distributed machines; ExaStencils is a four-layer domain-specific language for multigrid solvers. Two surveys429establish that learned compiler heuristics are a programme older than the window: the \emph{Proceedings of the430IEEE} survey of machine learning in compiler optimisation \citep{wang2018mlcompiler} and the \emph{Computing431Surveys} review of autotuning, optimisation selection and phase ordering \citep{ashouri2018autotuning}, which432dates the first attempts to the mid-1990s. Three MIT and Delaware theses on learned optimisation selection and433on sparse tensor-algebra compilation complete the baseline picture.434435The post-period candidates show the programme's change of scale. LLM4VV \citep{munley2024llm4vv} uses language436models to generate a validation test suite for directive-based parallel programming compilers (metadata only;437no abstract). LLM Compiler \citep{cummins2025llmcompiler} is a suite of foundation models built on Code Llama438and trained, per its abstract, on 546 billion tokens of LLVM intermediate representation and assembly, then439instruction-tuned to predict and emulate compiler behaviour; fine-tuned versions reach 77\% of the optimising440potential of an autotuning search for code size and disassemble x86-64 and ARM assembly back to LLVM-IR. The441preprint that preceded it \citep{cummins2023llmcompiler} framed the task as predicting optimisation-pass442sequences. The shift is from learning a heuristic inside a compiler, with features chosen by compiler writers,443to pre-training a model on the compiler's own artefacts; what the shift leaves open is the question that444compiler research has always had to answer last, correctness, which the field handled through differential445testing \citep{yang2011csmith} and translation validation \citep{lopes2021alive2} rather than through model446evaluation. Co-classification with the LLM category reached \ThyCoocCompilersLlmTwoZeroTwoFivePct\% in 2025;447references to LLM works are \ThyFlowCompilersToLlmPostPct\%, and the category's citations continue to go448first to computer architecture (\ThyFlowCompilersToComputerArchitecturePostPct\% of references in the post449period) and to itself. The deep-learning compiler stack recorded in the main bibliography, TVM, Triton and450PyTorch~2 \citep{chen2018tvm,tillet2019triton,ansel2024pytorch2}, and the image-processing DSL that preceded451it \citep{ragankelley2013halide}, belong to Part~VI and are only noted here as the other post-2018 development452of the category.453454\section{Formal verification}455\label{sec:thy-fv}456457Formal verification has the most in-scope research candidates of the six458(\ThyAuditFormalVerificationInScopeResearch{} of \ThyAuditFormalVerificationN{}) and the clearest internal459structure, which the review follows: solvers and competitions, neural-network verification, verification of new460targets, learned theorem proving, and the theory of verification.461462\paragraph{Solvers and competitions.}463cvc5 \citep{barbosa2022cvc5} is the system description of the SMT solver that succeeded CVC4, evaluated on all464SMT-LIB benchmarks against CVC4 and Z3; the Handbook of Satisfiability in its second edition465\citep{biere2021handbook} is the reference work, present twice in the candidate list under two records. The466SV-COMP~2024 report \citep{beyer2024svcomp} describes the largest edition of the software-verification467competition to that date, 76 tools from 34 teams on 30,300 verification tasks for C programs, with a second468track for witness validation and a new witness format. Competitions of this kind are the category's benchmark469culture, and they are a point of contrast with the benchmark culture of Part~V: the tasks are fixed programs470with fixed specifications, a tool's result is a proof or a counterexample that a validator checks, and the471score is not self-reported.472473\paragraph{Neural-network verification.}474The baseline built a sub-field: Reluplex \citep{katz2017reluplex} extended the simplex method to ReLU475constraints; the 2018 symbolic-interval preprint in the candidate list argued, per its abstract, that existing476analyses ``struggle to scale beyond very small networks'' and proposed interval propagation that does;477DeepPoly \citep{singh2019deeppoly} introduced an abstract domain of floating-point polyhedra with intervals and478transformers for ReLU, sigmoid, tanh and maxpool, and reported the first proofs of robustness to rotations479with interpolation; Marabou \citep{katz2019marabou} packaged SMT-based verification as a framework accepting480TensorFlow models. The VNN-COMP report \citep{brix2023vnncomp} summarises the first three years of the481competition that organised the sub-field. The doubling of formal verification's inbound citations from482computer vision in the post period (Section~\ref{sec:thy-statistics}) is consistent with this literature being483cited by robustness work, and the sub-field is the main channel through which the category meets the484machine-learning categories; whether it has guarantees that survive the scale of the models of Part~V is not a485question these abstracts address.486487\paragraph{New targets.}488VerX \citep{permenev2020verx} is described by its abstract as the first automated verifier of functional489properties of Ethereum smart contracts, combining reduction of temporal properties to reachability, a symbolic490execution engine for the Ethereum virtual machine, and delayed predicate abstraction, evaluated on 83491properties of 12 projects. The answer-set-programming monitor for automated driving \citep{klampfl2024asp}492and the theses on parametric and multi-objective Markov models represent runtime and probabilistic493verification; the Warwick thesis on model checking quantum protocols, re-deposited with a 2026 date, is a494baseline work of the previous decade.495496\paragraph{Learned theorem proving.}497The abstract attached in the corpus to the ITP~2023 paper, under a wrong title (Section~\ref{sec:thy-landmarks}),498is the clearest statement in the candidate set of what machine learning has done for automated reasoning:499MizAR \citep{jakubuv2023mizar} proves about 60\% of the theorems of the Mizar Mathematical Library in the hammer500setting and 75\% when given the premises of the human proofs, through the E and Vampire provers with the ENIGMA501and Deepire learned guidance and an incremental loop that grows a corpus of millions of proofs while training502stronger systems on it. This is the saturation-prover line. The language-model line is represented by Baldur503\citep{first2023baldur}, which generates and repairs whole Isabelle proofs; by LeanDojo504\citep{yang2023leandojo} and DeepSeek-Prover \citep{xin2024deepseekprover}, both preprints, which report505retrieval-augmented and synthetic-data-trained provers on Lean benchmarks; and by the position paper on formal506mathematical reasoning as a frontier \citep{yang2024formalmath}, also a preprint. The figures these works507report are on different benchmarks, under different compute budgets, with the possibility of overlap between508training corpora and test theorems that the abstracts do not exclude; a benchmark of theorems posted after the509training cut-off, with proof checking rather than self-reported success, is the direction stated as open510problem G-P5. The machine-learned mathematics of Part~V, olympiad geometry \citep{trinh2024alphageometry} and511program search \citep{romeraparedes2024funsearch}, is adjacent but distinct: it produces objects that a human or512a checker then verifies, where the works above produce the proofs.513514\paragraph{Theory of verification.}515Equality saturation as implemented in \emph{egg} \citep{willsey2021egg}, whose abstract describes e-graph516rewriting that ``only adds information'' and extraction by a user-supplied cost function, is a baseline result517republished as a research highlight in 2026; the quantitative interface automata of the CSL~2026 paper on reward518interfaces, whose abstract introduces multi-valued correctness requirements and best-effort satisfaction into519interface theories, is the one post-period research candidate of this kind.520521The category's primary share halved between 2018 and 2025 while its multi-label count grew by eleven per cent522(Tables~\ref{tab:theory_counts} and~\ref{tab:theory_counts_primary}). The arithmetic of the argmax assignment (Section~\ref{sec:m-score}) suggests523why: a work that carries a verification label and an AI or security label loses the primary label to the524larger category when the scores are close, so the primary series understates a category whose work is525increasingly done in combination. Measuring the share of works whose primary label switched, by co-assigned526category and year, is open problem G-P10.527528\section{Software engineering}529\label{sec:thy-se}530531Software engineering is where the window's change is largest, best documented, and most contested. Its532baseline was not AI-free (Section~\ref{sec:p2-pl}): the Codex models \citep{chen2021codex}, the533code-generation benchmarks \citep{austin2021mbpp}, the systematic evaluation of code models534\citep{xu2022codelms} and the first productivity assessment of neural code completion535\citep{ziegler2022copilot} precede the reference date, and the survey of machine-learning testing536\citep{zhang2022mltesting}, 144 papers on testing properties, components and workflows of learned systems,537shows the category already organised around learned software as an object of test. The window's surveys538reverse the direction of the relation. The survey of software testing with large language models539\citep{wang2024llmtesting} analyses 102 studies and reports, per its abstract, that test-case preparation and540program repair are the most common uses; the two systematic reviews of language models for software541engineering \citep{fan2023llm4se,hou2024llm4se} and the code-generation survey \citep{jiang2024codegensurvey}542map the same territory. Method papers from the main bibliography and the Part~VII-a bibliography give the543texture: program repair in the era of pre-trained models \citep{xia2023apr}, bug reproduction from reports544\citep{kang2023fewshottesters}, universal fuzzing \citep{xia2024fuzz4all}, and the agentic setting defined by545SWE-bench \citep{jimenez2024swebench} and SWE-agent \citep{yang2024sweagent}, both preprints, in which a model546is asked to resolve a GitHub issue end to end. Among the candidates, APISS \citep{chen2025apiss} retrieves547functionality-equivalent APIs through LLM embeddings to migrate proof-of-concept exploits, and a 2026 paper548proposes a multi-scale temporal model for just-in-time defect prediction; both are method contributions judged549from their abstracts.550551\paragraph{Productivity: two findings that need reconciling.}552The most cited post-period empirical candidate reports three randomised field experiments at Microsoft,553Accenture and an unnamed Fortune~100 company, run by the firms in the course of business, in which a random554subset of 4,867 developers received an AI coding assistant; the pooled estimate is a 26.08\% increase in555completed tasks with a standard error of 10.3\%, each experiment being ``noisy'' on its own, and less556experienced developers adopting more and gaining more \citep{cui2026genaiwork}. The earlier controlled557experiment on a single task reported a larger speed-up \citep{peng2023copilot}, and the field studies of558generative AI at work outside software \citep{brynjolfsson2023genaiwork,noy2023productivity,dellacqua2023jagged}559report the same pattern of larger gains for less experienced workers. Against these stands a 2025 randomised560trial preprint in which experienced open-source developers working on repositories they maintain took longer561to complete issues with AI tools than without \citep{becker2025metr}. The two findings are not contradictory562once population and outcome are distinguished: enterprise developers completing assigned tasks versus expert563maintainers resolving issues in mature codebases they know well, and tasks completed versus time per issue.564But the reconciliation is a reading of two abstracts, the second of a preprint, and the design that would565settle it, a preregistered multi-site trial stratified by experience and repository maturity with time-to-merge566and defect rate as joint outcomes, has not been run (open problem G-P3). The user studies of how programmers567interact with code-generating models \citep{barke2023groundedcopilot,vaithilingam2022expectation,liang2024usability}568supply the mechanism, acceleration mode against exploration mode, that any such trial would need to measure.569570\paragraph{Security of generated code.}571The security evaluations agree with one another. Copilot's suggestions were found vulnerable at a substantial572rate in 2022 \citep{pearce2022asleep}; the CCS~2023 user study found that participants with an AI assistant573wrote less secure code and believed it more secure \citep{perry2023insecure}; and the ICPEC~2025 study in the574candidate list, evaluating three open models on a filtered Big-Vul subset with eight CWE categories, reports575``a sharp contrast between high detection rates and markedly poor classification accuracy''576\citep{gasparlopes2025vuln}. High detection or completion paired with poor fine-grained security reasoning is577the consistent pattern across three designs, and it is the category's clearest negative result about the578models.579580\paragraph{The statistics.}581Software engineering has the highest co-classification with the LLM category of the six582(\ThyCoocSoftwareEngineeringLlmTwoZeroTwoFivePct\% of its works in 2025, from583\ThyCoocSoftwareEngineeringLlmTwoZeroTwoTwoPct\% in 2022), the largest post-period growth584(\ThyCagrMultilabelSoftwareEngineeringPostPct\% per year), the only positive level change at the reference585date and the only significant positive level change at the GPT-4 date (Section~\ref{sec:thy-statistics}).586Its references to LLM works are \ThyFlowSoftwareEngineeringToLlmPostPct\% in the post period, from587\ThyFlowSoftwareEngineeringToLlmBaselinePct\%, and inbound citations from the LLM category are588\ThyInflowSoftwareEngineeringFromLlmPostPct\% of its inbound references. Whether a vocabulary shift of this589size is a method shift, that is, whether the works co-classified with LLM cite LLM method papers at a higher590rate than the category's baseline, can be tested on the knowledge graph of Part~III once method nodes are591extracted for the high-priority set; it is open problem G-P2. The research-software case of the Astropy592project \citep[in the candidate list;][]{collberg2016repeatability} and the reproducibility literature of593Part~IX are the other side of the same category, and the only part of it where the window changed nothing594visible.595596\section{Synthesis}597\label{sec:thy-synthesis}598599Three conclusions follow, in decreasing order of evidential strength.600601The first is about the instrument. In the theory and software areas the automatically selected landmark602candidates do not identify landmarks: \ThyAuditVerdictInScopeResearch{} of \ThyAuditN{} are in-scope research603works, \ThyAuditIdCollision{} carry citation windows that belong to other works, and the rest are chapters with604generic titles, re-deposited classics, theses in small normalisation cells and lexical misclassifications. The605defects are identifiable and partly correctable at the selection stage, and the audit table606(Table~\ref{tab:theory_landmark_audit}) should accompany any use of the list; the major theoretical results of607the window, almost-linear flow, near-linear negative-weight shortest paths, the directed sorting barrier,608optimal open addressing, square-root-space simulation and the 3-progression bounds, are invisible to a60936-month field-normalised ranking and were brought into this review through verified records. The same610blindness will affect any bibliometric answer to RQ3 and RQ7 for these categories.611612The second is about the statistics. The six categories grew in absolute terms and declined in relative terms613after 2022; their slope changes at the reference date are positive but not distinguishable from pseudo-events614in the baseline; their vocabulary moved toward language models in proportion to their distance from615mathematics; and their citation behaviour moved little. For RQ2 the answer is that none of the six is among616the categories with structural change that survives the placebo test, and for RQ5 that the relationship with617the foundation-model categories changed in what these works say far more than in what they cite.618619The third is about the research. The substantive developments of the window are of two kinds that the corpus620treats very differently. Theoretical results were obtained by people, at the rate and in the venues of the621previous decade, and are cited accordingly. The entry of language models into verification, program analysis,622compiler testing and software engineering is visible in the co-classification statistics and in the abstracts623of the in-scope candidates, and it is where the open problems lie: guarantees for learned program analysis and624compiler testing (G-P4), comparability of learned provers (G-P5), the productivity effect on experienced625developers (G-P3), and the distinction between a vocabulary and a method (G-P2). What this half of Part~VII626can say with confidence is which of these questions the corpus can answer with its present instruments, and627which it cannot.628