% !TEX program = pdflatex %% The Rising-Sea Theses / The 57 Grothendieckian Problems — Pandoc LaTeX template. %% Journal-article form (author 2026-10-28, Q4): the AMS article class, no cover. Second layout (author 2026-10-28): %% a title block on the first page (title, subtitle, author, affiliation, ORCID iD, e-mail, abstract, MSC, keywords) %% under a line with the version, date, DOI and licence; a 132 mm measure (about 78 characters a line); bold %% headings set flush left; figures across the measure. %% Faces: the series TeX Gyre Pagella family and Pagella Math (series standard §2.1); A4. \PassOptionsToPackage{unicode,bookmarksnumbered}{hyperref} \PassOptionsToPackage{hyphens}{url} \documentclass[11pt,a4paper]{amsart} \usepackage[a4paper,textwidth=132mm,hmarginratio=1:1,top=27mm,bottom=30mm,headheight=14pt,headsep=8mm,footskip=11mm]{geometry} \usepackage{amsmath,amsthm,mathtools} % pdfLaTeX font set-up for the Hexagon deposit: the same TeX Gyre Pagella text faces (Type 1, T1) and newpxmath, % the Palatino-design companion of TeX Gyre Pagella Math; the sealed build used LuaLaTeX with fontspec. \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{textcomp} \usepackage{tgpagella} \usepackage[scale=0.92]{tgheros} \usepackage{tgcursor} \usepackage{amssymb} \usepackage{newpxmath} \input{rs-unicode.tex} \usepackage[protrusion=true,expansion=true]{microtype} \input{rs-microtype.tex} \usepackage{graphicx} \usepackage{longtable,booktabs,array,multirow,calc} \usepackage{enumitem} \usepackage{csquotes} \usepackage{xurl} \usepackage{xcolor} \usepackage{framed} \usepackage{needspace} \usepackage{fancyhdr} \usepackage[font=small,labelfont=sc,labelsep=period,justification=justified,singlelinecheck=true,skip=6pt]{caption} \usepackage{hyperref} %% ---- Pandoc compatibility shims -------------------------------------------------------------------------------- \providecommand{\tightlist}{\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}} \providecommand{\passthrough}[1]{#1} \providecommand{\LTcaptype}{table} \makeatletter \@ifundefined{c@none}{\newcounter{none}}{} \makeatother %% ---- the paper's metadata (metadata.yaml) ---------------------------------------------------------------------- \newcommand{\RStitle}{The 57 Grothendieckian Problems} \newcommand{\RSsubtitle}{Open Problems for Mathematics and Machine Reasoning from the Grothendieckian Programme} \newcommand{\RSshorttitle}{The 57 Grothendieckian Problems} \newcommand{\RSauthor}{Vincent Liu} \newcommand{\RSaffiliation}{WiseMotif.ai} \newcommand{\RSaffiliationurl}{https://wisemotif.ai} \newcommand{\RSemail}{vincent.liu@wisemotif.ai} \newcommand{\RSorcid}{https://orcid.org/0009-0000-8718-222X} \newcommand{\RSversion}{Preprint · Version 1.0} \newcommand{\RSdate}{28 October 2026} \newcommand{\RSlicence}{CC BY 4.0} \def\RSdoi{10.5281/zenodo.23734427} % \def, not \newcommand: the title block tests it against \@empty \newcommand{\RSmsc}{Primary 00A07; Secondary 68T01, 68V15, 03B35, 18F10} \newcommand{\RSkeywords}{Grothendieckian Programme, open problems, machine reasoning, formal verification, Lean, descent} \hypersetup{pdftitle={The 57 Grothendieckian Problems: Open Problems for Mathematics and Machine Reasoning from the Grothendieckian Programme},pdfauthor={Vincent Liu},pdfkeywords={Grothendieckian Programme, open problems, machine reasoning, formal verification, Lean, descent}, pdfsubject={Open Problems for Mathematics and Machine Reasoning from the Grothendieckian Programme},pdflang={en-GB}} %% ---- the house layer: title block, headings, theses, problem cards, figures, references ------------------------ \input{rs-header.tex} \begin{document} \RSmaketitle{% We state fifty-seven open problems drawn from the seven works of the Grothendieckian Programme (34 volumes, 26,021 pages, released openly in October 2026 as first drafts that have not been peer-reviewed). Thirty-five come from the two works on the architecture of a reasoning system and twenty-two from the five works that each take a named conjecture or programme as research subject; no problem is one of those conjectures. Each problem is stated in the words of its source, located by work, chapter and page, given the status the source assigns it, and paired with a criterion that decides when it is solved, a note on existing work and the date of a literature check. The problems are of three kinds: twenty-five mathematical problems, nineteen machine problems with success criteria fixed in advance, and thirteen formalization problems for Lean 4 and Mathlib. Every quotation from the sources has been checked against the published PDFs, and each problem has been checked against the literature as of 28 October 2026; a machine-readable version accompanies the paper. } \RSepigraph{``All right, take 57.''}{As told in A. Jackson, \emph{Notices Amer. Math. Soc.} 51 (2004), p.~1196} \section{Introduction}\label{introduction} In a mathematical conversation, someone suggested to Grothendieck that they should consider a particular prime number; asked whether that meant an actual number, and told that it did, Grothendieck answered ``All right, take 57.'' Allyn Jackson tells the story as ``the legend of the so-called ``Grothendieck prime''\,'', to illustrate how little his thinking relied on examples {[}Jac04, pp.~1196--1197{]}. Fifty-seven is \(3 \times 19\). We take the title of this paper from the story for a second reason as well: a list of problems drawn from first drafts will contain errors of its own, and the place to report them is given with every problem below. The fifty-seven problems are drawn from the seven works of the Grothendieckian Programme {[}S01; S02; S03; S04; S05; S06; S07{]}, with the overview {[}S00{]}. The works were released on Zenodo between 20 and 25 October 2026, under a CC BY-NC-ND 4.0 licence, as a Research Architecture Edition. Together they comprise 34 volumes and 26,021 pages. They are first drafts and have not been peer-reviewed. The first two works are on the architecture of a reasoning system for mathematics: \emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]} treats mathematical worlds as typed, versioned objects that can be compared and carried from one setting to another, and \emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]} builds a reasoning kernel on sites, sheaves and descent. The other five works each take a research subject --- the Riemann Hypothesis, the conjecture of Birch and Swinnerton-Dyer, the Hodge conjecture, the \(abc\) conjecture and the Langlands programme --- and record what a single method, carried out in full, establishes about it, what it reduces to stated hypotheses, and what it leaves open. None of the seven works claims a proof of any of these conjectures, and none of the problems below is one of them. This is the third of three papers released together. The first, \emph{The Grothendieckian Programme: An Overview} {[}Liu26a{]}, describes the architecture of the Programme, its five research subjects, its method and the series. The second, \emph{The Rising-Sea Theses} {[}Liu26b{]}, states twelve theses on mathematics and machine reasoning drawn from the same works. Each problem below is attached to one thesis; the problems are the points at which the theses can be tested. \figref{rose} shows the fifty-seven problems in the seven works, with their kinds and levels. \begin{figure}[p] \centering\input{fig-rose.tex} \caption{The fifty-seven problems in the seven works, in the honeycomb of {[}S00, Figure 1{]}: Problems 1--35 (Part I) from {[}S01{]} and {[}S02{]}, Problems 36--57 (Part II) from the five works on research subjects. Within each work the problems are grouped by kind; the dots under a number give its level (one: entry, two: research, three: programme). Each small cell links to its card.}\label{fig:rose} \end{figure} \subsection{Selection}\label{selection} The seven works state many items as open, conditional, conjectural or owed. We extracted them by script from the sealed PDFs, using the status notation of each work: 1,040 items in all (73 in {[}S01{]}, 113 in {[}S02{]}, 111 in {[}S03{]}, 136 in {[}S04{]}, 179 in {[}S05{]}, 204 in {[}S06{]}, 224 in {[}S07{]}). From these we selected fifty-seven by four rules (\figref{selection}); the list of extracted items, with work, number, status and page, is in the repository. \begin{figure}[tbp] \centering\input{fig-selection.tex} \caption{How the problems were chosen: the items extracted from the seven works, the four rules below, the literature check of Section 1.3, whose changes are listed in Appendix B, and the problems by part and by kind.}\label{fig:selection} \end{figure} \begin{enumerate} \def\labelenumi{\arabic{enumi}.} \tightlist \item \emph{The problem is stated in the source.} Each problem is an open problem, conjecture, obligation, falsification test or question printed in one of the seven works, and the card quotes the source wherever it gives the source's words. Where the problem below narrows or makes precise the source's statement, the card says so. \item \emph{The problem is not a named conjecture.} The Riemann Hypothesis and its generalisations, the conjecture of Birch and Swinnerton-Dyer, the Hodge, standard, Tate, \(abc\), Szpiro and Vojta conjectures, Grothendieck's section conjecture and the Langlands correspondence appear in the cards only as background. A problem whose solution would by itself prove one of them is excluded. So are problems that turn on the disputed step of inter-universal Teichmüller theory, on which the sources record a disagreement without adjudicating it {[}S06{]}. \item \emph{The problem is open as far as we can determine.} Every problem was checked against the literature on 28 October 2026 (see below). Seven candidates were changed as a result: five were replaced by other problems from the same works and two were narrowed; the changes and their reasons are listed in Appendix B. \item \emph{The problem has a decision criterion.} Each card states what counts as a solution, so that a solution can be checked by someone other than its author and other than us. \end{enumerate} Thirty-five problems come from the two architectural works and twenty-two from the five research subjects, four or five from each. By kind, twenty-five are mathematical problems, nineteen are \emph{machine problems} --- a system to be built or an experiment to be run, with its success criterion fixed in advance --- and thirteen are formalization problems. Eleven are marked \emph{entry level}: a solution needs no new theory. Thirty-five are \emph{research level}. Eleven are marked \emph{programme level}: they are the problems on which the respective work depends as a whole. \subsection{What a card contains}\label{what-a-card-contains} Each problem is given in a fixed format. The heading of a card gives the number and title of the problem, its kind and its level. \emph{Thesis} names the thesis of \emph{The Rising-Sea Theses} to which the problem belongs. \emph{Source} names the work, the place in it and the page of the sealed PDF; the page is the printed folio. \emph{Status in the source} is the status that the source assigns, in its own notation. \emph{Statement} states the problem. \emph{What the source establishes} records what has been proved or specified, and what the source itself says about the gap. \emph{Proposed by} names the source of the problem and, where the problem or its subject has an earlier origin, that origin. \emph{Background} cites the standard literature on which the problem rests. \emph{Solved when} states the decision criterion. \emph{Literature check} records what the check of 28 October 2026 found. \figref{card} shows the card of Problem 49 in this format. \begin{figure}[tbp] \centering\input{fig-card.tex} \caption{What a card contains, with the card of Problem 49 as the example: on the left the heading and the first words of each field, on the right what each field records. Below, what is published with every card.}\label{fig:card} \end{figure} The words between quotation marks in a card are those of the source, on the pages named; this has been checked by machine for every quotation. A quotation from a work of the Programme is not a claim of this paper that the quoted statement is correct. \subsection{The literature check}\label{the-literature-check} For each problem we ran two or more search strings against arXiv, OpenAlex, zbMATH Open and Crossref, and, for the formalization problems, a code search of the Lean 4 repository, of Mathlib and of the Formal Conjectures collection {[}FLM+26{]}; we then read the results that bore on the problem. The searches, their dates and their first results are published with the paper. A search can show that something exists; it cannot show that nothing exists. The check is therefore scoped to what was searched, and a problem that turns out to have been answered elsewhere will be recorded as such. One finding is a correction to a source: a construction that {[}S03{]} describes as unknown has been published (Problem 38); it is recorded in the errata of the repository. The check also narrowed Problem 34 to what remains open, since independent checkers for Lean 4 now exist. \subsection{Participation and credit}\label{participation-and-credit} A solution, a partial result, a counterexample to a problem as stated, a report that a problem is already solved, or a correction to a card is submitted through the repository of the paper. Each problem has its own discussion thread, named in its card. A solution that meets the criterion of its card is recorded in the next version of this paper and in the next edition of the work from which the problem comes, under the solver's name, and in a list of solutions kept with the repository. No prize is attached to any problem (\figref{credit}). \begin{figure}[tbp] \centering\input{fig-credit.tex} \caption{Participation and credit: what can be submitted, where, how it is checked, and where a solution and a correction are recorded.}\label{fig:credit} \end{figure} The cards and a machine-readable file of all fifty-seven problems are released under CC BY 4.0, and the statements of the formalization problems in Lean 4, with the scripts that produced and checked this paper, under Apache-2.0, so that they can be translated, adapted and used as a benchmark. The seven works keep their own licence, and the quotations from them are reproduced under it with attribution. \RSpart{part-1}{Part I}{The Machine} The problems of this part come from the two works on the architecture of a reasoning system for mathematics: Problems 1--17 from \emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]} and Problems 18--35 from \emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}. Page numbers in {[}S01{]} run through its six volumes. \RSproblem{problem-1}{The first rising-sea event}{machine · programme level}{The first rising-sea event} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, §5.1, p.~8034, and §5.8, p.~8039. \RSfield{Status in the source}S/R (source-grounded synthesis; falsifiable research construction). \begin{RSbar} \RSfield{Statement}Carry out one operational rising-sea event in the sense of {[}S01, Vol. III, §5.1{]}. Such an event ``must begin from an explicit obstruction or language deficit, propose a typed extension, compile bounded probes, preserve or explicitly surrender recovery, record costs and residuals, and submit any status request to authority outside the producing engines.'' The problem asks for an event of this kind after which the original difficulty, stated before the event, has become tractable in the extended setting without the question having been changed. \end{RSbar} \RSfield{What the source establishes}The source fixes the sequence obstruction → typed extension → bounded execution and checking → computed, partial or failed → recovery and transport → external request, observes that ``Each arrow may fail'', and declines to promote the strategy: ``Volume III does not turn that strategy into a universal theorem of problem solving. It turns it into a falsifiable campaign record.'' It names four ways in which an extension changes the question instead of answering it: an extension that ``deletes the predicate expressing a contradiction, forgets the invariant detecting failure, weakens equality until disagreement disappears, or renames an unknown as a new primitive has not resolved the original obstruction.'' Section 5.8 specifies the residual and non-equivalence records that a partial outcome must leave. No event has been carried out. \RSfield{Proposed by}The image of the rising sea is Grothendieck's {[}McL07{]}; its operational form and this problem are from {[}S01{]}. \RSfield{Background}{[}McL07{]}; {[}Lak76{]}; machine-guided discovery with an external evaluator {[}DVB+21; RBN+24{]}. \begin{RSbar} \RSfield{Solved when}A campaign record is published that a third party can replay, in which (i) every step of the §5.1 sequence is present as a typed artifact; (ii) the target statement, frozen before the campaign, receives in the extended setting a kernel-checked proof, a kernel-checked refutation, or a reduction to named hypotheses with their statuses recorded; and (iii) a reviewer independent of the producing system certifies that none of the four failures of §5.1 applies. A complete record of a failed campaign is listed as a partial result. \end{RSbar} \RSfield{Literature check (28 October 2026)}No published campaign record of this form was found. Machine-guided discovery systems {[}DVB+21; RBN+24; TWL+24{]} evaluate candidates externally but do not record the four failure patterns or a separate status request. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/1}{Issue 1} of the repository. \par \RSproblem{problem-2}{A bounded fixed point of the coupled world--language cycle}{formalization · programme level}{A bounded fixed point of the coupled world–language cycle} \RSfield{Thesis}Thesis 10 (Discovery is recursive). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, §75.17, pp.~9503--9504; §75.11, pp.~9499--9500; §56.15, pp.~9130--9131. \RSfield{Status in the source}O (obligation). \begin{RSbar} \RSfield{Statement}Give a formal transition model of the coupled world--language cycle of {[}S01, Vol. III, Ch. 71--78{]} and prove, in a proof assistant, three properties of it: (a) the obligation-preservation inclusion \(O^{\mathrm{open}}_n \subseteq O^{\mathrm{open}}_{n+1} \cup O^{\mathrm{dis}}_{n+1} \cup O^{\mathrm{term}}_{n+1}\) of §75.11 holds for every accepted step; (b) the six conditions of §75.17 under which ``A cycle reaches BOUNDED\_FIXED\_POINT'' are decidable from the records; and (c) every run terminates, since ``A conforming campaign therefore carries a well-founded repair measure or a hard policy bound.'' \end{RSbar} \RSfield{What the source establishes}The conditions are stated as contracts; none is proved. Failure of the inclusion in (a) ``is sufficient for refusal or quarantine, regardless of the attractiveness of the new result.'' The source limits what a fixed point means: ``This is not equality of world and language, global convergence, consistency, optimality, or future stability.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}Transition systems and invariants in the style of {[}HW90{]}; mechanised metatheory {[}BW05{]}. \begin{RSbar} \RSfield{Solved when}A machine-checked development (Lean, Rocq, Isabelle or Agda) that defines the model, documents its correspondence with §§75.11 and 75.17 clause by clause, and proves (a)--(c); or a machine-checked counterexample showing that one of them fails in every model faithful to the source. \end{RSbar} \RSfield{Literature check (28 October 2026)}No formal model of this cycle was found; the searches returned general work on invariants in refinement-based verification only. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/2}{Issue 2} of the repository. \par \RSproblem{problem-3}{From obstruction to conjecture}{machine · research level}{From obstruction to conjecture} \RSfield{Thesis}Thesis 10 (Discovery is recursive). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. IV, §109.1, p.~11670, and §109.5, p.~11675 (algorithm ALG-118). \RSfield{Status in the source}ALG-R (research algorithm). \begin{RSbar} \RSfield{Statement}Implement the obstruction-driven conjecture generator ALG-118 of {[}S01, Vol. IV, Ch. 109{]}, which takes replayable, typed records of failed constructions or proof attempts and returns scoped conjectures, each with at least one executable falsifier, and run it until it produces a conjecture that is then settled by others. \end{RSbar} \RSfield{What the source establishes}The source specifies the contract and its limits: ``An obstruction can explain why a particular construction, proof route, or finite experiment failed. It does not by itself establish the negation, necessity, naturalness, or novelty of a conjecture inferred from that failure.'' Status is not affected by how a candidate looks: ``Frequency, linguistic plausibility, retrieval rank, model agreement, elegance, and apparent usefulness do not change its epistemic status.'' Falsifiers are part of the output, and ``No finite search can certify an unrestricted conjecture.'' No implementation exists. \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}Lak76{]}; automated conjecturing {[}Faj88; RGM+21{]}; {[}DVB+21{]}. \begin{RSbar} \RSfield{Solved when}An implementation run on a published set of typed obstructions, with the full record of every candidate and of its falsifiers, such that at least one generated conjecture that is not in the frozen corpus (in the scoped sense of {[}S01, Vol. IV, §110.8{]}) is afterwards proved, or refuted by a replayed counterexample, by parties independent of the generator. \end{RSbar} \RSfield{Literature check (28 October 2026)}Theory exploration and conjecturing systems were found {[}Faj88; RGM+21{]}; none takes typed obstruction records as input or attaches falsifiers to each output. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/3}{Issue 3} of the repository. \par \RSproblem{problem-4}{Minimal extension questions}{machine · research level}{Minimal extension questions} \RSfield{Thesis}Thesis 1 (Worlds, not isolated theorems). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, §24.10, pp.~8440--8441. \RSfield{Status in the source}O (obligation). \begin{RSbar} \RSfield{Statement}``MinimalExtensionQuestion turns a diagnosed deficit into an ordered search over semantic deltas.'' For a declared class of mathematical worlds and a declared partial order on deltas, give a procedure that, from an independently checked obstruction, returns an extension that is minimal for that order, consistent, conservative over the predecessor world, and reopens the blocked obligation; or prove that no such procedure exists for the class. \end{RSbar} \RSfield{What the source establishes}The question belongs to the Topos New-Creation Architecture (TNCA), the engine of {[}S01{]} that proposes successor worlds. The source fixes the meaning of minimality --- ``Minimality is relative to that declared partial order, not to implementation effort or textual brevity'' --- and gives the two failure modes it must avoid (jumping to a stronger logic, and refusing an extension that is needed). It states what is missing: ``TNCA has not shown existence, consistency, conservativity, or usefulness of any answer.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}Conservative extensions in logic and type theory; {[}Mac78{]} for the categorical constructions involved. \begin{RSbar} \RSfield{Solved when}A stated class of worlds (for example finitely axiomatised first-order theories or finite presentations of categories), a declared order on deltas, and a machine-checked proof that the procedure is correct on the class, with an implementation evaluated on published obstructions; or a machine-checked impossibility result for a class of comparable generality. \end{RSbar} \RSfield{Literature check (28 October 2026)}Work on conservative extension and minimal extensions in logic was found; no procedure with the inputs and guarantees of §24.10 was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/4}{Issue 4} of the repository. \par \RSproblem{problem-5}{Target fidelity}{machine · research level}{Target fidelity} \RSfield{Thesis}Thesis 6 (A chain of non-implications). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, §30.10, p.~8574, and §64.17, p.~9294; Architectural Prospectus, p.~7966; Vol. IV, §5.16, p.~9846. \RSfield{Status in the source}O (obligation). \begin{RSbar} \RSfield{Statement}A proof kernel checks a proof against a formal statement; it does not check that the formal statement is the mathematics it was meant to express. In the source: ``A named, pinned formal kernel may check a proof term against a formal target; target fidelity and publication authority remain separate obligations.'' Give a certificate format and checker for the fidelity of a formal statement to a statement in a source text, within a declared fragment of mathematical language and a declared library. \end{RSbar} \RSfield{What the source establishes}The source treats every machine proof as a candidate ``until source-target fidelity, kernel replay, and axiom-closure review pass under the same canonical subject key'', and lists among the open obligations of the formal layer to ``verify that adapted definitions and rule candidates faithfully reflect the cited locators and declared deltas'' and ``target-fidelity theorems connecting source constructs to generated declarations''. \RSfield{Proposed by}{[}S01{]}; the question is shared with the autoformalization literature {[}WJL+22; FLM+26{]}. \RSfield{Background}{[}BW05{]}; {[}WJL+22{]}; misformalization records in {[}FLM+26{]}. \begin{RSbar} \RSfield{Solved when}A certificate format that binds a formal target, a source locator and a declared map of definitions, and a checker that rejects every certificate in a published adversarial suite of statement pairs with deliberately introduced misformalizations (quantifier order, hypothesis loss, changed definitions) while accepting the faithful pairs, with the suite, the checker and the results released for independent replay. \end{RSbar} \RSfield{Literature check (28 October 2026)}Many 2025--2026 preprints measure faithfulness of autoformalization by scores or round-trip tests; none found issues a fidelity certificate of the kind required here. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/5}{Issue 5} of the repository. \par \RSproblem{problem-6}{Verified encodings of universal properties}{formalization · research level}{Verified encodings of universal properties} \RSfield{Thesis}Thesis 3 (A structured latent space). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, §18.5, p.~8307, and §21.16, item 8, p.~8370. \RSfield{Status in the source}O (obligation). \begin{RSbar} \RSfield{Statement}The component MUF-H (Motivic Universal Factorization Algorithm---Hybrid) of {[}S01{]} solves universal-property constraints for finite proxies of categories. ``A solver that returns a satisfying assignment only proves satisfiability of the encoded finite constraints if the encoding and certificate are independently checked. It does not establish that the encoding captures the intended universal property.'' For finite categories given by their composition tables, give an encoding of the statement that a cone (or cocone) is a limit (colimit) of a finite diagram into constraints a solver can decide, and prove the encoding correct. \end{RSbar} \RSfield{What the source establishes}The source requires that ``Universality encodings still require an independently checked correspondence between mathematical quantifiers and constraints'', and that existence of mediating maps and their uniqueness be recorded as separate obligations, since ``Universality requires a quantified mediating property and generally uniqueness at an explicitly stated identity strength.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}Mac78{]}; {[}MM94{]}. \begin{RSbar} \RSfield{Solved when}A machine-checked theorem that, for every finite diagram in a finite category, the solutions of the encoded constraints correspond bijectively to mediating morphisms and that the uniqueness check is complete, together with a verified checker for solver certificates. \end{RSbar} \RSfield{Literature check (28 October 2026)}General work on constraint solving and finite model finding was found; no verified encoding of universal properties was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/6}{Issue 6} of the repository. \par \RSproblem{problem-7}{The AURORA-K0 kernel, I: syntax and checking}{formalization · research level}{The AURORA-K0 kernel, I: syntax and checking} \RSfield{Thesis}Thesis 2 (Status is part of the type). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, §70.19, pp.~9428--9429 (obligations K0-META-001 to K0-META-009). \RSfield{Status in the source}O (``Every item begins OPEN''). \begin{RSbar} \RSfield{Statement}Mechanise AURORA-K0, the small formal kernel of the experimental calculus AURORA {[}S01, Vol. III, Ch. 70{]}, and discharge the first nine obligations of its registry, among them that the ``Concrete grammar has unique parsing after canonical Unicode normalization'', that ``Substitution preserves K0 typing'', that ``Registered reduction preserves typing'', that ``Algorithmic checking agrees with declarative K0 rules'', and that the ``Definitional equality procedure is decidable for the declared finite fragment''. \end{RSbar} \RSfield{What the source establishes}The registry lists each obligation with the evidence required before its status may change, and rules out the shortcut: ``No row may become RECEIPT\_BOUND merely because a checker returns success.'' No obligation is discharged. \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}The de Bruijn criterion and small kernels {[}BW05{]}; {[}MU21{]}; {[}Car24{]}. \begin{RSbar} \RSfield{Solved when}A development in a proof assistant that defines K0 as in the exact edition of Chapter 70 and proves K0-META-001 to K0-META-009 using no axioms beyond the assistant's standard ones; a machine-checked counterexample to any item also counts and is recorded as a correction to the source. \end{RSbar} \RSfield{Literature check (28 October 2026)}Mechanised metatheory of type theories is an established field; no mechanisation of K0 was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/7}{Issue 7} of the repository. \par \RSproblem{problem-8}{The AURORA-K0 kernel, II: a model and relative consistency}{formalization · research level}{The AURORA-K0 kernel, II: a model and relative consistency} \RSfield{Thesis}Thesis 2 (Status is part of the type). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, §70.19, pp.~9428--9429 (obligations K0-META-010 to K0-META-012). \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{14} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}For the kernel K0 of Problem 7, discharge the semantic obligations of the registry: ``At least one nontrivial model validates the rules''; ``Relative consistency, if pursued'', relative to a named base theory; and ``Conservativity over any source theory'' for the source theories that the architecture embeds. \end{RSbar} \RSfield{What the source establishes}The registry requires an explicit model construction with independent validation, a proposition-exact metatheorem for relative consistency, and an explicit interpretation with a conservativity proof, and records all three as open. \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}Models of type theory; {[}Uni13{]}; conservativity results for extensions of type theory. \begin{RSbar} \RSfield{Solved when}A machine-checked model of K0 that is not trivial in the sense of §70.19, and machine-checked proofs of relative consistency and of conservativity over at least one named source theory. \end{RSbar} \RSfield{Literature check (28 October 2026)}Mechanised relative-consistency proofs exist for other systems; none for K0 was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/8}{Issue 8} of the repository. \par \RSproblem{problem-9}{The seven obligations of descent execution}{formalization · research level}{The seven obligations of descent execution} \RSfield{Thesis}Thesis 5 (Report failure; abstain without evidence). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, §56.15, pp.~9130--9132, and §56.1, p.~9119. \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{14} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}The Grothendieckian Descent Reasoning Architecture (GDRA) of {[}S01{]}, the layer that executes local-to-global campaigns, exists to prevent one error: ``The central architectural error is to convert operational completion into global meaning.'' Give a formal transition model of GDRA campaigns and prove the seven properties that §56.15 leaves open: ``canonical serialization must preserve identity; every accepted transition must preserve the invariants; forbidden authority effects must be noninterfering; budget events must conserve declared dimensions; event replay must converge to the same eligible head under the stated delivery model; counterevidence closure must be omission-resistant; and adapters must preserve the disjoint failure constructors.'' \end{RSbar} \RSfield{What the source establishes}The source states the seven properties and the delivery model (at-least-once delivery with idempotent effects), and records: ``None has a supplied mechanized proof.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}Noninterference {[}GM82{]}; linearizability {[}HW90{]}. \begin{RSbar} \RSfield{Solved when}Machine-checked proofs of all seven properties for a model whose correspondence with Chapter 56 is documented clause by clause, or a machine-checked counterexample to one of them. \end{RSbar} \RSfield{Literature check (28 October 2026)}Noninterference and replay-safety proofs exist for other systems; none for this model was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/9}{Issue 9} of the repository. \par \RSproblem{problem-10}{Non-self-authorization}{formalization · research level}{Non-self-authorization} \RSfield{Thesis}Thesis 7 (Machines propose; humans authorize). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. V, Proposition 1.3, p.~11913; Proposition 5.1, p.~11940; Proposition 10.1, p.~11979. \RSfield{Status in the source}D/O (definition; obligation). \begin{RSbar} \RSfield{Statement}The rule that machines propose and humans authorise publication is stated in {[}S01, Vol. V{]} as three propositions, each conditional on assumptions about capabilities. Proposition 1.3 concludes that ``a non-root module cannot, through a conforming Volume V interface, make its own output both authoritative and active''; Proposition 10.1 that ``adding a validated evidence edge to an artifact cannot by itself increase the artifact's epistemic class''. Give a formal model of capabilities, signing and status transitions in which the hypotheses of Propositions 1.3, 5.1 and 10.1 are definitions, and prove the three conclusions. \end{RSbar} \RSfield{What the source establishes}The propositions are argued informally and marked D/O: ``The proposition is conditional on correct capability isolation and validator independence; those conditions are test obligations, not assumptions to be hidden.'' The negative cases (a worker writing to the status store, a signature detached from the artifact hash) are listed. \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}DV66{]}; {[}SS75{]}; {[}GM82{]}. \begin{RSbar} \RSfield{Solved when}Machine-checked proofs of the three propositions in a published model, and a test suite showing that each listed negative case is rejected by an implementation conforming to the model. \end{RSbar} \RSfield{Literature check (28 October 2026)}Verified capability machines and separation kernels exist; no formalisation of these three propositions was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/10}{Issue 10} of the repository. \par \RSproblem{problem-11}{Evolution without authority}{formalization · research level}{Evolution without authority} \RSfield{Thesis}Thesis 7 (Machines propose; humans authorize). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. VI, §11.11, p.~13204; Vol. III, §21.16, item 12, pp.~8370--8371. \RSfield{Status in the source}O (obligation O-V6-11-04). \begin{RSbar} \RSfield{Statement}A self-improving component may propose changes to itself but must not acquire authority. In {[}S01, Vol. VI{]} the obligation reads: ``O-V6-11-04 --- prove that no composition of EvolutionContract ports reaches signing, promotion, activation, root mutation, or rollback capabilities''. Prove it for a formal model of the evolution interface. \end{RSbar} \RSfield{What the source establishes}In the released architecture ``Evolution remains inert: telemetry cannot evaluate candidates, adapt routing, update policy, canary, promote, deploy, or roll back.'' The source does not claim more: ``Until these obligations are discharged, policy morphisms and version graphs are precise governance objects, not a claim that safe whole-system evolution has been solved.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}SS75{]}; reward hacking as the failure this obligation guards against {[}SHKK22{]}. \begin{RSbar} \RSfield{Solved when}A machine-checked reachability theorem over all finite compositions of the ports of the published EvolutionContract model, with the model's correspondence to Vol. VI, Ch. 11 documented; or a composition that reaches a forbidden capability. \end{RSbar} \RSfield{Literature check (28 October 2026)}Recent work studies privilege escalation in AI agents empirically; no formal reachability proof for an evolution interface of this kind was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/11}{Issue 11} of the repository. \par \RSproblem{problem-12}{Deterministic identity across implementations}{machine · entry level}{Deterministic identity across implementations} \RSfield{Thesis}Thesis 6 (A chain of non-implications). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. V, Proposition 2.2, p.~11920, and Proposition 3.2, p.~11927. \RSfield{Status in the source}D/O. \begin{RSbar} \RSfield{Statement}Build two independent implementations of the canonical serialization and replay profile of {[}S01, Vol. V{]} and show that they agree: identical canonical bytes and identifiers for the same artifacts (Proposition 2.2), and identical kernel judgments under identical inputs and environments (Proposition 3.2). \end{RSbar} \RSfield{What the source establishes}Proposition 2.2 is ``an interoperability obligation to be tested by cross-language fixtures.'' For replay, ``A disagreement is a first-class incident'', and ``The system does not choose the favorable result by majority vote.'' No second implementation exists. \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}LZ22{]}; {[}Nec97{]}. \begin{RSbar} \RSfield{Solved when}Two implementations in different languages by different authors, and a published fixture suite (Unicode normalisation, exact numbers, ordered and unordered collections, extension fields) on which they agree byte for byte, with every disagreement found during development recorded as an incident. \end{RSbar} \RSfield{Literature check (28 October 2026)}Reproducible-builds practice {[}LZ22{]} addresses the same property for software artifacts; no implementation of this profile was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/12}{Issue 12} of the repository. \par \RSproblem{problem-13}{A frozen benchmark for counterexample and proof discovery}{machine · entry level}{A frozen benchmark for counterexample and proof discovery} \RSfield{Thesis}Thesis 12 (Judge a method by its open ledger). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. IV, §113.1, p.~11744; §113.12.12 to §113.12.15, pp.~11763--11764. \RSfield{Status in the source}D (specified, not run). \begin{RSbar} \RSfield{Statement}Release the first version of the benchmark specified in {[}S01, Vol. IV, Ch. 113{]}. ``A benchmark is not merely a directory of examples and a script that prints a score.'' Before any run, it ``must freeze the task, version, population, split, metric, abstention policy, leakage boundary, resource model, and reporting semantics'', and it must separate counterexample tasks into strata A--F and proof tasks into the seven types of §113.12.13. \end{RSbar} \RSfield{What the source establishes}The specification is complete and unexecuted. Its scoring rules include that ``Stratum E evaluates whether the system reports bounded unknown honestly; it does not reward a claim that the theorem is true'', and that ``Hidden proofs are protected evaluation assets, not canonical solution paths.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}ZHP22{]}; {[}FLM+26{]}. \begin{RSbar} \RSfield{Solved when}A release with the four boundaries of §113.1 frozen by digest, at least one item in every counterexample stratum and every proof-task type, a working challenge process (§113.12.15), and results for at least two systems reported stratum by stratum. \end{RSbar} \RSfield{Literature check (28 October 2026)}Benchmarks for formal and research mathematics exist {[}ZHP22; FLM+26{]}; none found has the stratification, the abstention strata or the frozen constitution of Ch. 113. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/13}{Issue 13} of the repository. \par \RSproblem{problem-14}{The language forge, end to end}{machine · programme level}{The language forge, end to end} \RSfield{Thesis}Thesis 11 (Creating language). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. III, Preface, p.~7956; §43.14, p.~8873; §44.16, pp.~8888--8889; §45.8, p.~8898. \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{14} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}``The language forge follows a deliberately articulated cycle: collect, mine, name, notate, ground, reconstruct, axiomatize, grow, re-encode, and validate.'' Run the cycle of {[}S01, Vol. III, Ch. 41--48{]} end to end on a published corpus and produce a new notation and language package for a declared mathematical domain, with its metatheoretic obligations discharged. \end{RSbar} \RSfield{What the source establishes}The source specifies each stage and leaves completeness open: ``The order organizes a bounded language-formation workflow and leaves completeness as an open research question.'' It requires that ``Notation earns trust by declaring what it compresses, what it preserves, and what it cannot recover'', and that ``An obligation is not promoted because it is conventional for a language family or appears plausible from examples.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}Gan13{]}; {[}CF09{]}. \begin{RSbar} \RSfield{Solved when}A package for a declared domain in which every introduced primitive is linked to the structural motifs and counterexamples that motivated it, whose substitution, preservation and conservativity obligations (§44.16) are machine-checked, and whose round trips (Ch. 43) pass on a held-out set of statements from the domain. \end{RSbar} \RSfield{Literature check (28 October 2026)}Work on mathematical concept formation and on the language of mathematics {[}Gan13{]} was found; no end-to-end language-formation system with these obligations was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/14}{Issue 14} of the repository. \par \RSproblem{problem-15}{A preregistered test of typed base change}{machine · entry level}{A preregistered test of typed base change} \RSfield{Thesis}Thesis 1 (Worlds, not isolated theorems). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. I, §11.12, p.~277 (Conjecture V1-CH-011-C001); definitions, pp.~275--276. \RSfield{Status in the source}C (conjecture). \begin{RSbar} \RSfield{Statement}Test the conjecture of {[}S01, Vol. I, §11.12{]}: ``For a corpus whose categorical claims are already expressed as finite typed diagrams, requiring an RCP/RCT pair for each use of ``base change'' will reduce orientation and hypothesis errors relative to an untyped prose baseline.'' Here an RCP (relative change passport) records the bases, the base arrow and its variance, and an RCT (relative claim trace) records the status and hypotheses of the claim made after the change (Definitions V1-CH-011-D003 and D004). \end{RSbar} \RSfield{What the source establishes}``This is a falsifiable editorial-engineering conjecture. It requires a preregistered corpus, error taxonomy, reviewers, and comparison protocol; no performance result is claimed here.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}Preregistration {[}NEDM18{]}. \begin{RSbar} \RSfield{Solved when}A study whose corpus, error taxonomy, reviewer assignment and analysis are registered before data are collected, with independent reviewers, reporting the result in either direction. \end{RSbar} \RSfield{Literature check (28 October 2026)}No study of this question was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/15}{Issue 15} of the repository. \par \RSproblem{problem-16}{A preregistered test of the four judgments of gluing}{machine · entry level}{A preregistered test of the four judgments of gluing} \RSfield{Thesis}Thesis 5 (Report failure; abstain without evidence). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. I, §15.12, p.~361 (Conjecture V1-CH-015-C001). \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{2} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}Test the conjecture of {[}S01, Vol. I, §15.12{]}: ``On a preregistered corpus of local-to-global mathematical arguments, mandatory separation of compatibility, effectivity, uniqueness, and property return will reduce false ``gluing succeeds'' judgments relative to an untyped prose baseline.'' \end{RSbar} \RSfield{What the source establishes}``Testing requires fixed cases, independent reviewers, and an error taxonomy; no empirical result is claimed here.'' \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}NEDM18{]}; descent in {[}SGA4{]}. \begin{RSbar} \RSfield{Solved when}A preregistered study as in Problem 15, reporting the result in either direction. \end{RSbar} \RSfield{Literature check (28 October 2026)}No study of this question was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/16}{Issue 16} of the repository. \par \RSproblem{problem-17}{A preregistered test of obstruction records}{machine · entry level}{A preregistered test of obstruction records} \RSfield{Thesis}Thesis 5 (Report failure; abstain without evidence). \RSfield{Source}\emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]}, Vol. I, Ch. 17, p.~404 (Conjecture V1-CH-017-C001). \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{2} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}Test the conjecture of {[}S01, Vol. I, Ch. 17{]}: ``For a fixed benchmark of finite, fully enumerated lifting and gluing problems with independently verified ground truth, requiring the fields of ObstructionRecordV1 will reduce false ``no solution'' classifications relative to an otherwise identical checker that stores only a Boolean success flag.'' \end{RSbar} \RSfield{What the source establishes}``This is an empirical systems conjecture, not a mathematical theorem.'' The same section forbids the strengthening that every failed construction determines a cohomology class whose vanishing solves the problem. \RSfield{Proposed by}{[}S01{]}. \RSfield{Background}{[}NEDM18{]}; {[}Gir71{]} for obstruction classes. \begin{RSbar} \RSfield{Solved when}A preregistered comparison of the two checkers on a published benchmark with enumerated ground truth, reporting the false-negative rates of both with confidence intervals. \end{RSbar} \RSfield{Literature check (28 October 2026)}No study of this question was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/17}{Issue 17} of the repository. \par \RSproblem{problem-18}{Discovering the site}{machine · programme level}{Discovering the site} \RSfield{Thesis}Thesis 3 (A structured latent space). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, §1.2.5, p.~22. \RSfield{Status in the source}open (listed among ``The five things we are least sure of''). \begin{RSbar} \RSfield{Statement}In the architecture of {[}S02{]} a context is a site, the information it supports is a sheaf, and a conclusion is a global section. The site itself is supplied by hand: ``The site must be imposed. We do not know how to discover the evidence-atom locale from a corpus; we construct it.'' Give a procedure that constructs the evidence-atom locale, its refinement order and its covering families from a corpus, with a stated sufficiency criterion, and show that the result does not merely reflect the design of the procedure. \end{RSbar} \RSfield{What the source establishes}The source states the objection it cannot answer: ``a critic who says the invariants measure our design choices rather than the model's structure has a real point that we cannot fully answer.'' Learned restriction maps are studied elsewhere on a fixed graph {[}BDCLB22; DBDL24{]}; the base space is not learned there. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}HG19{]}; {[}BDCLB22{]}; {[}DBDL24{]}; {[}MM94{]}. \begin{RSbar} \RSfield{Solved when}A procedure and a published evaluation in which (i) planted sites in synthetic corpora are recovered up to a declared isomorphism budget, (ii) the site constructed from a natural corpus is stable under resampling within that budget, and (iii) invariants computed on it survive the gaming controls of {[}S02, §9.1{]} (terminal-site collapse, zero restrictions, filled nerve). \end{RSbar} \RSfield{Literature check (28 October 2026)}Sheaf neural networks with learned restriction maps on a given graph were found {[}BDCLB22; DBDL24{]}; no procedure that learns the site itself was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/18}{Issue 18} of the repository. \par \RSproblem{problem-19}{The capability wager}{machine · research level}{The capability wager} \RSfield{Thesis}Thesis 4 (Attention as descent). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Conjecture 3.6.17, p.~778; §1.2.5, p.~22. \RSfield{Status in the source}D (design-grade conjecture). \begin{RSbar} \RSfield{Statement}On an orthogonal cellular sheaf the non-abelian holonomy capacity \(\beta\) of {[}S02{]} is either \(0\) or at least a constant \(c(d)\) depending only on the stalk dimension. The wager is that \(\beta\) governs capability. In the words of the source: ``At matched parameters, data and compute, compare models with CERTIFIED\_VIRTUALLY\_ABELIAN and CERTIFIED\_FREE reports on tasks requiring route-dependent evidence.'' Decide the wager. \end{RSbar} \RSfield{What the source establishes}The dichotomy is proved; the wager is not. ``That β governs capability is grade D and we have no proof. It is the most interesting claim in the document and the least supported.'' The comparison is set up so that a negative result costs only the wager: ``No theorem links the verdict to capability; failure of the registered comparison removes the capability claim while leaving the group theorem intact.'' \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}The Tits alternative {[}Tit72{]}; uniform growth gaps {[}Bre11{]}; {[}HG19{]}. \begin{RSbar} \RSfield{Solved when}A preregistered comparison at matched parameters, data and compute, with certificates computed as in {[}S02, Ch. 3.6{]}, published with its outcome in either direction. \end{RSbar} \RSfield{Literature check (28 October 2026)}No study linking holonomy growth of cellular sheaves to model capability was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/19}{Issue 19} of the repository. \par \RSproblem{problem-20}{Nerve baselines between GRPO and RLOO}{machine · research level}{Nerve baselines between GRPO and RLOO} \RSfield{Thesis}Thesis 4 (Attention as descent). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, §1.2.4, pp.~21--22 (claim C11 of Appendix A7). \RSfield{Status in the source}open empirical question. \begin{RSbar} \RSfield{Statement}The source proves that the group-relative advantage of group relative policy optimisation (GRPO) {[}SWZ+24{]} equals \(\Delta_0 R/\lVert\delta_0 R\rVert_2\) for the \(0\)-Laplacian of the nerve of the sampling group, wherever \(\sigma>0\). This places GRPO in ``a family of graph baselines indexed by a nerve, of which the complete-graph member is GRPO and the i.i.d. leave-one-out member is RLOO.'' (RLOO is the leave-one-out REINFORCE baseline {[}ACG+24{]}.) Determine whether another member of the family reduces the variance of the policy-gradient estimate at matched cost. \end{RSbar} \RSfield{What the source establishes}The identity is proved and the family defined; ``Whether any other member of that family reduces variance at matched cost is an open empirical question, tested by claim C11 of A7 and unanswered here.'' \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}SWZ+24{]}; {[}ACG+24{]}; recent baselines for reinforcement learning with verifiable rewards {[}ZZA+25{]}. \begin{RSbar} \RSfield{Solved when}A theorem identifying, under stated assumptions on rewards, a nerve whose baseline has strictly smaller variance than both GRPO and RLOO at matched sampling cost, or proving that no member of the family does; or the registered experiment C11 with its outcome. \end{RSbar} \RSfield{Literature check (28 October 2026)}Variance-reduction baselines for GRPO-type methods are an active topic {[}ZZA+25{]}; no study of the nerve family was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/20}{Issue 20} of the repository. \par \RSproblem{problem-21}{Relative obstruction as a predictor of unsupported answers}{machine · research level}{Relative obstruction as a predictor of unsupported answers} \RSfield{Thesis}Thesis 5 (Report failure; abstain without evidence). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, §10.1.7.3, pp.~1854--1855; instrument N5, §9.1.7, p.~1766. \RSfield{Status in the source}T for the mathematics; D for what remains; N5 withdrawn. \begin{RSbar} \RSfield{Statement}For an evidence subdomain \(A\subseteq X\), a coefficient sheaf \(F\) and a partial section \(s_A\), the connecting class \(\partial(s_A)\in H^1(X,A;F)\) is a genuine obstruction to extending \(s_A\). Supply the typed record that the source requires before this class may be used as an instrument, and test prospectively whether it predicts unsupported answers of a language model. \end{RSbar} \RSfield{What the source establishes}The mathematics is proved; the instrument is not: ``N5 is therefore WITHDRAWN as a validation or falsification instrument.'' Reinstatement requires six items, including ``at least one worked non-zero example, together with a zero control, computed before labels are revealed''. The remaining task is stated as ``What remains is the difficult empirical part: the evidence sheaf must reflect factual support, the relative class must be approximated at scale, and prospective prediction must beat entropy, retrieval sufficiency, self-consistency and correctness probes without site collapse.'' \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}HG19{]}; {[}FKKG24{]}; {[}HRH24{]}. \begin{RSbar} \RSfield{Solved when}The six reinstatement items of §9.1.7 published for one benchmark, followed by a prospective comparison against entropy, sequence likelihood, verbal confidence, retrieval sufficiency, self-consistency and a trained correctness probe, reported in either direction. \end{RSbar} \RSfield{Literature check (28 October 2026)}Hallucination detectors based on entropy and probes exist {[}FKKG24{]}; sheaf-based consistency rating has been proposed {[}HRH24{]}; no instrument based on a relative connecting class was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/21}{Issue 21} of the repository. \par \RSproblem{problem-22}{Topos-MoE against modern sparse mixture-of-experts}{machine · research level}{Topos-MoE against modern sparse mixture-of-experts} \RSfield{Thesis}Thesis 4 (Attention as descent). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, §10.1.7.2, p.~1854; instrument N7, §9.1.9, pp.~1768--1769. \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{3} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}In Topos-MoE, the mixture-of-experts layer of {[}S02{]}, each expert is an open sub-topos and routing constructs a sufficient cover. Run the registered comparison N7 of {[}S02, §9.1.9{]} against a modern fine-grained sparse mixture-of-experts at matched total and active parameters, executed FLOPs, wall time and communication. ``Coverage routing must beat top-k on quality and on total cost; lowering its own deficiency score proves nothing about either.'' \end{RSbar} \RSfield{What the source establishes}The descent typing is proved; the benefit is not. In the released configuration the coverage router cannot yet be trained, and it ``may not report the coverage router as a trained component until that backward exists and is finite-difference checked.'' The thresholds are fixed in advance: ``Confirmation requires a 10 per cent relative reduction in multi-expert composition error or a 3-point absolute improvement, while remaining within 1 per cent of the top-k baseline on single-expert tasks and within 10 per cent of its throughput.'' \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}SMM+17{]}; {[}FZS22{]}; categorical approaches to architectures {[}GLD+24; Mah25{]}. \begin{RSbar} \RSfield{Solved when}A trainable coverage router with a finite-difference-checked backward pass, and the N7 comparison executed under the registered protocol, reporting confirmation or one of the registered null outcomes. \end{RSbar} \RSfield{Literature check (28 October 2026)}Many routing variants for mixture-of-experts were found; none uses sheaf-theoretic coverage routing with these controls. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/22}{Issue 22} of the repository. \par \RSproblem{problem-23}{A defence against a globally coherent falsehood}{machine · programme level}{A defence against a globally coherent falsehood} \RSfield{Thesis}Thesis 5 (Report failure; abstain without evidence). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, §1.2.5, p.~22. \RSfield{Status in the source}open (``we have no structural defence to propose''). \begin{RSbar} \RSfield{Statement}``Descent verification provably catches local inconsistency. Against a globally coherent falsehood it offers nothing, and we have no structural defence to propose.'' Give a verification method that detects a stated class of globally coherent falsehoods, or prove that no verifier with access only to stated information can do so. \end{RSbar} \RSfield{What the source establishes}The source proves the local guarantee and records the global gap as one of ``The five things we are least sure of''; Part VI of {[}S02{]} discusses reward hacking at length without proposing a defence. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}SHKK22{]}; selective prediction {[}EW10{]}; {[}FKKG24{]}. \begin{RSbar} \RSfield{Solved when}Either a method with a theorem stating which globally coherent falsehoods it detects and at what cost, evaluated on a published adversarial benchmark, or an impossibility theorem for a stated class of verifiers. \end{RSbar} \RSfield{Literature check (28 October 2026)}Consistency- and verification-based hallucination detection was found; no structural defence or impossibility theorem for globally coherent falsehoods was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/23}{Issue 23} of the repository. \par \RSproblem{problem-24}{Compiled-to-streaming descent stability}{mathematical · research level}{Compiled-to-streaming descent stability} \RSfield{Thesis}Thesis 4 (Attention as descent). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Conjecture 2.2.15, p.~104. \RSfield{Status in the source}D/OPEN. \begin{RSbar} \RSfield{Statement}Consider a session tower of finite certified sites and solid-valued states \((\mathcal C_n,P_n,F_n)_{n\ge 0}\) with the site maps of {[}S02, §2.2{]}. Conjecture 2.2.15: ``If the cd-certificates are uniformly compatible under these site morphisms, the density bound is uniform, the coefficient towers satisfy the required derived-limit vanishing condition, and the finite probe systems form a conservative filtered family, then the limit state satisfies Nisnevich descent with solid condensed coefficients.'' Prove or refute it. \end{RSbar} \RSfield{What the source establishes}``The hypotheses are not discharged.'' The source explains which hypotheses fail in practice --- ``Uniform density generally fails when new maximal atoms are added; derived-limit vanishing is not certified by the runtime; and no conservative finite probe family has been proved for arbitrary state classes'' --- and that ``The conjecture therefore cannot be used to upgrade stagewise FINITE-ONLY certificates to a session-wide theorem.'' \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}Nisnevich descent {[}MV99{]}; condensed and solid mathematics {[}Sch19{]}; {[}Lur09{]}. \begin{RSbar} \RSfield{Solved when}A proof of the conjecture as stated, or a counterexample tower satisfying the four hypotheses whose limit state fails Nisnevich descent. \end{RSbar} \RSfield{Literature check (28 October 2026)}Work on descent for condensed and syntomic coefficients was found; no result on limits of towers of finite certified sites was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/24}{Issue 24} of the repository. \par \RSproblem{problem-25}{The Beck--Chevalley square 12.6.3}{mathematical · research level}{The Beck–Chevalley square 12.6.3} \RSfield{Thesis}Thesis 4 (Attention as descent). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, §2.4.4, pp.~157--158 (Proposition 2.4.24, Theorem 2.4.25). \RSfield{Status in the source}globally open. \begin{RSbar} \RSfield{Statement}For a context family \(\mathrm{Rep}\colon\mathcal C_{\mathrm{ref}}\to\mathrm{Cat}_\infty\), transport along refinements is coherent by straightening, but ``Straightening supplies no Beck--Chevalley comparison for that square'' formed by a refinement arrow and a cover restriction, and Proposition 2.4.24 shows that ``The gap is real even in discrete categories.'' Characterise the families and covers for which the comparison \(\rho_V\circ r_!\Rightarrow (r_i)_!\circ\rho_U\) exists, is invertible, and satisfies the identity, composition and overlap coherence laws, so that the conditional Theorem 2.4.25 applies. \end{RSbar} \RSfield{What the source establishes}Theorem 2.4.25 proves coverwise transport under exactly these hypotheses, and Chapter 13.5 audits finite fixtures; the source calls this ``a scope restriction and conditional local closure, not a general solution.'' ``The monograph does not close the gap globally.'' \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}Lur09{]}; {[}MM94{]}; {[}SGA4{]}. \begin{RSbar} \RSfield{Solved when}A theorem giving necessary and sufficient conditions, in a stated generality, for the comparison of Theorem 2.4.25 to exist with its coherences, or a proof that no condition weaker than the hypothesis itself suffices in that generality. \end{RSbar} \RSfield{Literature check (28 October 2026)}Recent work on Beck--Chevalley fibrations concerns ambidexterity and norm squares; no result on refinement--cover squares of this kind was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/25}{Issue 25} of the repository. \par \RSproblem{problem-26}{Sharp accumulation bounds for equivariance defects}{mathematical · research level}{Sharp accumulation bounds for equivariance defects} \RSfield{Thesis}Thesis 6 (A chain of non-implications). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Question 11.11.18, p.~2259. \RSfield{Status in the source}X (open question). \begin{RSbar} \RSfield{Statement}The accumulation bound of {[}S02, Theorem 11.9.28{]} for the equivariance defects of successive layers is tight in the worst case, but its use as a certificate needs a lower bound on output norms that is not available. Question 11.11.18 asks: ``Is there a class of architectures with certified lower norm control on which a usable ratio of bound to witness is O(1)? Failing that, is there a sharper bound that tracks the direction of the equivariance defect rather than only its magnitude, for instance by carrying a covariance rather than a scalar?'' \end{RSbar} \RSfield{What the source establishes}``Theorem 11.9.28 is tight in the worst case, with both of its constants attained.'' Without the lower-norm premise the gate leaves the claim open: ``A witness may still falsify a claim but cannot replace the missing certificate.'' The source suggests, without attempting it, that defects may add in quadrature under a randomness assumption. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}Error accumulation in composed computations {[}Hig02{]}; equivariance in deep learning {[}BBCV21{]}. \begin{RSbar} \RSfield{Solved when}Either a class of architectures with certified lower norm control on which the ratio of bound to witness is proved O(1), or a direction-sensitive bound strictly sharper than Theorem 11.9.28 on a stated class, with proof. \end{RSbar} \RSfield{Literature check (28 October 2026)}No result of this form for equivariance defects was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/26}{Issue 26} of the repository. \par \RSproblem{problem-27}{Local dynamics of the restriction-frame locus}{mathematical · research level}{Local dynamics of the restriction-frame locus} \RSfield{Thesis}Thesis 4 (Attention as descent). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Table 13.16.13, entry O8, p.~3174. \RSfield{Status in the source}OPEN. \begin{RSbar} \RSfield{Statement}Determine ``whether the head-indexed restriction-frame embedded locus is attracting, repelling or a saddle under unfrozen frame dynamics'', the open entry O8 of the unproved register of {[}S02, Part P{]}. \end{RSbar} \RSfield{What the source establishes}Proposition 13.11.46 proves a parameter-specific departure from the locus and refutes universal invariance, but does not classify the local dynamics. The register names the missing tool: ``a Lyapunov, centre-manifold or other local-dynamics argument for the frame manifold''. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}Car81{]}; optimisation on matrix manifolds {[}AMS08{]}. \begin{RSbar} \RSfield{Solved when}A proof classifying the locus as attracting, repelling or a saddle (possibly depending on stated parameters) under the dynamics of Chapter 13.11. \end{RSbar} \RSfield{Literature check (28 October 2026)}Work on Stiefel-manifold training dynamics was found; no classification of this locus was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/27}{Issue 27} of the repository. \par \RSproblem{problem-28}{A base-change bound for the descent solve}{mathematical · research level}{A base-change bound for the descent solve} \RSfield{Thesis}Thesis 4 (Attention as descent). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Table 13.16.13, entry O14, pp.~3174--3175. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}Prove ``a base-change bound for the descent solve'': a bound relating the outputs of the descent solve of {[}S02, Ch. 13.10{]} at two bases, on which every cross-base stability statement of the book depends. \end{RSbar} \RSfield{What the source establishes}The register records where the argument stops: ``no bound relates the solve at two bases; the available Jacobian square measures a different quantity''. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}Spectral theory of sheaf Laplacians {[}HG19{]}; perturbation bounds {[}Hig02{]}. \begin{RSbar} \RSfield{Solved when}A proved bound, with explicit constants, on the difference of the descent solves at two bases in terms of a stated distance between the bases, or a family of examples showing that no such bound holds. \end{RSbar} \RSfield{Literature check (28 October 2026)}Work on sheaf diffusion and its stability was found; no base-change bound for this solve was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/28}{Issue 28} of the repository. \par \RSproblem{problem-29}{The training-to-serving deviation}{mathematical · research level}{The training-to-serving deviation} \RSfield{Thesis}Thesis 6 (A chain of non-implications). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Table 13.16.13, entry O16, pp.~3174--3175. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}Prove that ``the training-to-serving deviation is bounded'' for the forward map of {[}S02, Ch. 13.10--13.11{]}, or remove the failure: the register asks for ``a proved bound, or a tie-break that removes the failure''. \end{RSbar} \RSfield{What the source establishes}Bitwise equality between training and serving is proved under stated contracts and fails outside them: ``equality fails through the tie-break under rounding; no bound on the output difference is proved''. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}IEEE19{]}; {[}Hig02{]}; deterministic inference across parallel configurations {[}ZDY+25{]}. \begin{RSbar} \RSfield{Solved when}A proved bound on the output difference between training and serving under the rounding model of Chapter 13.11, or a tie-break rule with a proof that it restores equality. \end{RSbar} \RSfield{Literature check (28 October 2026)}Engineering work on deterministic inference was found {[}ZDY+25{]}; no proved bound for this forward map was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/29}{Issue 29} of the repository. \par \RSproblem{problem-30}{Monotone refinement budgets}{mathematical · research level}{Monotone refinement budgets} \RSfield{Thesis}Thesis 5 (Report failure; abstain without evidence). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Question 11.11.19, p.~2259. \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{23} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}The recomputed refinement budget of {[}S02, Proposition 11.9.20{]} is not monotone along refinement. Question 11.11.19: ``Is there a natural class of covers --- closed under the refinements one actually performs --- on which some useful instrument is monotone?'' The source names two candidate classes, nerve-preserving refinements and split-only refinements. \end{RSbar} \RSfield{What the source establishes}For both candidates the needed facts are unproved, and ``No such theorem is currently available.'' A proved monotone direction would let the diameter of a totally ordered class be read at its endpoints. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}Cellular sheaves and their cohomology {[}HG19{]}. \begin{RSbar} \RSfield{Solved when}A theorem identifying such a class and an instrument monotone on it, or a proof that each of the two named classes admits no useful monotone instrument. \end{RSbar} \RSfield{Literature check (28 October 2026)}No result on monotone instruments under cover refinement was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/30}{Issue 30} of the repository. \par \RSproblem{problem-31}{How many ambiguity axes are there?}{mathematical · research level}{How many ambiguity axes are there?} \RSfield{Thesis}Thesis 2 (Status is part of the type). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Question 11.11.20, p.~2259. \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{23} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}The indeterminacy calculus of {[}S02, Ch. 11.9{]} separates the ways a reported number can depend on arbitrary choices. ``Chapter 11.9 opened with three and closed with four: the comparison link of Definition 11.9.42 was found only after the first three had been written up, which is evidence that the enumeration is incomplete.'' Determine whether routing tie-breaking is a fifth axis with useful exact invariants, and whether the enumeration is complete. \end{RSbar} \RSfield{What the source establishes}``Whether tie rules form a separate typed transformation family with useful exact invariants remains open; no fifth calculus is asserted.'' Simplicial orientation and numerical precision are examined and dismissed with reasons. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}Gauge and presentation invariance {[}BBCV21{]}; {[}HG19{]}. \begin{RSbar} \RSfield{Solved when}A typed transformation family for tie rules with its exact invariants, or a proof that tie rules reduce to the four existing axes; a completeness theorem for a stated class of instruments also solves the problem. \end{RSbar} \RSfield{Literature check (28 October 2026)}No result on this classification was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/31}{Issue 31} of the repository. \par \RSproblem{problem-32}{Second-order disagreement without engineering}{mathematical · research level}{Second-order disagreement without engineering} \RSfield{Thesis}Thesis 5 (Report failure; abstain without evidence). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, §1.1.13, p.~15; §1.2.5, p.~22; §9.1.7, p.~1766. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}``On a graph, and under standard top-k routing, H2 vanishes identically.'' The degree-two (gerbe) theory of disagreement among experts is therefore vacuous unless the cover is built for it: ``The minimal non-vacuous configuration is four experts arranged as ∂Δ3, and it must be engineered deliberately.'' Determine whether covers produced by a data-driven routing or cover-construction procedure, on natural tasks, carry non-zero second cohomology with the coefficient data of {[}S02{]}. \end{RSbar} \RSfield{What the source establishes}The source proves the vanishing results and warns that ``engineering a structure into existence in order to measure it is a move that deserves suspicion.'' A gerbe diagnostic is ``vacuous unless the cover has a deliberate, data-justified sparse nerve with genuine two-dimensional cycles and explicitly defined coefficient data.'' \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}Gir71{]}; {[}HG19{]}. \begin{RSbar} \RSfield{Solved when}A procedure, not tuned to produce two-cycles, whose covers on a published natural task carry a certified non-zero class in degree two; or a theorem that a stated class of procedures always yields vanishing second cohomology. \end{RSbar} \RSfield{Literature check (28 October 2026)}No result on second cohomology of routing nerves was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/32}{Issue 32} of the repository. \par \RSproblem{problem-33}{Formalizing uniform circuit classes}{formalization · research level}{Formalizing uniform circuit classes} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Open Problem 13.15.B, p.~3135; cut ledger, Table 13.15.7, p.~3133. \RSfield{Status in the source}OPEN. \begin{RSbar} \RSfield{Statement}``Formalise L-uniform circuit families and the AC\(^0\) many-one reduction convention of Definition 2.14.5 to the point where clauses 4 and 5 of Theorem 13.13.24 become statable, and decide whether the Barrington construction of Chapter 2.14 is within reach of a proof term.'' \end{RSbar} \RSfield{What the source establishes}The source's separation results use L-uniform circuit classes and Barrington's theorem on paper; the machine-checked part stops at statements, and the cut ledger records that ``a Barrington formalisation is a project in itself''. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}Bar89{]}; {[}BIS90{]}; a recent Lean formalisation of the non-uniform PARITY lower bound {[}Wes26{]}. \begin{RSbar} \RSfield{Solved when}A Lean (or other assistant) library defining L-uniform circuit families and AC\(^0\) many-one reductions in which clauses 4 and 5 of Theorem 13.13.24 are stated, together with either a formal proof of Barrington's theorem or a documented estimate of what such a proof requires. \end{RSbar} \RSfield{Literature check (28 October 2026)}The non-uniform PARITY lower bound has been formalised in Lean {[}Wes26{]}; uniformity and Barrington's theorem were not found in mathlib or in formal-conjectures (GitHub code search). \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/33}{Issue 33} of the repository. \par \RSproblem{problem-34}{A second kernel}{formalization · entry level}{A second kernel} \RSfield{Thesis}Thesis 6 (A chain of non-implications). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Open Problem 13.15.D, p.~3135. \RSfield{Status in the source}OPEN / D. \begin{RSbar} \RSfield{Statement}``Establish whether an independent type-checker covers the features used by the 13.11 and 13.13 developments, and if so make REPLAYED require two kernels rather than two machines.'' Independent checkers for Lean 4 now exist {[}Car24; nanoda{]}; the problem is to elaborate the Lean declarations of {[}S02, Table 13.15.1{]} at a pinned toolchain and replay them under Lean's kernel and under an independent checker. \end{RSbar} \RSfield{What the source establishes}In the release no declaration was elaborated, and the source says of its replay status: ``The present definition of REPLAYED is weaker than the name suggests, and this is stated rather than hidden.'' \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}BW05{]}; {[}MU21{]}; {[}Car24{]}; {[}nanoda{]}. \begin{RSbar} \RSfield{Solved when}The declarations elaborated at a pinned toolchain and replayed by two independent kernels, with a report of the features used and of any declaration that one kernel rejects. \end{RSbar} \RSfield{Literature check (28 October 2026)}Independent Lean 4 checkers were found {[}Car24; nanoda{]}; the Lean 4 repository contains a replay checker and an export format (src/LeanChecker.lean, src/Lean\-Ex\-port; GitHub code search, leanprover/lean4). No replay of these declarations was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/34}{Issue 34} of the repository. \par \RSproblem{problem-35}{The computational-univalence bridge}{formalization · programme level}{The computational-univalence bridge} \RSfield{Thesis}Thesis 4 (Attention as descent). \RSfield{Source}\emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, Hypothesis 4.7.26, p.~1103. \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{23} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}Build the checker of Hypothesis CU-MJ of {[}S02{]}: ``There exists an approved external checker that: 1. represents proof-relevant paths and a univalent universe independently of Lean equality; 2. computes coercion along equivalences using cubical composition or an equivalent certified mechanism; 3. checks the higher coherences required by the transported family; 4. emits a replayable term rather than a Boolean success flag;'' and 5. binds that term to the canonical target, equivalence, site, cover, universe and checker of the justification being transported. \end{RSbar} \RSfield{What the source establishes}``No such integrated component is supplied by this chapter, so CU-MJ is graded X.'' Every theorem that assumes it is conditional; the finite branch of the chapter does not need it. \RSfield{Proposed by}{[}S02{]}. \RSfield{Background}{[}CCHM18{]}; {[}VMA21{]}; {[}Uni13{]}. \begin{RSbar} \RSfield{Solved when}A checker satisfying the five clauses, and one transported justification from {[}S02, Ch. 4.7{]} checked end to end with its replayable term published. \end{RSbar} \RSfield{Literature check (28 October 2026)}Cubical proof assistants and proof-transfer tools exist {[}CCHM18; VMA21{]}; no checker bound to Lean targets in the sense of clause 5 was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/35}{Issue 35} of the repository. \par \RSpart{part-2}{Part II}{The Five Research Subjects} Each of the five works of this part takes a named conjecture or programme as its research subject and records what its method establishes about it. The problems below are drawn from those records. None of them is the named conjecture, and a solution of any of them would not by itself prove one. \subsection*{\emph{Arithmetic Spectral Descent} (research subject: the Riemann Hypothesis)}\label{arithmetic-spectral-descent-research-subject-the-riemann-hypothesis}\def\RSbmlevel{3} \RSproblem{problem-36}{Polarization of a cyclotomic spectrum}{mathematical · research level}{Polarization of a cyclotomic spectrum} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{Arithmetic Spectral Descent} {[}S03{]}, Problem 24.18, p.~539 (restated as Problems 29.8 and 30.16); Criterion 57.5, p.~1145. \RSfield{Status in the source}O (open). \begin{RSbar} \RSfield{Statement}Define a polarization of a cyclotomic spectrum: extra data on Real topological Hochschild homology (THR) \((\mathrm{THR}(R),O(2),\{\varphi^{\mathbb R}_p\})\), generalising an ample class or a Kähler form, such that (i) it induces a real quadratic form on \(\pi_*(\mathrm{THR}(R)^{hO(2)})\) through a trace state; (ii) ``the form is definite on primitive parts with respect to a Lefschetz decomposition''; and (iii) for \(X\) smooth projective over \(\mathbb F_q\) with an ample line bundle, ``it recovers the Hodge index theorem on crystalline cohomology / the positivity underlying the Weil conjectures.'' \end{RSbar} \RSfield{What the source establishes}The source explains why (iii) is already delicate: crystalline cohomology carries no real structure, and the Katz--Messing comparison transports eigenvalues but not the positivity mechanism. Criterion 57.5 fixes a test: a proposed polarization solves the problem only if, applied to the topological Hochschild homology \(\mathrm{THH}(C)\) of a curve \(C\) over \(\mathbb F_q\) of genus \(g\ge1\), it proves \(|\alpha_i|=\sqrt q\) for the inverse roots of the numerator of \(Z(C,t)\) without invoking Weil's theorem, Riemann--Roch on \(C\times C\) or the Hodge index theorem. \RSfield{Proposed by}{[}S03{]}. \RSfield{Background}{[}NS18{]}; {[}DMPR21{]}; {[}Del74{]}. \begin{RSbar} \RSfield{Solved when}A definition satisfying (i)--(iii), with the test of Criterion 57.5 passed for every curve over a finite field. The bound \(|\alpha_i|=\sqrt q\) is a theorem (Weil); the problem is to obtain it from the new structure. \end{RSbar} \RSfield{Literature check (28 October 2026)}Work on Real topological Hochschild homology and its cyclotomic structure was found {[}DMPR21{]}; no notion of polarization of the required kind was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/36}{Issue 36} of the repository. \par \RSproblem{problem-37}{Construction Problem A1 on the syntomic stack}{mathematical · research level}{Construction Problem A1 on the syntomic stack} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{Arithmetic Spectral Descent} {[}S03{]}, Problem 22.9, p.~483. \RSfield{Status in the source} \begin{enumerate} \def\labelenumi{\Alph{enumi}.} \setcounter{enumi}{14} \tightlist \item \end{enumerate} \begin{RSbar} \RSfield{Statement}Construct, on quasi-coherent sheaves on the syntomic stack \(\mathbb Z_p^{\mathrm{syn}}\) (equivalently on \(F\)-gauges over \(\mathbb Z_p\)), a \(\mathbb C\)-linear endomorphism \(\Theta\) of the underlying object after \(\otimes_{W,\iota}\mathbb C\) such that (A1.1) on the Hodge--Tate locus \(\Theta=-\tfrac{2\pi i}{\log q}\Theta_{\mathrm{Sen}}\) for objects pulled back from \(\mathbb F_q\); (A1.2) \(q^\Theta=\mathrm{Fr}_q^*\) for \(F\)-gauges coming from smooth proper \(X/\mathbb F_q\); (A1.3) \(\Theta\) is \(\mathbb C\)-linear, which ``rules out semilinear operators''; and (A1.4) the regularized determinant \(\det_\infty(s-\Theta)\) on motivic cohomology converges and equals \(\zeta(X,s)\). \end{RSbar} \RSfield{What the source establishes}The source isolates the difficulty in (A1.3): the Frobenius part of \(\Theta\) is semilinear over \(W\), and over \(\mathbb Z_p\) no power of \(\varphi\) is \(W\)-linear. ``The syntomic stack exists, but the operator on it does not---yet.'' \RSfield{Proposed by}{[}S03{]}. \RSfield{Background}{[}BS22{]}; {[}BL22{]}; {[}Dri20{]}. \begin{RSbar} \RSfield{Solved when}A construction satisfying (A1.1)--(A1.4), or a proof that no endomorphism with (A1.1)--(A1.3) exists. \end{RSbar} \RSfield{Literature check (28 October 2026)}The Sen operator on the Hodge--Tate stack is known {[}BL22; Dri20{]}; no operator with (A1.1)--(A1.4) was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/37}{Issue 37} of the repository. \par \RSproblem{problem-38}{Archimedean Frobenius from quaternionic THH}{mathematical · research level}{Archimedean Frobenius from quaternionic THH} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{Arithmetic Spectral Descent} {[}S03{]}, Problem 28.13, p.~604; Construction 28.14, p.~605. \RSfield{Status in the source}O (first half answered since; see the literature check). \begin{RSbar} \RSfield{Statement}Problem 28.13 of {[}S03{]} asks two questions. The first --- whether there is ``a lift of THH to genuine Pin(2)-spectra rather than O(2)-spectra'' --- has been answered: quaternionic topological Hochschild homology THQ, defined for rings with twisted \(C_4\)-action, carries a \(\mathrm{Pin}(2)\)-action {[}AMP26{]}. The second remains: is its \(\mathrm{Pin}(2)\)-homotopy fixed-point theory ``the correct 𝜑∞ for symplectically self-dual motives, with 𝑂(2) handling the orthogonal ones?'' Concretely, determine whether \(\mathrm{THQ}(R)^{h\mathrm{Pin}(2)}\) carries an operator \(\Theta_\infty\) satisfying the analogue of requirement (C′1) of Construction 28.14 --- its half-line spectrum, with Hodge multiplicities, gives the archimedean local factors of symplectically self-dual motives by \(\det_\infty((s-\Theta_\infty)/2\pi)\). \end{RSbar} \RSfield{What the source establishes}The source calls the question ``a well-posed question in equivariant stable homotopy theory, independent of RH'', and states that ``No existing construction is known''; that statement is corrected here (it is recorded in the errata of the repository). Construction 28.14 lists the requirements (C′1)--(C′4) for the orthogonal case. \RSfield{Proposed by}{[}S03{]}. \RSfield{Background}{[}AMP26{]}; {[}DMPR21{]}; {[}Man16{]}; {[}NS18{]}. \begin{RSbar} \RSfield{Solved when}An operator on \(\mathrm{THQ}(R)^{h\mathrm{Pin}(2)}\) for a stated class of rings with the required structure, with a proof of the analogue of (C′1) for symplectically self-dual motives in that class; or a proof that no natural operator can satisfy it. \end{RSbar} \RSfield{Literature check (28 October 2026)}Found: Angelini-Knoll, Merling and Péroux construct THQ with its Pin(2)-action (arXiv:2409.18187, 2024; Adv. Math. 2026) {[}AMP26{]}. This answers the first question of Problem 28.13; no work on the second was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/38}{Issue 38} of the repository. \par \RSproblem{problem-39}{A certified inertia for the pole-removed Weil form}{machine · entry level}{A certified inertia for the pole-removed Weil form} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{Arithmetic Spectral Descent} {[}S03{]}, Criterion 58.9 (falsification predicate F2), p.~1169; Proposition 46.5 and Remark 46.13, pp.~xxxv, 919. \RSfield{Status in the source}E (finite measurement) / O. \begin{RSbar} \RSfield{Statement}For sixty-three cubic-spline test spaces \(V_{T,N}\) (\(0.15\le T\le 3\), \(4\le N\le 64\)) the source measured, in floating point with tolerance \(10^{-9}\), that the pole-removed Weil form \(B_N=W_N-P_N\) has inertia \((N-1,1)\). Certify this measurement in interval or exact arithmetic for each configuration --- certify \(N-1\) positive eigenvalues and exhibit a vector \(z\) with a certified enclosure of \(B_N(z,z)<0\) --- or show for some configuration that the certified inertia differs, which is falsification predicate F2 of {[}S03, Criterion 58.9{]}. \end{RSbar} \RSfield{What the source establishes}Under RH the full Weil form is positive semidefinite and \(n_-(B_N)\le1\) (Corollary 46.11); the lower bound \(n_-(B_N)\ge1\) is not proved conditionally or otherwise (Warning 46.12). The measurement is finite evidence: ``What the data exclude is a large second negative direction. What they do not exclude is a small one.'' F2 asks for ``the computation certified in interval arithmetic''. \RSfield{Proposed by}{[}S03{]}. \RSfield{Background}Weil positivity at the archimedean place {[}CC21{]}; interval arithmetic {[}Joh17{]}; certified computation of zeta zeros {[}PT21{]}; certification for other finite truncations of the Weil form {[}Gro26{]}. \begin{RSbar} \RSfield{Solved when}Certified inertia for all sixty-three configurations of Proposition 46.5, with the code and the enclosures published; a configuration whose certified inertia is not \((N-1,1)\) also solves the problem, by firing F2. The result is a statement about finitely many matrices; it is not evidence for or against RH. \end{RSbar} \RSfield{Literature check (28 October 2026)}A certification rule and an interval factorization for the Galerkin truncations of the Weil quadratic form of Connes, van Suijlekom, Consani and Moscovici were found {[}Gro26{]}; no certified computation of the inertia of the Gram matrices of these sixty-three test spaces was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/39}{Issue 39} of the repository. \par \subsection*{\emph{Fractured Adelic Geometry} (research subject: the conjecture of Birch and Swinnerton-Dyer)}\label{fractured-adelic-geometry-research-subject-the-conjecture-of-birch-and-swinnerton-dyer}\def\RSbmlevel{3} \RSproblem{problem-40}{The Tamagawa factor as a local term}{mathematical · research level}{The Tamagawa factor as a local term} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{Fractured Adelic Geometry} {[}S04{]}, Problem 22.7.1, p.~173; §2.8.1, p.~19; §56.3, p.~437. \RSfield{Status in the source}OPEN. \begin{RSbar} \RSfield{Statement}The source proposes three constructions of the bad-prime term \(c_p\) of the conjecture of Birch and Swinnerton-Dyer: a vertical intersection multiplicity on the arithmetic surface, a Lefschetz--Verdier term of a fixed-point stack, and a determinant defect of the prismatic/Néron component lattice. Problem 22.7.1: ``Construct the three local objects just described and prove that each has Euler characteristic c\_p, compatibly with change of model, Frobenius action, and the integral orientation of the fundamental line.'' \end{RSbar} \RSfield{What the source establishes}The identification of \(c_p\) as a Lefschetz--Verdier local term is listed among the book's novelties, and the source fixes the test: ``This is a particularly useful falsification test. Tate's algorithm gives c\_p independently for every database curve. If a proposed prismatic or fixed-point formula disagrees even once, that local construction is wrong. No appeal to BSD can repair such a disagreement.'' The book lists this among the items that are ``testable now, independently of BSD.'' \RSfield{Proposed by}{[}S04{]}. \RSfield{Background}{[}Tat75{]}; {[}BK90{]}; {[}BS22{]}. \begin{RSbar} \RSfield{Solved when}The three constructions with proofs that each has Euler characteristic \(c_p\) with the stated compatibilities; or a curve and a prime at which a proposed construction disagrees with Tate's algorithm, which refutes that construction. The problem concerns local terms and does not bear on the truth of BSD. \end{RSbar} \RSfield{Literature check (28 October 2026)}No prismatic or fixed-point formula for the Tamagawa factor was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/40}{Issue 40} of the repository. \par \RSproblem{problem-41}{The arithmetic flow}{mathematical · programme level}{The arithmetic flow} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{Fractured Adelic Geometry} {[}S04{]}, Problem 53.2.4 (Obstruction IV), p.~416; Problem 4.5.1, p.~37. \RSfield{Status in the source}OPEN. \begin{RSbar} \RSfield{Statement}Construct a strongly continuous flow on a cohomology theory over \(\operatorname{Spec}\mathbb Z\) whose primitive closed orbits are the primes, the orbit at \(p\) having length \(\log p\), with no spurious orbits and with a generator satisfying the weight adjunction. In the form of Problem 4.5.1: a foliated or laminated space with a flow and a leafwise cohomology admitting duality and regularized determinants, whose Lefschetz trace formula is the explicit formula. \end{RSbar} \RSfield{What the source establishes}``The flow Φ𝑡 is postulated, not built. No ℝ≥0-action has ever been constructed on any cohomology theory over Specℤ whose primitive closed orbits are the primes with lengths log p''. For Problem 4.5.1: ``No object satisfying these requirements is presently known.'' The cyclotomic structure of THH supplies \(\psi_p\) at each prime; the interpolation to a continuous action is missing. \RSfield{Proposed by}Deninger {[}Den98{]}; restated, with the source's axioms, in {[}S04{]}. \RSfield{Background}{[}Den98{]}; {[}NS18{]}. \begin{RSbar} \RSfield{Solved when}A construction with the stated properties, or a no-go theorem showing that no \(\mathbb R_{\ge0}\)-action of the required kind exists on any cohomology of \(\operatorname{Spec}\mathbb Z\) (item (ii) of the refutation list of {[}S04, §2.8.1{]}). \end{RSbar} \RSfield{Literature check (28 October 2026)}Trace formulas for foliated flows and regularized-determinant formulas in Deninger's framework were found; no construction over Spec ℤ was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/41}{Issue 41} of the repository. \par \RSproblem{problem-42}{Sub-conductor rank detection}{mathematical · research level}{Sub-conductor rank detection} \RSfield{Thesis}Thesis 12 (Judge a method by its open ledger). \RSfield{Source}\emph{Fractured Adelic Geometry} {[}S04{]}, Question 46.2.1, p.~354. \RSfield{Status in the source}OPEN. \begin{RSbar} \RSfield{Statement}Does there exist a natural family \(\mathcal F_X\) of elliptic curves, a function \(P(X)=X^{o(1)}\), and explicit statistics \(S_X\) depending only on \(\{a_p(E): p\le P(X)\}\), such that the conditional laws of \(S_X\) for analytic rank \(0\), \(1\) and at least \(2\) have distinct non-degenerate limits after the root number and all known local confounders are matched? \end{RSbar} \RSfield{What the source establishes}The source explains the clause on confounders: ``The matching clause matters. Without it, a classifier may merely learn the functional-equation sign or a database convention.'' Either answer is informative: ``A positive answer would ask for a new family trace formula; a negative answer would also be informative by locating the finite-sample origin of the observed signal.'' \RSfield{Proposed by}{[}S04{]}. \RSfield{Background}{[}HLOP22{]}; {[}Zub23{]}; {[}BKLPR15{]}; neural rank prediction from Frobenius traces {[}BCD+26{]}. \begin{RSbar} \RSfield{Solved when}A theorem establishing distinct limits for a stated family and statistic with \(P(X)=X^{o(1)}\), or a theorem that no statistic of this kind separates the ranks after matching. \end{RSbar} \RSfield{Literature check (28 October 2026)}Machine-learning prediction of analytic rank from Frobenius traces has been reported with high accuracy {[}BCD+26{]} and murmurations studied {[}HLOP22; Zub23{]}; no theorem of the requested form, with the matching clause, was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/42}{Issue 42} of the repository. \par \RSproblem{problem-43}{Murmurations from the flow: a falsification test}{machine · entry level}{Murmurations from the flow: a falsification test} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{Fractured Adelic Geometry} {[}S04{]}, Conjecture 36.4.6, pp.~276--277. \RSfield{Status in the source}OPEN (a falsifiable prediction). \begin{RSbar} \RSfield{Statement}If the framework of {[}S04{]} is correct, the murmuration density arises as a transition term in its Lefschetz--Verdier localisation, and three computable predictions follow: (i) \(y=p/N\) is the natural coordinate, and no other combination of \(p\) and \(N\) appears in the leading term; (ii) the density for elliptic curves, if it exists, has the same oscillation frequencies as the modular-form density \(M_2\); (iii) the rank-conditioned densities are governed by the same density with the root number replaced by the Selmer fixed-point class. Carry out the tests. \end{RSbar} \RSfield{What the source establishes}``Each clause is falsifiable by computation. Clause (i) fails if any family shows a leading term depending on p and N other than through p/N; clause (ii) fails if the observed elliptic-curve frequencies differ from those of M2.'' The protocol is in Chapter 55. \RSfield{Proposed by}{[}S04{]}. \RSfield{Background}{[}HLOP22{]}; {[}Zub23{]}; {[}SS25{]}; {[}Cow24{]}. \begin{RSbar} \RSfield{Solved when}The tests of clauses (i) and (ii) carried out under the protocol of {[}S04, Ch. 55{]} against the densities of {[}Zub23{]} and {[}SS25{]}, with data and code published and the outcome reported in either direction; clause (iii) when the Selmer class is computable. \end{RSbar} \RSfield{Literature check (28 October 2026)}A conjectural explicit murmuration density for elliptic curves ordered by height has been given {[}SS25{]}, and murmurations have been derived from ratios conjectures {[}Cow24{]}; these supply what clause (ii) is tested against. No test of the three clauses was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/43}{Issue 43} of the repository. \par \subsection*{\emph{The Archimedean Prism} (research subject: the Hodge conjecture)}\label{the-archimedean-prism-research-subject-the-hodge-conjecture}\def\RSbmlevel{3} \RSproblem{problem-44}{The Hodge decomposition in Lean}{formalization · programme level}{The Hodge decomposition in Lean} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{The Archimedean Prism} {[}S05{]}, Problem 71.11.1, p.~1027; dossier, p.~1034; The five volumes, p.~xv. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}``Formalise the Hodge decomposition for compact Kähler manifolds in Lean 4 with mathlib, the single largest absent prerequisite identified in Chapter 64.'' \end{RSbar} \RSfield{What the source establishes}The source records the verdict that ``the Hodge conjecture cannot presently even be stated in Lean 4 with mathlib'', and estimates the formalisation ``as an effort on the order of the Liquid Tensor Experiment.'' Its dossier limits what success means: ``Success would enable formal statements of the later conjectures; it would prove none of them by itself.'' Problem 71.11.2 (Chow groups and the cycle class map) is the other missing prerequisite. \RSfield{Proposed by}{[}S05{]}. \RSfield{Background}{[}Voi02b{]}; {[}mC20{]}; {[}Sch22{]}. \begin{RSbar} \RSfield{Solved when}A Lean 4 development, accepted into Mathlib or released as a library building against it, that defines compact Kähler manifolds and proves the Hodge decomposition of their de Rham cohomology. \end{RSbar} \RSfield{Literature check (28 October 2026)}GitHub code search (2026-10-28) found in mathlib a Hodge star on exterior powers and algebraic Kähler differentials, but no Kähler manifolds and no Hodge decomposition; formal-conjectures contains no Hodge-theoretic statement. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/44}{Issue 44} of the repository. \par \RSproblem{problem-45}{No δ-structure on the archimedean prism}{mathematical · research level}{No δ-structure on the archimedean prism} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{The Archimedean Prism} {[}S05{]}, Problem 71.3.4, p.~1023; dossier, p.~1029. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}``Make precise, as a no-go theorem, the claim that the archimedean prism carries no 𝛿-structure and hence no literal Frobenius lift.'' \end{RSbar} \RSfield{What the source establishes}``Chapter 16 argues the analogy with prismatic cohomology is structural only; a no-go theorem would settle the point rather than assert it.'' The dossier sets the standard: ``A no-go theorem must quantify over all functorial candidate operations and identify an invariant they cannot satisfy; observing that the current construction lacks one is not enough.'' \RSfield{Proposed by}{[}S05{]}. \RSfield{Background}δ-rings {[}Joy85; Bui05{]}; prisms {[}BS22{]}. \begin{RSbar} \RSfield{Solved when}A theorem that quantifies over all functorial operations on the archimedean prism of {[}S05, Ch. 13--17{]} in a stated sense and proves that none is a δ-structure (or a Frobenius lift), by exhibiting an invariant that every such operation would have to satisfy and does not; or a functorial δ-structure, which would refute the claim. \end{RSbar} \RSfield{Literature check (28 October 2026)}No result on δ-structures for archimedean or real Hodge-theoretic analogues of prisms was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/45}{Issue 45} of the repository. \par \RSproblem{problem-46}{Independence of the twelve prism axioms}{mathematical · entry level}{Independence of the twelve prism axioms} \RSfield{Thesis}Thesis 12 (Judge a method by its open ledger). \RSfield{Source}\emph{The Archimedean Prism} {[}S05{]}, Problem 71.8.1, p.~1026; dossier, p.~1032. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}``Prove that the twelve prism axioms AP1--AP12 are logically independent by exhibiting, for each, a model satisfying the other eleven and failing it.'' \end{RSbar} \RSfield{What the source establishes}``Theorem 46.4.1 states the axioms; their independence is asserted but not demonstrated.'' The dossier: ``The twelve axioms are individually motivated, but motivation does not prove logical independence.'' \RSfield{Proposed by}{[}S05{]}. \RSfield{Background}Hodge theory {[}Del71{]}; the axioms and their sources are in {[}S05, Ch. 46{]}. \begin{RSbar} \RSfield{Solved when}Twelve models, the \(k\)-th satisfying every axiom except AP\(k\), each verified against the definitions of {[}S05, Ch. 46{]}; or a proof that one axiom follows from the others, which is a correction to the source. \end{RSbar} \RSfield{Literature check (28 October 2026)}No work on these axioms outside {[}S05{]} was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/46}{Issue 46} of the repository. \par \RSproblem{problem-47}{Descent beyond the polarized case}{mathematical · research level}{Descent beyond the polarized case} \RSfield{Thesis}Thesis 5 (Report failure; abstain without evidence). \RSfield{Source}\emph{The Archimedean Prism} {[}S05{]}, Problem 71.3.3, p.~1023; dossier, p.~1029. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}``Determine whether the descent theorem Theorem 15.4.2 holds for non-polarisable mixed Hodge structures, or exhibit the first obstruction to it.'' \end{RSbar} \RSfield{What the source establishes}In the source, ``descent along the prism is proved only in the polarised pure case.'' The dossier explains what changes: ``Nonpolarisable mixed structures have nonsemisimple extension data and weight filtrations that need not split; automorphism groupoids can cease to be reductive'', and notes that the answer may be a counterexample rather than an extension theorem. \RSfield{Proposed by}{[}S05{]}. \RSfield{Background}{[}Del71{]}; {[}Sch73{]}; {[}CDK95{]}. \begin{RSbar} \RSfield{Solved when}A proof of the descent theorem for non-polarisable mixed Hodge structures in a stated class, or an explicit mixed Hodge structure for which descent fails, with the obstruction identified. \end{RSbar} \RSfield{Literature check (28 October 2026)}No result on descent along the archimedean prism was found outside {[}S05{]}. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/47}{Issue 47} of the repository. \par \RSproblem{problem-48}{A prism reading of Voisin's counterexample}{mathematical · entry level}{A prism reading of Voisin’s counterexample} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{The Archimedean Prism} {[}S05{]}, Problem 71.6.6, p.~1025; dossier, p.~1031. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}``Compute the prism obstruction class of Voisin's 2002 Weil-torus counterexample and verify that it is exactly the projectivity obstruction, not a new one.'' \end{RSbar} \RSfield{What the source establishes}``Theorem 37.2.4 predicts the counterexample strikes at the projectivity step; an explicit computation would confirm the negation of falsifier F8.'' Voisin's examples {[}Voi02{]} show that the Hodge conjecture fails for compact Kähler manifolds that are not projective. \RSfield{Proposed by}{[}S05{]}. \RSfield{Background}{[}Voi02{]}; {[}Voi02b{]}. \begin{RSbar} \RSfield{Solved when}An explicit computation of the prism obstruction class for the tori of {[}Voi02{]}, showing that it is the projectivity obstruction of {[}S05, Theorem 37.2.4{]}; a computation showing that it is a different class refutes the prediction. \end{RSbar} \RSfield{Literature check (28 October 2026)}No prism-theoretic analysis of Voisin's examples was found outside {[}S05{]}. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/48}{Issue 48} of the repository. \par \subsection*{\emph{Strained Prismatic Geometry} (research subject: the \(abc\) conjecture)}\label{strained-prismatic-geometry-research-subject-the-abc-conjecture}\def\RSbmlevel{3} \RSproblem{problem-49}{Close the formal algebra leaf}{formalization · entry level}{Close the formal algebra leaf} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{Strained Prismatic Geometry} {[}S06{]}, Problem 62.1.5 (rank 2 of the critical path), p.~1275. \RSfield{Status in the source}OPEN. \begin{RSbar} \RSfield{Statement}With pinned Lean and Mathlib versions, ``Discharge PO-090 with definitions whose types separate a p-derivation from an ordinary derivation, proofs of the sum and product identities including p = 2, compatibility with the induced Frobenius lift, executable regression examples, no admitted declarations, and an axiom report containing only the approved logical foundations.'' \end{RSbar} \RSfield{What the source establishes}``This ranks second because the mathematics is known and the acceptance test is finite.'' Failures of tooling do not count against the mathematics: ``A library or elaboration failure is an engineering result, not a refutation.'' The repository gives the statements in Lean (formal/Grothendieck\-ian\-Prob\-lems/P49.lean). \RSfield{Proposed by}{[}S06{]}. \RSfield{Background}{[}Joy85{]}; {[}Bui05{]}; {[}BS22{]}; {[}mC20{]}. \begin{RSbar} \RSfield{Solved when}Proofs of the statements in formal/Grothendieck\-ian\-Prob\-lems/P49.lean, with no sorry, no new axioms, and the regression examples of PO-090, checked at the pinned toolchain. \end{RSbar} \RSfield{Literature check (28 October 2026)}GitHub code search (2026-10-28) found no δ-ring or p-derivation in mathlib. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/49}{Issue 49} of the repository. \par \RSproblem{problem-50}{Toward an algorithm for prismatic cohomology}{machine · research level}{Toward an algorithm for prismatic cohomology} \RSfield{Thesis}Thesis 12 (Judge a method by its open ledger). \RSfield{Source}\emph{Strained Prismatic Geometry} {[}S06{]}, Obstruction 49.6.6, pp.~1029--1030. \RSfield{Status in the source}OPEN. \begin{RSbar} \RSfield{Statement}``There is presently no general terminating algorithm which, from equations for an arbitrary p-adic formal scheme, computes its absolute prismatic cohomology together with derived completion, Nygaard filtration, Frobenius, and effective descent as an F-gauge''. ``The frontier relevant to this book has five layers'': absolute descent; integral semistable gauges for curves with bad reduction, including the primes 2 and 3; the Habiro--prismatic comparison; archimedean assembly; and the global strain trace. Give a terminating, certified algorithm for one layer. \end{RSbar} \RSfield{What the source establishes}The companion package of {[}S06{]} supplies finite inputs and hard failure states, and ``implements none of these by renaming a local matrix.'' \RSfield{Proposed by}{[}S06{]}. \RSfield{Background}{[}BS22{]}; {[}BL22{]}. \begin{RSbar} \RSfield{Solved when}A terminating algorithm for one of the five layers on a stated class of inputs, with a proof of correctness and an implementation whose outputs agree with known computations. \end{RSbar} \RSfield{Literature check (28 October 2026)}Explicit computations of prismatic and syntomic cohomology in special cases were found; no general algorithm for any of the five layers was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/50}{Issue 50} of the repository. \par \RSproblem{problem-51}{The real-place gauge}{mathematical · research level}{The real-place gauge} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{Strained Prismatic Geometry} {[}S06{]}, Problem 62.1.7 (rank 4 of the critical path), p.~1276. \RSfield{Status in the source}OPEN. \begin{RSbar} \RSfield{Statement}In the analytic-stack and condensed setting of {[}S06, Ch. 17{]}, ``Construct the gauge stack of PO-017; prove the uniqueness, finite-place compatibility, coherent all-place gluing, Arakelov degree comparison, and exceptional-operation functoriality of PO-018--PO-022; and settle the archimedean coefficient overlap and dualisability issues represented by PO-097--PO-098.'' \end{RSbar} \RSfield{What the source establishes}The target is typed but no existence theorem is available. The source gives the falsifier: ``A non-zero principal-rescaling defect, failure of real descent, or failure of dualisability for the required leg destroys this version of the all-place assembly.'' \RSfield{Proposed by}{[}S06{]}. \RSfield{Background}{[}Sch19{]}; {[}BS22{]}; {[}Efi24{]}. \begin{RSbar} \RSfield{Solved when}A construction with proofs of PO-017--PO-022 and PO-097--PO-098, or an instance of one of the three named falsifiers. \end{RSbar} \RSfield{Literature check (28 October 2026)}No construction of an archimedean gauge stack of this kind was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/51}{Issue 51} of the repository. \par \RSproblem{problem-52}{The gluing problem for the global substrate}{mathematical · programme level}{The gluing problem for the global substrate} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{Strained Prismatic Geometry} {[}S06{]}, Problem 18.1.5, p.~352. \RSfield{Status in the source}open. \begin{RSbar} \RSfield{Statement}Construct an analytic stack \(\mathfrak S\) with morphisms \(\mathfrak S_v\to\mathfrak S\) for every place \(v\) of \(\mathbb Q\) and a morphism \(\operatorname{Spec}\mathbb Z\to\mathfrak S\) such that (i) \(D(\mathfrak S)\) maps to \(D(\mathfrak S_v)\) for every \(v\), compatibly with the rational realisations; (ii) the local structures --- Frobenius and Nygaard filtration at finite \(v\), weight filtration and dilation at \(\infty\) --- are matched by the comparison data; and (iii) \(\mathfrak S\) is not terminal. \end{RSbar} \RSfield{What the source establishes}``Condition (iii) is what makes the problem non-trivial: a terminal object satisfies (i) and (ii) vacuously.'' The legs can be compared only through \(\mathbb Q\) (Remark 18.1.4), and Obstruction 18.1.6 shows that a Frobenius datum on a glued object degenerates at infinity. \RSfield{Proposed by}{[}S06{]}. \RSfield{Background}{[}Sch19{]}; {[}BL22{]}; {[}Dri20{]}. \begin{RSbar} \RSfield{Solved when}A construction satisfying (i)--(iii), or a proof that every analytic stack satisfying (i) and (ii) is terminal. \end{RSbar} \RSfield{Literature check (28 October 2026)}No construction of this kind was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/52}{Issue 52} of the repository. \par \subsection*{\emph{The Arithmetic Topos} (research subject: the Langlands programme)}\label{the-arithmetic-topos-research-subject-the-langlands-programme}\def\RSbmlevel{3} \RSproblem{problem-53}{The multiplicative-group gate}{mathematical · research level}{The multiplicative-group gate} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{The Arithmetic Topos} {[}S07{]}, Criterion 1.26, p.~28. \RSfield{Status in the source}FORMAL TARGET. \begin{RSbar} \RSfield{Statement}Let \(\mathrm{Bun}^{\mathrm{ar}}_{\mathbb G_m}\) be the arithmetic Picard stack of the global arithmetic curve \(\mathfrak X_{\mathbb Z}\) of {[}S07{]} and \(\mathrm{Gauge}\) its category of gauge sheaves. Construct them and prove or refute that \(\zeta(\mathrm{TC}(\Phi\mid\mathrm{Gauge}(\mathrm{Bun}^{\mathrm{ar}}_{\mathbb G_m})),s)=\pi^{-s/2} \Gamma(s/2)\zeta(s)\), the completed Riemann zeta function, with the archimedean factor produced by the archimedean chart and not inserted. \end{RSbar} \RSfield{What the source establishes}The source calls this ``the primary go/no-go test for the framework'': ``If the framework yields anything else --- in particular, if it yields 𝜁(𝑠) without the Γ-factor, or with a Γ-factor of the wrong argument --- then it is wrong, and no amount of repair at higher strata will save it.'' ``This criterion is designated for formal verification; its current status is recorded in Appendix F.'' \RSfield{Proposed by}{[}S07{]}. \RSfield{Background}Archimedean factors as regularized determinants {[}Den98{]}; {[}CC21{]}; {[}NS18{]}. \begin{RSbar} \RSfield{Solved when}A construction of the objects in the abelian case and a proof of the displayed identity, or a proof that the construction yields a different function, which refutes the framework as stated. The completed zeta function and its functional equation are classical; the problem is whether this construction produces them. \end{RSbar} \RSfield{Literature check (28 October 2026)}No construction of the arithmetic Picard stack of this framework was found outside {[}S07{]}. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/53}{Issue 53} of the repository. \par \RSproblem{problem-54}{The first falsification test for GL\(_2\)}{mathematical · research level}{The first falsification test for GL2} \RSfield{Thesis}Thesis 9 (State what is not established). \RSfield{Source}\emph{The Arithmetic Topos} {[}S07{]}, Problem 28.28, pp.~1108--1109. \RSfield{Status in the source}CONJECTURE (a falsification test). \begin{RSbar} \RSfield{Statement}``For the standard GL2 monoid over Q, construct a global distribution on the rank-one stratum whose local normal residue is the coefficient of'' Proposition 28.16 of {[}S07{]}, ``and prove that its spectral expansion is exactly the sum of the trivial, special, and maximal-parabolic terms removed in Altuğ's Poisson reorganisation.'' \end{RSbar} \RSfield{What the source establishes}A mismatch of coefficients would refute the simplest form of the source's Conjecture 28.20. The problem precedes functoriality on purpose: ``It asks whether the diagnosis reproduces a known rank-one calculation without changing its constants. A framework that cannot pass this comparison has no claim on the general problem.'' \RSfield{Proposed by}{[}S07{]}; the rank-one calculation is Altuğ's {[}Alt15{]}. \RSfield{Background}{[}Alt15{]}; {[}EEKW24{]}. \begin{RSbar} \RSfield{Solved when}The distribution constructed and its spectral expansion proved equal to the terms removed in {[}Alt15{]}, or a proof that the coefficients differ. \end{RSbar} \RSfield{Literature check (28 October 2026)}Altuğ's Beyond Endoscopy computations for GL\(_2\) over the rationals {[}Alt15{]} and their extension to totally real fields, which removes the trivial and special representations by Poisson summation on the regular elliptic terms {[}EEKW24{]}, were found; no boundary-resolution reading of them was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/54}{Issue 54} of the repository. \par \RSproblem{problem-55}{Ambidexterity over the arithmetic base}{mathematical · programme level}{Ambidexterity over the arithmetic base} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{The Arithmetic Topos} {[}S07{]}, Problem 40.11, p.~1603. \RSfield{Status in the source}CONJECTURE. \begin{RSbar} \RSfield{Statement}Let \(q\colon\mathrm{Bun}_G(\mathfrak X_{\mathbb Z})\to\mathrm{pt}\) be the structure map. Prove or refute that \(q_!\simeq q_*\) on \(\mathrm{Shv}_{\mathcal N}(\mathrm{Bun}_G(\mathfrak X_{\mathbb Z}))\) after Whittaker renormalisation; if the equivalence holds only after a renormalisation, identify it explicitly and determine whether it is canonical. \end{RSbar} \RSfield{What the source establishes}``This is the load-bearing hypothesis of the entire framework.'' Over a curve the corresponding statement, miraculous duality, is a theorem of Drinfeld and Gaitsgory; over \(\mathfrak X_{\mathbb Z}\) the local finiteness its proof uses is unavailable. ``It is also the gap about which the least can currently be said.'' \RSfield{Proposed by}{[}S07{]}; over a curve the source cites miraculous duality as a theorem of Drinfeld and Gaitsgory; see {[}Gai18{]} and {[}AGK+20{]}. \RSfield{Background}{[}DG15{]}; {[}Gai18{]}; {[}AGK+20{]}. \begin{RSbar} \RSfield{Solved when}A proof or a refutation of the equivalence, with the renormalisation identified if one is needed. \end{RSbar} \RSfield{Literature check (28 October 2026)}Miraculous duality and duality for automorphic sheaves over curves were found {[}Gai18; AGK+20{]}; no arithmetic analogue was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/55}{Issue 55} of the repository. \par \RSproblem{problem-56}{Construct the global arithmetic curve}{mathematical · programme level}{Construct the global arithmetic curve} \RSfield{Thesis}Thesis 8 (The rising sea). \RSfield{Source}\emph{The Arithmetic Topos} {[}S07{]}, Problem 40.10, p.~1602. \RSfield{Status in the source}CONJECTURE. \begin{RSbar} \RSfield{Statement}Exhibit a condensed analytic stack over the sphere spectrum satisfying the eight clauses of the definition of the global arithmetic curve \(\mathfrak X_{\mathbb Z}\) {[}S07, Definition 10.15{]} --- finite syntomic charts, an archimedean chart, a restricted adelic halo with a rational diagonal, the gluing as a homotopy fibre product, an absolute Frobenius, a gauge map to \(\mathbb A^1/\mathbb G_m\), a place map to \(\operatorname{Spec}\mathbb Z\), and a fundamental class in degree three --- prove it unique up to canonical equivalence, and equip it with a six-functor formalism with proper base change and Verdier duality. \end{RSbar} \RSfield{What the source establishes}``What exists at present is a specification and two of its charts.'' The finite charts are theorems of Bhatt--Lurie and Drinfeld; the archimedean chart is stipulated. ``The obstacle is not the charts. It is the gluing, and the reason is specific. Adelic descent along a restricted product is not a standard operation in any existing formalism.'' \RSfield{Proposed by}{[}S07{]}. \RSfield{Background}{[}BL22{]}; {[}Dri20{]}; {[}BL95{]}; {[}FS21{]}; {[}Sch19{]}. \begin{RSbar} \RSfield{Solved when}A construction with the eight clauses, the uniqueness statement and the six-functor formalism, or a proof that no object satisfies the eight clauses. \end{RSbar} \RSfield{Literature check (28 October 2026)}No construction of this kind was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/56}{Issue 56} of the repository. \par \RSproblem{problem-57}{Coherence for arithmetic modes}{formalization · research level}{Coherence for arithmetic modes} \RSfield{Thesis}Thesis 11 (Creating language). \RSfield{Source}\emph{The Arithmetic Topos} {[}S07{]}, Problem 6.29, p.~228. \RSfield{Status in the source}CONJECTURE. \begin{RSbar} \RSfield{Statement}For the modal directed type theory \(\mathrm{TT}^{\mathrm{comp}}_{\mathrm{KH}}\) of {[}S07, Ch. 6{]}, construct a finite presentation of its mode two-category and ``prove a coherence theorem deciding equality of generated two-cells'', while retaining the Beck--Chevalley, projection-formula, place-commutation, Frobenius and \(\flat\dashv\sharp\) structures of the chapter. \end{RSbar} \RSfield{What the source establishes}``A positive solution would not construct the semantic functors, but it would make their formal composites manageable. A negative solution would force a proof-relevant representation of coherence cells in the kernel and would weaken the decidability prospect.'' \RSfield{Proposed by}{[}S07{]}. \RSfield{Background}{[}GKNB21{]}; {[}Gra22{]}; {[}RS17{]}. \begin{RSbar} \RSfield{Solved when}A finite presentation and a coherence theorem with a decision procedure for equality of generated two-cells, mechanised or proved on paper with all cases, or a proof that equality is undecidable for every finite presentation retaining the listed structures. \end{RSbar} \RSfield{Literature check (28 October 2026)}Multimodal type theory {[}GKNB21{]} and its normalization theorem, which reduces conversion to the conversion problem of the mode theory and gives decidable type checking for a decidable mode theory {[}Gra22{]}, were found; no coherence theorem for these modes was found. \RSfield{Discussion}\href{https://github.com/AlienMuse/grothendieckian-problems/issues/57}{Issue 57} of the repository. \par \clearpage \section*{Appendices}\label{appendices} \subsection*{A. The problems by thesis and by work}\label{a.-the-problems-by-thesis-and-by-work}\def\RSbmlevel{3} \figref{matrix} places each problem by its thesis and its work. The first table below lists the problems of each thesis, the second counts the problems of each work by kind. \par\begin{center}\input{fig-matrix.tex} \captionof{figure}{The problems by thesis and by work. Each small cell is a problem, tinted by kind and linked to its card; the totals are by row and by column.}\label{fig:matrix} \end{center} {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Thesis \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Problems \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot 1. Worlds, not isolated theorems & 4, 15 \\ 2. Status is part of the type & 7, 8, 31 \\ 3. A structured latent space & 6, 18 \\ 4. Attention as descent & 19, 20, 22, 24, 25, 27, 28, 35 \\ 5. Report failure; abstain without evidence & 9, 16, 17, 21, 23, 30, 32, 47 \\ 6. A chain of non-implications & 5, 12, 26, 29, 34 \\ 7. Machines propose; humans authorize & 10, 11 \\ 8. The rising sea & 1, 36, 37, 38, 41, 51, 52, 55, 56 \\ 9. State what is not established & 33, 39, 40, 43, 44, 45, 48, 49, 53, 54 \\ 10. Discovery is recursive & 2, 3 \\ 11. Creating language & 14, 57 \\ 12. Judge a method by its open ledger & 13, 42, 46, 50 \\ \end{longtable} } {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{}lllll@{}} \toprule\noalign{} Work & Problems & Mathematical & Machine & Formalization \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot S01 & 1--17 & 0 & 10 & 7 \\ S02 & 18--35 & 9 & 6 & 3 \\ S03 & 36--39 & 3 & 1 & 0 \\ S04 & 40--43 & 3 & 1 & 0 \\ S05 & 44--48 & 4 & 0 & 1 \\ S06 & 49--52 & 2 & 1 & 1 \\ S07 & 53--57 & 4 & 0 & 1 \\ All & 1--57 & 25 & 19 & 13 \\ \end{longtable} } \subsection*{B. Changes made by the literature check}\label{b.-changes-made-by-the-literature-check}\def\RSbmlevel{3} The selection approved before the literature check was changed in seven places. The replaced problems are listed so that the reasons can be checked. {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Problem \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Approved candidate \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Change and reason \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot 26 & Robust exact group scan {[}S02, Open Problem 2.14.C{]} & Replaced by Question 11.11.18 of {[}S02{]}. Without the numerical setting of {[}S02, Ch. 2.14{]}, the problem reduces to multiplying permutation matrices, which floating-point arithmetic performs exactly; stated on its own it would be misleading. \\ 34 & A second kernel {[}S02, Open Problem 13.15.D{]} & Narrowed and moved to entry level. Independent type checkers for Lean 4 exist {[}Car24; nanoda{]}; the remaining task is to replay the declarations of {[}S02{]} under two of them. \\ 38 & Pin(2)-twisted topological Hochschild homology {[}S03, Problem 28.13{]} & Narrowed. The first question of the source, whether a Pin(2)-equivariant lift of THH exists, has been answered by quaternionic THH {[}AMP26{]}; the second question is kept. The source's statement that no construction is known is listed in the errata. \\ 39 & A certified finite-height computation {[}S03, Problem J.38{]} & Replaced by falsification predicate F2 {[}S03, Criterion 58.9{]}. Certified computation of the zeros of the zeta function to great height is established {[}PT21{]}, and the source's problem asks for a computation of a related kind with no decision criterion beyond it. \\ 40 & The Construction Problem {[}S04, Problem 54.1.1{]} & Replaced by Problem 22.7.1 of {[}S04{]}. The source records that its axiom F12 carries essentially the whole arithmetic content of the conjecture of Birch and Swinnerton-Dyer {[}S04, Remark 56.2.1{]}, so the original would fall under the exclusion of problems whose solution proves a named conjecture. \\ 45 & The certification boundary {[}S05, Problem 71.9.3{]} & Replaced by Problem 71.3.4 of {[}S05{]}. In the form stated, the impossibility of certifying a relation from finite-precision data follows from the undecidability of equality of computable real numbers, a standard result of computable analysis. \\ 47 & The Rigidification Conjecture in rank two {[}S05, Problem 71.6.3{]} & Replaced by Problem 71.3.3 of {[}S05{]}. The relation of the rank-two case to known results, including the Lefschetz (1,1) theorem, needs an expert reading before it can be posed as open. \\ \end{longtable} } \subsection*{C. The machine-readable file}\label{c.-the-machine-readable-file}\def\RSbmlevel{3} \texttt{problems.json} in the repository contains, for each problem, the fields of its card and the identifiers of its source (work, DOI, pages, status), its thesis, its kind and level, the date of its literature check and the path of its Lean statement where one exists. The file is generated from the same source as this paper, and the two are checked to agree field by field. \section*{Declarations}\label{declarations} \textbf{Use of AI tools.} The main ideas and the architecture of the Grothendieckian Programme are the author's and come from the author's research at WiseMotif.ai. In the seven works, AI tools assisted with drafting and with part of the literature collation; all of the text was reviewed by the author. Lean verification of the seven works is incomplete. Because of their size, the works are first drafts (Research Architecture Edition 1) and have not been peer-reviewed; they need review by experts and further work on the programme. They are released openly for that purpose, in the hope of further contributions and of more recursive mathematical discovery in AI for mathematics. For the present paper, statements were extracted from the published works by script and checked against the PDFs; AI tools assisted with drafting and with literature collation; the author selected the theses and problems and reviewed every statement. \textbf{Funding and competing interests.} No external funding. The author is affiliated with WiseMotif.ai. \textbf{Data availability.} The source texts are the sealed PDFs of the seven works and of the overview, each with a Zenodo DOI given in the references. The extraction scripts and the list of extracted items, the record of the literature check, the reference check, the Lean statements, the figures with their data and sources, and the machine-readable file of the paper are in the repository \url{https://github.com/AlienMuse/grothendieckian-problems}. \textbf{Licence.} This paper, its figures and its data are released under the Creative Commons Attribution 4.0 International licence (CC BY 4.0); the code in the repository --- the Lean files, the scripts and the source code of the figures --- under the Apache License 2.0. The seven works and the overview are released under CC BY-NC-ND 4.0, and the quotations from them in this paper are reproduced under that licence with attribution. \textbf{Name.} The adjective \emph{Grothendieckian} names a mathematical method used in the seven works. It carries no attribution of design or endorsement to Alexander Grothendieck or to any other mathematician whose work is cited; no problem in this paper was posed by Grothendieck unless the card says so. \section*{References}\label{references} \begin{RSreferences} \item {[}S00{]} Vincent Liu, \emph{The Grothendieckian Programme: Recursive Mathematical Discovery in the Age of Machine Reasoning}, Zenodo, 2026, An overview of Series 01--07; WiseMotif Monograph of Mathematical Intelligence, Series 00, doi:\href{https://doi.org/10.5281/zenodo.23669107}{10.5281/zenodo.23669107}. \item {[}S01{]} Vincent Liu, \emph{GAI-MUA: The Grothendieckian Machine. A Mathematical Universe Architecture for Verifiable and Self-Evolving Artificial Intelligence}, Zenodo, 2026, WiseMotif Monograph of Mathematical Intelligence, Series 01; 6 volumes, doi:\href{https://doi.org/10.5281/zenodo.23480696}{10.5281/zenodo.23480696}. \item {[}S02{]} Vincent Liu, \emph{GM-Omega-Infinity: Topos-Native Intelligence. A Sheaf-Theoretic Architecture for Verifiable Machine Intelligence}, Zenodo, 2026, Series 02; 5 volumes, doi:\href{https://doi.org/10.5281/zenodo.23538544}{10.5281/zenodo.23538544}. \item {[}S03{]} Vincent Liu, \emph{Arithmetic Spectral Descent: Obstruction Theory, Hodge--Krein Realization, and a Falsifiable Architecture for the Riemann Hypothesis}, Zenodo, 2026, Series 03; 4 volumes, doi:\href{https://doi.org/10.5281/zenodo.23564898}{10.5281/zenodo.23564898}. \item {[}S04{]} Vincent Liu, \emph{Fractured Adelic Geometry: A Foundational Framework for the Birch and Swinnerton-Dyer Conjecture}, Zenodo, 2026, Series 04; 4 volumes, doi:\href{https://doi.org/10.5281/zenodo.23585887}{10.5281/zenodo.23585887}. \item {[}S05{]} Vincent Liu, \emph{The Archimedean Prism: Tame Period Geometry and the Hodge Conjecture}, Zenodo, 2026, Series 05; 5 volumes, doi:\href{https://doi.org/10.5281/zenodo.23597954}{10.5281/zenodo.23597954}. \item {[}S06{]} Vincent Liu, \emph{Strained Prismatic Geometry: Deformation over the Absolute Base and the abc Conjecture}, Zenodo, 2026, Series 06; 5 volumes, doi:\href{https://doi.org/10.5281/zenodo.23610034}{10.5281/zenodo.23610034}. \item {[}S07{]} Vincent Liu, \emph{The Arithmetic Topos: Foundations of a Trace-Theoretic Approach to the Langlands Programme}, Zenodo, 2026, Series 07; 5 volumes, doi:\href{https://doi.org/10.5281/zenodo.23629681}{10.5281/zenodo.23629681}. \item {[}ACG+24{]} Arash Ahmadian, Chris Cremer, Matthias Gallé, Marzieh Fadaee, Julia Kreutzer, Olivier Pietquin, Ahmet Üstün, and Sara Hooker, \emph{Back to basics: revisiting REINFORCE-style optimization for learning from human feedback in LLMs}, Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (ACL 2024), 2024, arXiv:\href{https://arxiv.org/abs/2402.14740}{2402.14740}. \item {[}AGK+20{]} Dima Arinkin, Dennis Gaitsgory, David Kazhdan, Sam Raskin, Nick Rozenblyum, and Yakov Varshavsky, \emph{Duality for automorphic sheaves with nilpotent singular support}, preprint, 2020, arXiv:\href{https://arxiv.org/abs/2012.07665}{2012.07665}. \item {[}Alt15{]} S. Ali Altuğ, \emph{Beyond endoscopy via the trace formula: 1. Poisson summation and isolation of special representations}, Compos. Math. \textbf{151} (2015), 1791--1820, doi:\href{https://doi.org/10.1112/S0010437X15007320}{10.1112/S0010437X15007320}. \item {[}AMP26{]} Gabriel Angelini-Knoll, Mona Merling, and Maximilien Péroux, \emph{Topological ΔG-homology of rings with twisted G-action}, Adv. Math. (2026), 110907, doi:\href{https://doi.org/10.1016/j.aim.2026.110907}{10.1016/j.aim.2026.110907}. \item {[}AMS08{]} P.-A. Absil, R. Mahony, and R. Sepulchre, \emph{Optimization Algorithms on Matrix Manifolds}, Princeton University Press, 2008, doi:\href{https://doi.org/10.1515/9781400830244}{10.1515/9781400830244}. \item {[}Bar89{]} David A. Mix Barrington, \emph{Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹}, J. Comput. System Sci. \textbf{38} (1989), 150--164, doi:\href{https://doi.org/10.1016/0022-0000(89)90037-8}{10.1016/0022-0000(89)90037-8}. \item {[}BBCV21{]} Michael M. Bronstein, Joan Bruna, Taco Cohen, and Petar Veličković, \emph{Geometric deep learning: grids, groups, graphs, geodesics, and gauges}, preprint, 2021, arXiv:\href{https://arxiv.org/abs/2104.13478}{2104.13478}. \item {[}BCD+26{]} Joanna Bieri, Edgar Costa, Alyson Deines, Kyu-Hwan Lee, David Lowry-Duda, Thomas Oliver, Yidi Qi, and Tamara Veenstra, \emph{Murmurations, Mestre--Nagao sums, and convolutional neural networks for elliptic curves}, preprint, 2026, arXiv:\href{https://arxiv.org/abs/2603.17681}{2603.17681}. \item {[}BDCLB22{]} Cristian Bodnar, Francesco Di Giovanni, Benjamin Paul Chamberlain, Pietro Liò, and Michael M. Bronstein, \emph{Neural sheaf diffusion: a topological perspective on heterophily and oversmoothing in GNNs}, Advances in Neural Information Processing Systems 35 (NeurIPS 2022), 2022, arXiv:\href{https://arxiv.org/abs/2202.04579}{2202.04579}. \item {[}BIS90{]} David A. Mix Barrington, Neil Immerman, and Howard Straubing, \emph{On uniformity within NC¹}, J. Comput. System Sci. \textbf{41} (1990), 274--306, doi:\href{https://doi.org/10.1016/0022-0000(90)90022-D}{10.1016/0022-0000(90)90022-D}. \item {[}BK90{]} Spencer Bloch and Kazuya Kato, \emph{L-functions and Tamagawa numbers of motives}, The Grothendieck Festschrift, Vol. I, Progr. Math. 86, Birkhäuser, 1990, pp.~333--400, DOI of the 2007 Modern Birkhäuser Classics reprint, doi:\href{https://doi.org/10.1007/978-0-8176-4574-8_9}{10.1007/978-0-8176-4574-8\_9}. \item {[}BKLPR15{]} Manjul Bhargava, Daniel M. Kane, Hendrik W. Lenstra Jr., Bjorn Poonen, and Eric Rains, \emph{Modeling the distribution of ranks, Selmer groups, and Shafarevich--Tate groups of elliptic curves}, Camb. J. Math. \textbf{3} (2015), 275--321, doi:\href{https://doi.org/10.4310/CJM.2015.v3.n3.a1}{10.4310/CJM.2015.v3.n3.a1}. \item {[}BL22{]} Bhargav Bhatt and Jacob Lurie, \emph{Absolute prismatic cohomology}, preprint, 2022, arXiv:\href{https://arxiv.org/abs/2201.06120}{2201.06120}. \item {[}BL95{]} Arnaud Beauville and Yves Laszlo, \emph{Un lemme de descente}, C. R. Acad. Sci. Paris Sér. I Math. \textbf{320} (1995), 335--340. \item {[}Bre11{]} Emmanuel Breuillard, \emph{A height gap theorem for finite subsets of GL\_d(\={Q}) and nonamenable subgroups}, Ann. of Math. (2) \textbf{174} (2011), 1057--1110, doi:\href{https://doi.org/10.4007/annals.2011.174.2.7}{10.4007/annals.2011.174.2.7}. \item {[}BS22{]} Bhargav Bhatt and Peter Scholze, \emph{Prisms and prismatic cohomology}, Ann. of Math. (2) \textbf{196} (2022), 1135--1275, doi:\href{https://doi.org/10.4007/annals.2022.196.3.5}{10.4007/annals.2022.196.3.5}. \item {[}Bui05{]} Alexandru Buium, \emph{Arithmetic Differential Equations}, Mathematical Surveys and Monographs 118, Amer. Math. Soc., 2005, doi:\href{https://doi.org/10.1090/surv/118}{10.1090/surv/118}. \item {[}BW05{]} Henk Barendregt and Freek Wiedijk, \emph{The challenge of computer mathematics}, Philos. Trans. R. Soc. A \textbf{363} (2005), 2351--2375, doi:\href{https://doi.org/10.1098/rsta.2005.1650}{10.1098/rsta.2005.1650}. \item {[}Car24{]} Mario Carneiro, \emph{Lean4Lean: towards a verified typechecker for Lean, in Lean}, preprint, 2024, arXiv:\href{https://arxiv.org/abs/2403.14064}{2403.14064}. \item {[}Car81{]} Jack Carr, \emph{Applications of Centre Manifold Theory}, Applied Mathematical Sciences 35, Springer, 1981, doi:\href{https://doi.org/10.1007/978-1-4612-5929-9}{10.1007/978-1-4612-5929-9}. \item {[}CC21{]} Alain Connes and Caterina Consani, \emph{Weil positivity and trace formula, the archimedean place}, Selecta Math. (N.S.) \textbf{27} (2021), 77, doi:\href{https://doi.org/10.1007/s00029-021-00689-4}{10.1007/s00029-021-00689-4}. \item {[}CCHM18{]} Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, \emph{Cubical type theory: a constructive interpretation of the univalence axiom}, 21st International Conference on Types for Proofs and Programs (TYPES 2015), LIPIcs 69, 2018, pp.~5:1--5:34, doi:\href{https://doi.org/10.4230/LIPIcs.TYPES.2015.5}{10.4230/LIPIcs.TYPES.2015.5}. \item {[}CDK95{]} Eduardo Cattani, Pierre Deligne, and Aroldo Kaplan, \emph{On the locus of Hodge classes}, J. Amer. Math. Soc. \textbf{8} (1995), 483--506, doi:\href{https://doi.org/10.1090/S0894-0347-1995-1273413-2}{10.1090/S0894-0347-1995-1273413-2}. \item {[}CF09{]} Jacques Carette and William M. Farmer, \emph{A review of mathematical knowledge management}, Intelligent Computer Mathematics (MKM 2009), Lecture Notes in Comput. Sci. 5625, Springer, 2009, pp.~233--246, doi:\href{https://doi.org/10.1007/978-3-642-02614-0_21}{10.1007/978-3-642-02614-0\_21}. \item {[}Cow24{]} Alex Cowan, \emph{Murmurations and ratios conjectures}, preprint, 2024, arXiv:\href{https://arxiv.org/abs/2408.12723}{2408.12723}. \item {[}DBDL24{]} Leonardo Di Nino, Sergio Barbarossa, and Paolo Di Lorenzo, \emph{Learning sheaf Laplacian optimizing restriction maps}, 58th Asilomar Conference on Signals, Systems, and Computers, IEEE, 2024, doi:\href{https://doi.org/10.1109/IEEECONF60004.2024.10942997}{10.1109/IEEECONF60004.2024.10942997}. \item {[}Del71{]} Pierre Deligne, \emph{Théorie de Hodge. II}, Publ. Math. Inst. Hautes Études Sci. \textbf{40} (1971), 5--57, doi:\href{https://doi.org/10.1007/BF02684692}{10.1007/BF02684692}. \item {[}Del74{]} Pierre Deligne, \emph{La conjecture de Weil. I}, Publ. Math. Inst. Hautes Études Sci. \textbf{43} (1974), 273--307, doi:\href{https://doi.org/10.1007/BF02684373}{10.1007/BF02684373}. \item {[}Den98{]} Christopher Deninger, \emph{Some analogies between number theory and dynamical systems on foliated spaces}, Proceedings of the International Congress of Mathematicians, Vol. I (Berlin, 1998), Doc. Math. Extra Vol. ICM I, 1998, pp.~163--186. \item {[}DG15{]} Vladimir Drinfeld and Dennis Gaitsgory, \emph{Compact generation of the category of D-modules on the stack of G-bundles on a curve}, Camb. J. Math. \textbf{3} (2015), 19--125, doi:\href{https://doi.org/10.4310/CJM.2015.v3.n1.a2}{10.4310/CJM.2015.v3.n1.a2}. \item {[}DMPR21{]} Emanuele Dotto, Kristian Moi, Irakli Patchkoria, and Sune Precht Reeh, \emph{Real topological Hochschild homology}, J. Eur. Math. Soc. \textbf{23} (2021), 63--152, doi:\href{https://doi.org/10.4171/jems/1007}{10.4171/jems/1007}. \item {[}Dri20{]} Vladimir Drinfeld, \emph{Prismatization}, preprint, 2020, arXiv:\href{https://arxiv.org/abs/2005.04746}{2005.04746}. \item {[}DV66{]} Jack B. Dennis and Earl C. Van Horn, \emph{Programming semantics for multiprogrammed computations}, Comm. ACM \textbf{9} (1966), 143--155, doi:\href{https://doi.org/10.1145/365230.365252}{10.1145/365230.365252}. \item {[}DVB+21{]} Alex Davies, Petar Veličković, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomašev, Richard Tanburn, Peter Battaglia, Charles Blundell, András Juhász, Marc Lackenby, Geordie Williamson, Demis Hassabis, and Pushmeet Kohli, \emph{Advancing mathematics by guiding human intuition with AI}, Nature \textbf{600} (2021), 70--74, doi:\href{https://doi.org/10.1038/s41586-021-04086-x}{10.1038/s41586-021-04086-x}. \item {[}EEKW24{]} Melissa Emory, Malors Espinosa-Lara, Debanjana Kundu, and Tian An Wong, \emph{Beyond endoscopy via Poisson summation for GL(2, K)}, preprint, 2024, arXiv:\href{https://arxiv.org/abs/2404.10139}{2404.10139}. \item {[}Efi24{]} Alexander I. Efimov, \emph{K-theory and localizing invariants of large categories}, preprint, 2024, arXiv:\href{https://arxiv.org/abs/2405.12169}{2405.12169}. \item {[}EW10{]} Ran El-Yaniv and Yair Wiener, \emph{On the foundations of noise-free selective classification}, J. Mach. Learn. Res. \textbf{11} (2010), 1605--1641, \url{https://www.jmlr.org/papers/v11/el-yaniv10a.html}. \item {[}Faj88{]} Siemion Fajtlowicz, \emph{On conjectures of Graffiti}, Discrete Math. \textbf{72} (1988), 113--118, doi:\href{https://doi.org/10.1016/0012-365X(88)90199-9}{10.1016/0012-365X(88)90199-9}. \item {[}FKKG24{]} Sebastian Farquhar, Jannik Kossen, Lorenz Kuhn, and Yarin Gal, \emph{Detecting hallucinations in large language models using semantic entropy}, Nature \textbf{630} (2024), 625--630, doi:\href{https://doi.org/10.1038/s41586-024-07421-0}{10.1038/s41586-024-07421-0}. \item {[}FLM+26{]} Moritz Firsching, Paul Lezeau, Salvatore Mercuri, Miklós Z. Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, and Pushmeet Kohli, \emph{Formal Conjectures: an open and evolving benchmark for verified discovery in mathematics}, preprint, 2026, arXiv:\href{https://arxiv.org/abs/2605.13171}{2605.13171}. \item {[}FS21{]} Laurent Fargues and Peter Scholze, \emph{Geometrization of the local Langlands correspondence}, preprint, 2021, arXiv:\href{https://arxiv.org/abs/2102.13459}{2102.13459}. \item {[}FZS22{]} William Fedus, Barret Zoph, and Noam Shazeer, \emph{Switch transformers: scaling to trillion parameter models with simple and efficient sparsity}, J. Mach. Learn. Res. \textbf{23} (2022), no. 120, 1--39, arXiv:\href{https://arxiv.org/abs/2101.03961}{2101.03961}. \item {[}Gai18{]} Dennis Gaitsgory, \emph{A ``strange'' functional equation for Eisenstein series and miraculous duality on the moduli stack of bundles}, Ann. Sci. Éc. Norm. Supér. (4) \textbf{50} (2017), 1123--1162, doi:\href{https://doi.org/10.24033/asens.2341}{10.24033/asens.2341}. \item {[}Gan13{]} Mohan Ganesalingam, \emph{The Language of Mathematics: A Linguistic and Philosophical Investigation}, Lecture Notes in Comput. Sci. 7805, Springer, 2013, doi:\href{https://doi.org/10.1007/978-3-642-37012-0}{10.1007/978-3-642-37012-0}. \item {[}Gir71{]} Jean Giraud, \emph{Cohomologie non abélienne}, Grundlehren der mathematischen Wissenschaften 179, Springer, 1971, doi:\href{https://doi.org/10.1007/978-3-662-62103-5}{10.1007/978-3-662-62103-5}. \item {[}GKNB21{]} Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal, \emph{Multimodal dependent type theory}, Log. Methods Comput. Sci. \textbf{17} (2021), no. 3, 11:1--11:67, doi:\href{https://doi.org/10.46298/lmcs-17(3:11)2021}{10.46298/lmcs-17(3:11)2021}. \item {[}GLD+24{]} Bruno Gavranović, Paul Lessard, Andrew Dudzik, Tamara von Glehn, João G. M. Araújo, and Petar Veličković, \emph{Position: categorical deep learning is an algebraic theory of all architectures}, Proceedings of the 41st International Conference on Machine Learning (ICML 2024), PMLR 235, 2024, arXiv:\href{https://arxiv.org/abs/2402.15332}{2402.15332}. \item {[}GM82{]} Joseph A. Goguen and José Meseguer, \emph{Security policies and security models}, 1982 IEEE Symposium on Security and Privacy, IEEE, 1982, pp.~11--20, doi:\href{https://doi.org/10.1109/SP.1982.10014}{10.1109/SP.1982.10014}. \item {[}Gra22{]} Daniel Gratzer, \emph{Normalization for multimodal type theory}, Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022), ACM, 2022, pp.~1--13, doi:\href{https://doi.org/10.1145/3531130.3532398}{10.1145/3531130.3532398}. \item {[}Gro26{]} Akiva Groskin, \emph{A finite Guinand-Weil dictionary and archimedean tail order for the truncated Weil quadratic form}, preprint, 2026, arXiv:\href{https://arxiv.org/abs/2607.02828}{2607.02828}. \item {[}HG19{]} Jakob Hansen and Robert Ghrist, \emph{Toward a spectral theory of cellular sheaves}, J. Appl. Comput. Topol. \textbf{3} (2019), 315--358, doi:\href{https://doi.org/10.1007/s41468-019-00038-7}{10.1007/s41468-019-00038-7}. \item {[}Hig02{]} Nicholas J. Higham, \emph{Accuracy and Stability of Numerical Algorithms}, 2nd ed., SIAM, 2002, doi:\href{https://doi.org/10.1137/1.9780898718027}{10.1137/1.9780898718027}. \item {[}HLOP22{]} Yang-Hui He, Kyu-Hwan Lee, Thomas Oliver, and Alexey Pozdnyakov, \emph{Murmurations of elliptic curves}, preprint, 2022, arXiv:\href{https://arxiv.org/abs/2204.10140}{2204.10140}. \item {[}HRH24{]} Steve Huntsman, Michael Robinson, and Ludmilla Huntsman, \emph{Prospects for inconsistency detection using large language models and sheaves}, preprint, 2024, arXiv:\href{https://arxiv.org/abs/2401.16713}{2401.16713}. \item {[}HW90{]} Maurice P. Herlihy and Jeannette M. Wing, \emph{Linearizability: a correctness condition for concurrent objects}, ACM Trans. Program. Lang. Syst. \textbf{12} (1990), 463--492, doi:\href{https://doi.org/10.1145/78969.78972}{10.1145/78969.78972}. \item {[}IEEE19{]} IEEE, \emph{IEEE Standard for Floating-Point Arithmetic}, 2019, IEEE Std 754-2019, doi:\href{https://doi.org/10.1109/IEEESTD.2019.8766229}{10.1109/IEEESTD.2019.8766229}. \item {[}Jac04{]} Allyn Jackson, \emph{Comme appelé du néant --- As if summoned from the void: the life of Alexandre Grothendieck, Part II}, Notices Amer. Math. Soc. \textbf{51} (2004), no. 10, 1196--1212, \url{https://www.ams.org/notices/200410/fea-grothendieck-part2.pdf}. \item {[}Joh17{]} Fredrik Johansson, \emph{Arb: efficient arbitrary-precision midpoint-radius interval arithmetic}, IEEE Trans. Comput. \textbf{66} (2017), 1281--1292, doi:\href{https://doi.org/10.1109/TC.2017.2690633}{10.1109/TC.2017.2690633}. \item {[}Joy85{]} André Joyal, \emph{δ-anneaux et vecteurs de Witt}, C. R. Math. Rep.~Acad. Sci. Canada \textbf{7} (1985), 177--182. \item {[}Lak76{]} Imre Lakatos, \emph{Proofs and Refutations: The Logic of Mathematical Discovery}, Cambridge University Press, 1976, doi:\href{https://doi.org/10.1017/CBO9781139171472}{10.1017/CBO9781139171472}. \item {[}Liu26a{]} Vincent Liu, \emph{The Grothendieckian Programme: An Overview --- Seven Open Works on Mathematics and Machine Reasoning}, 2026, preprint, Zenodo; the first of three papers released together, doi:\href{https://doi.org/10.5281/zenodo.23734421}{10.5281/zenodo.23734421}. \item {[}Liu26b{]} Vincent Liu, \emph{The Rising-Sea Theses: Twelve Theses on Mathematics and Machine Reasoning}, 2026, preprint, Zenodo; the second of three papers released together, doi:\href{https://doi.org/10.5281/zenodo.23734423}{10.5281/zenodo.23734423}. \item {[}Lur09{]} Jacob Lurie, \emph{Higher Topos Theory}, Annals of Mathematics Studies 170, Princeton University Press, 2009, doi:\href{https://doi.org/10.1515/9781400830558}{10.1515/9781400830558}. \item {[}LZ22{]} Chris Lamb and Stefano Zacchiroli, \emph{Reproducible builds: increasing the integrity of software supply chains}, IEEE Software \textbf{39} (2022), no. 2, 62--70, doi:\href{https://doi.org/10.1109/MS.2021.3073045}{10.1109/MS.2021.3073045}. \item {[}Mac78{]} Saunders Mac Lane, \emph{Categories for the Working Mathematician}, Graduate Texts in Mathematics 5, Springer, 1978, doi:\href{https://doi.org/10.1007/978-1-4757-4721-8}{10.1007/978-1-4757-4721-8}. \item {[}Mah25{]} Sridhar Mahadevan, \emph{Topos theory for generative AI and LLMs}, preprint, 2025, arXiv:\href{https://arxiv.org/abs/2508.08293}{2508.08293}. \item {[}Man16{]} Ciprian Manolescu, \emph{Pin(2)-equivariant Seiberg--Witten Floer homology and the triangulation conjecture}, J. Amer. Math. Soc. \textbf{29} (2016), 147--176, doi:\href{https://doi.org/10.1090/jams829}{10.1090/jams829}. \item {[}mC20{]} The mathlib Community, \emph{The Lean mathematical library}, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, pp.~367--381, doi:\href{https://doi.org/10.1145/3372885.3373824}{10.1145/3372885.3373824}. \item {[}McL07{]} Colin McLarty, \emph{The rising sea: Grothendieck on simplicity and generality}, Episodes in the History of Modern Algebra (1800--1950) (Jeremy J. Gray and Karen Hunger Parshall, eds.), History of Mathematics 32, Amer. Math. Soc., 2007, pp.~301--325. \item {[}MM94{]} Saunders Mac Lane and Ieke Moerdijk, \emph{Sheaves in Geometry and Logic: A First Introduction to Topos Theory}, Universitext, Springer, 1994, corrected reprint of the 1992 edition, doi:\href{https://doi.org/10.1007/978-1-4612-0927-0}{10.1007/978-1-4612-0927-0}. \item {[}MU21{]} Leonardo de Moura and Sebastian Ullrich, \emph{The Lean 4 theorem prover and programming language}, Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci. 12699, Springer, 2021, pp.~625--635, doi:\href{https://doi.org/10.1007/978-3-030-79876-5_37}{10.1007/978-3-030-79876-5\_37}. \item {[}MV99{]} Fabien Morel and Vladimir Voevodsky, \emph{A¹-homotopy theory of schemes}, Publ. Math. Inst. Hautes Études Sci. \textbf{90} (1999), 45--143, doi:\href{https://doi.org/10.1007/BF02698831}{10.1007/BF02698831}. \item {[}nanoda{]} Chris Bailey, \emph{nanoda\_lib: library implementing type inference/check\-ing functionality based on the Lean theorem prover}, 2026, software, consulted 28 October 2026, \url{https://github.com/ammkrn/nanoda_lib}. \item {[}Nec97{]} George C. Necula, \emph{Proof-carrying code}, Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '97), ACM, 1997, pp.~106--119, doi:\href{https://doi.org/10.1145/263699.263712}{10.1145/263699.263712}. \item {[}NEDM18{]} Brian A. Nosek, Charles R. Ebersole, Alexander C. DeHaven, and David T. Mellor, \emph{The preregistration revolution}, Proc. Natl. Acad. Sci. USA \textbf{115} (2018), 2600--2606, doi:\href{https://doi.org/10.1073/pnas.1708274114}{10.1073/pnas.1708274114}. \item {[}NS18{]} Thomas Nikolaus and Peter Scholze, \emph{On topological cyclic homology}, Acta Math. \textbf{221} (2018), 203--409, doi:\href{https://doi.org/10.4310/ACTA.2018.v221.n2.a1}{10.4310/ACTA.2018.v221.n2.a1}. \item {[}PT21{]} Dave Platt and Tim Trudgian, \emph{The Riemann hypothesis is true up to 3·10¹²}, Bull. Lond. Math. Soc. \textbf{53} (2021), 792--797, doi:\href{https://doi.org/10.1112/blms.12460}{10.1112/blms.12460}. \item {[}RBN+24{]} Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi, \emph{Mathematical discoveries from program search with large language models}, Nature \textbf{625} (2024), 468--475, doi:\href{https://doi.org/10.1038/s41586-023-06924-6}{10.1038/s41586-023-06924-6}. \item {[}RGM+21{]} Gal Raayoni, Shahar Gottlieb, Yahel Manor, George Pisha, Yoav Harris, Uri Mendlovic, Doron Haviv, Yaron Hadad, and Ido Kaminer, \emph{Generating conjectures on fundamental constants with the Ramanujan Machine}, Nature \textbf{590} (2021), 67--73, doi:\href{https://doi.org/10.1038/s41586-021-03229-4}{10.1038/s41586-021-03229-4}. \item {[}RS17{]} Emily Riehl and Michael Shulman, \emph{A type theory for synthetic ∞-categories}, Higher Structures \textbf{1} (2017), 147--224, arXiv:\href{https://arxiv.org/abs/1705.07442}{1705.07442}. \item {[}Sch19{]} Peter Scholze, \emph{Lectures on condensed mathematics}, 2019, lecture notes, with D. Clausen, \url{https://www.math.uni-bonn.de/people/scholze/Condensed.pdf}. \item {[}Sch22{]} Peter Scholze, \emph{Liquid tensor experiment}, Exp. Math. \textbf{31} (2022), 349--354, doi:\href{https://doi.org/10.1080/10586458.2021.1926016}{10.1080/10586458.2021.1926016}. \item {[}Sch73{]} Wilfried Schmid, \emph{Variation of Hodge structure: the singularities of the period mapping}, Invent. Math. \textbf{22} (1973), 211--319, doi:\href{https://doi.org/10.1007/BF01389674}{10.1007/BF01389674}. \item {[}SGA4{]} Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier, \emph{Théorie des topos et cohomologie étale des schémas (SGA 4), Tome 1}, Lecture Notes in Math. 269, Springer, 1972, doi:\href{https://doi.org/10.1007/BFb0081551}{10.1007/BFb0081551}. \item {[}SHKK22{]} Joar Skalse, Nikolaus H. R. Howe, Dmitrii Krasheninnikov, and David Krueger, \emph{Defining and characterizing reward hacking}, Advances in Neural Information Processing Systems 35 (NeurIPS 2022), 2022, arXiv:\href{https://arxiv.org/abs/2209.13085}{2209.13085}. \item {[}SMM+17{]} Noam Shazeer, Azalia Mirhoseini, Krzysztof Maziarz, Andy Davis, Quoc Le, Geoffrey Hinton, and Jeff Dean, \emph{Outrageously large neural networks: the sparsely-gated mixture-of-experts layer}, International Conference on Learning Representations (ICLR 2017), 2017, arXiv:\href{https://arxiv.org/abs/1701.06538}{1701.06538}. \item {[}SS25{]} Will Sawin and Andrew V. Sutherland, \emph{Murmurations for elliptic curves ordered by height}, preprint, 2025, arXiv:\href{https://arxiv.org/abs/2504.12295}{2504.12295}. \item {[}SS75{]} Jerome H. Saltzer and Michael D. Schroeder, \emph{The protection of information in computer systems}, Proc. IEEE \textbf{63} (1975), 1278--1308, doi:\href{https://doi.org/10.1109/PROC.1975.9939}{10.1109/PROC.1975.9939}. \item {[}SWZ+24{]} Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo, \emph{DeepSeekMath: pushing the limits of mathematical reasoning in open language models}, preprint, 2024, arXiv:\href{https://arxiv.org/abs/2402.03300}{2402.03300}. \item {[}Tat75{]} John Tate, \emph{Algorithm for determining the type of a singular fiber in an elliptic pencil}, Modular Functions of One Variable IV, Lecture Notes in Math. 476, Springer, 1975, pp.~33--52, doi:\href{https://doi.org/10.1007/BFb0097582}{10.1007/BFb0097582}. \item {[}Tit72{]} Jacques Tits, \emph{Free subgroups in linear groups}, J. Algebra \textbf{20} (1972), 250--270, doi:\href{https://doi.org/10.1016/0021-8693(72)90058-0}{10.1016/0021-8693(72)90058-0}. \item {[}TWL+24{]} Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong, \emph{Solving olympiad geometry without human demonstrations}, Nature \textbf{625} (2024), 476--482, doi:\href{https://doi.org/10.1038/s41586-023-06747-5}{10.1038/s41586-023-06747-5}. \item {[}Uni13{]} The Univalent Foundations Program, \emph{Homotopy Type Theory: Univalent Foundations of Mathematics}, Institute for Advanced Study, 2013, \url{https://homotopytypetheory.org/book/}. \item {[}VMA21{]} Andrea Vezzosi, Anders Mörtberg, and Andreas Abel, \emph{Cubical Agda: a dependently typed programming language with univalence and higher inductive types}, J. Funct. Programming \textbf{31} (2021), e8, doi:\href{https://doi.org/10.1017/S0956796821000034}{10.1017/S0956796821000034}. \item {[}Voi02{]} Claire Voisin, \emph{A counterexample to the Hodge conjecture extended to Kähler varieties}, Int. Math. Res. Not. (2002), 1057--1075, no. 20, doi:\href{https://doi.org/10.1155/S1073792802111135}{10.1155/S1073792802111135}. \item {[}Voi02b{]} Claire Voisin, \emph{Hodge Theory and Complex Algebraic Geometry I}, Cambridge Studies in Advanced Mathematics 76, Cambridge University Press, 2002, doi:\href{https://doi.org/10.1017/CBO9780511615344}{10.1017/CBO9780511615344}. \item {[}Wes26{]} Saint Wesonga, \emph{Formalizing PARITY circuit lower bounds in Lean}, preprint, 2026, arXiv:\href{https://arxiv.org/abs/2609.24188}{2609.24188}. \item {[}WJL+22{]} Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy, \emph{Autoformalization with large language models}, Advances in Neural Information Processing Systems 35 (NeurIPS 2022), 2022, arXiv:\href{https://arxiv.org/abs/2205.12615}{2205.12615}. \item {[}ZDY+25{]} Ziyang Zhang, Xinheng Ding, Jiayi Yuan, Rixin Liu, Huizi Mao, Jiarong Xing, and Zirui Liu, \emph{Deterministic inference across tensor parallel sizes that eliminates training-inference mismatch}, preprint, 2025, arXiv:\href{https://arxiv.org/abs/2511.17826}{2511.17826}. \item {[}ZHP22{]} Kunhao Zheng, Jesse Michael Han, and Stanislas Polu, \emph{miniF2F: a cross-system benchmark for formal Olympiad-level mathematics}, International Conference on Learning Representations (ICLR 2022), 2022, arXiv:\href{https://arxiv.org/abs/2109.00110}{2109.00110}. \item {[}Zub23{]} Nina Zubrilina, \emph{Murmurations}, preprint, 2023, arXiv:\href{https://arxiv.org/abs/2310.07681}{2310.07681}. \item {[}ZZA+25{]} Guanning Zeng, Zhaoyi Zhou, Daman Arora, and Andrea Zanette, \emph{Shrinking the variance: shrinkage baselines for reinforcement learning with verifiable rewards}, preprint, 2025, arXiv:\href{https://arxiv.org/abs/2511.03710}{2511.03710}. \end{RSreferences} \end{document}