% !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 Grothendieckian Programme: An Overview}
\newcommand{\RSsubtitle}{Seven Open Works on Mathematics and Machine Reasoning}
\newcommand{\RSshorttitle}{The Grothendieckian Programme: An Overview}
\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.23734422}   % \def, not \newcommand: the title block tests it against \@empty
\newcommand{\RSmsc}{Primary 00-02; Secondary 68T01, 68V15, 18F10, 14A15}
\newcommand{\RSkeywords}{Grothendieckian Programme, machine reasoning, mathematical worlds, descent, recursive mathematical discovery, open science}
\hypersetup{pdftitle={The Grothendieckian Programme: An Overview --- Seven Open Works on Mathematics and Machine Reasoning},pdfauthor={Vincent Liu},pdfkeywords={Grothendieckian Programme, machine reasoning, mathematical worlds, descent, recursive mathematical discovery, open science},
  pdfsubject={An overview of the seven works of the Grothendieckian Programme, their method and their open process},pdflang={en-GB}}

%% ---- the house layer: title block, headings, theses, problem cards, figures, references ------------------------
\input{rs-header.tex}

\begin{document}
\RSmaketitle{%
The Grothendieckian Programme is a series of seven works on machine reasoning about mathematics (34 volumes, 26,021 pages), released openly on Zenodo in October 2026 with an overview volume. Two of the works specify a reasoning architecture --- a core that holds mathematical worlds as typed, versioned and verifiable objects, and a kernel that reasons inside such worlds by sites, sheaves and descent. Five apply one method, recursive mathematical discovery, to the Riemann Hypothesis, the conjecture of Birch and Swinnerton-Dyer, the Hodge conjecture, the abc conjecture and the Langlands programme, and record what it proves, what it reduces to stated hypotheses and what it leaves open. This paper describes the architecture, the five research subjects, the method, the published corpus and the open process by which the works are to be reviewed and continued. None of the works claims a proof of any of these conjectures; they are first drafts and have not been peer-reviewed.
}

\section{Introduction}\label{introduction}

A system that reasons about mathematics must settle what it stores, what it may assert, and who may turn an assertion into a result. The Grothendieckian Programme is a series of works that answers these questions by design and then tests the answers on hard problems. The Series Note of its five research subjects states the aim in one sentence: ``The Programme has a single research aim: machine intelligence that discovers mathematical structure on its own account.'' {[}S03, p.~iv{]} The method is modelled on Grothendieck's image of the rising sea {[}McL07{]}: ``A hard problem is not attacked where it stands; a theory is raised around it until the problem becomes natural and gives way.'' {[}S03, p.~iv{]}

The Programme consists of seven works and an overview volume {[}S00{]}, released on Zenodo between 20 and 26 October 2026 (\figref{programme}). Two of the works specify a reasoning architecture. The other five each take one named problem as research subject and record what the method establishes about it, what it reduces to stated hypotheses and what it leaves open. The works sit beside four bodies of existing work: machine-guided discovery, in which an external evaluator stands outside the generator {[}DVB+21; RBN+24; TWL+24{]}; formal verification under the de Bruijn criterion {[}BW05{]}, with Lean and Mathlib {[}MU21; mC20{]} and public collections of formally stated open problems {[}FLM+26{]}; structured representations in machine learning, among them sheaf neural networks {[}HG19; BDCLB22{]}; and the practice of mathematics, from proofs and refutations {[}Lak76{]} to the debate on how speculative mathematics should be labelled {[}JQ93; Thu94{]}.

This paper describes the Programme as published: the architecture (Section 2), the five research subjects (Section 3), the method and its discipline of reporting (Section 4), the series and its records (Section 5), the research plan and the ways to take part (Section 6), and the limits of what has been done (Section 7). It is the first of three papers released together. The second, \emph{The Rising-Sea Theses} {[}Liu26b{]}, states twelve theses on which the works rest, each with the passages that support it and an observation that would refute it. The third, \emph{The 57 Grothendieckian Problems} {[}Liu26c{]}, states fifty-seven open problems drawn from the works, each with a criterion that decides when it is solved. This paper adds no mathematical result to the works, and none of them claims a proof of the Riemann Hypothesis, the conjecture of Birch and Swinnerton-Dyer, the Hodge conjecture, the \(abc\) conjecture or the Langlands correspondence.

\begin{figure}[tbp]
\centering\input{fig-programme.tex}
\caption{The seven works of the Grothendieckian Programme as the seven cells of
one honeycomb {[}S00, Figure 1{]}. At the centre the core {[}S01{]};
above it, on a shared edge, the meta-reasoning kernel {[}S02{]}; around
them the five works on research subjects {[}S03; S04; S05; S06; S07{]}.
Each cell gives the formula printed on the centre cell of the work's
cover and the number of pages of its sealed PDF. The short arrows across
the shared edges are the three kinds of interface; a port marks an
interface, not a proof.}\label{fig:programme}
\end{figure}

\section{The architecture}\label{the-architecture}

\emph{The core.} \emph{GAI-MUA: The Grothendieckian Machine} {[}S01{]} is a work in six volumes with two stated obligations. The mathematical one is to explain schemes, topoi, descent, cohomology, motives and higher structures ``with exact hypotheses and source-aware proof lineage''; the architectural one is ``to express mathematical worlds as typed, versioned, provenance-bearing artifacts that can be searched, compared, formalized, computed with, and evolved without allowing statistical confidence to masquerade as proof.'' {[}S01, p.~iv{]} Volumes I and II carry the first obligation. Volume III specifies the architecture in two systems. The mathematical-universe system GMUS contains the Motivic Unification Engine (MUE), a structured carrier for geometric, cohomological and realisation data; the Topos Reasoning Engine (TRE), whose two engines propose new worlds and reason in admitted ones; and a source-audited research lane (GRA). The language system GMLS contains a language forge for notation and theory, a contextual cognitive layer, a descent workflow (GDRA) executed by capability-limited agents, and an experimental calculus (AURORA). Volumes IV--VI specify algorithms, services and evaluation. The work distinguishes seven kinds of statement --- ``Established mathematics, structural synthesis, proposed definitions, research programs, conjectures, proof obligations, and disputed claims'' --- and admits a theorem to the established layer ``only with a checked statement, complete hypotheses, an exact locator, and a recorded dependency closure.'' {[}S01, p.~iv{]}

\emph{The kernel.} \emph{GM-Omega-Infinity: Topos-Native Intelligence} {[}S02{]}, in five volumes, states what a reasoning kernel must be if it is to reason inside such worlds. A context is presented as a site, what it supports as a sheaf and a conclusion as a global section; the kernel covers, assigns, transports, glues, obstructs, decides by Kripke--Joyal forcing and changes base. Every claim in its claim ledger carries a licence grade and a falsification condition {[}S02, §1.2.6, p.~22{]}. Among the results on which the design rests are a dichotomy for the holonomy of orthogonal cellular sheaves {[}S02, §1.2.4{]} and an identity: the advantages used by group-relative policy optimisation (GRPO) are the degree-zero Laplacian of the rollout nerve applied to the reward {[}S02, Preface, p.~xiv{]}. The work states its position once: ``It has several proved local specialisations and no proved global subsumption or replacement result.'' {[}S02, p.~xxvii{]} And it states what has been done: ``the mathematics is written and partly proved, one finite instance has been computed, and nothing has been trained or measured.'' {[}S02, §1.2.6, p.~23{]}

\emph{Interfaces.} In \figref{programme} the kernel sits above the core on a shared edge, because it reasons over the worlds the core holds. Three kinds of interface cross the shared edges: worlds and their transports leave the core; descent reasoning and verification come from the kernel; obstructions, new structures and new conjectures return to the core {[}S00, Figure 1{]}. A port on an edge marks an interface, not a proof: nothing that crosses it is promoted by crossing.

\section{The five research subjects}\label{the-five-research-subjects}

Each of the other five works is a self-contained system and one research subject of the Programme, that is, ``a problem on which this method is carried through in full, with every step recorded in a form that a mathematician can check and a machine can execute.'' {[}S03, p.~iv{]} Four of them say that the recursion changes the object rather than the bridge, the argument, the inequality or the statement {[}S04, p.~v; S05, p.~v; S06, p.~v; S07, p.~v{]}; the first replaces a positivity condition by an index condition {[}S03, p.~xv{]}. Each tests its steps against the cases in which the answer is known and ends by stating where the recursion stops. Table 1 gives, for each, the key change, the state in which the recursion ends, and the boundary of the work's claims in its own words. The open items in its third column are the starting points of Section 6.

\begingroup\small\setlength{\tabcolsep}{4pt}

\begin{longtable}[]{@{}
  >{\raggedright\arraybackslash}p{(\linewidth - 6\tabcolsep) * \real{0.1684}}
  >{\raggedright\arraybackslash}p{(\linewidth - 6\tabcolsep) * \real{0.2526}}
  >{\raggedright\arraybackslash}p{(\linewidth - 6\tabcolsep) * \real{0.3053}}
  >{\raggedright\arraybackslash}p{(\linewidth - 6\tabcolsep) * \real{0.2737}}@{}}
\caption{The five research subjects. Quotation marks enclose the words of the work on the page cited.}\tabularnewline
\toprule\noalign{}
\begin{minipage}[b]{\linewidth}\raggedright
Work and subject
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
The key change
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Where the recursion ends
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Boundary, in the work's words
\end{minipage} \\
\midrule\noalign{}
\endfirsthead
\toprule\noalign{}
\begin{minipage}[b]{\linewidth}\raggedright
Work and subject
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
The key change
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Where the recursion ends
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Boundary, in the work's words
\end{minipage} \\
\midrule\noalign{}
\endhead
\bottomrule\noalign{}
\endlastfoot
\emph{Arithmetic Spectral Descent} {[}S03{]}: the Riemann Hypothesis & ``the replacement of a positivity condition by an index condition'' {[}S03, p.~xv{]}; four published counter-models test every mechanism & ``a proved conditional chain, twenty-three scoped obstructions, a certified computation stack, and two obligations stated precisely enough to be attacked, rejected or falsified'' {[}S03, p.~iv{]} & ``The Riemann Hypothesis remains open. This work does not claim a proof of it, of the generalized Riemann hypotheses, or of any equivalent statement.'' {[}S03, p.~iv{]} \\
\emph{Fractured Adelic Geometry} {[}S04{]}: the conjecture of Birch and Swinnerton-Dyer & one arithmetic spectrum with one determinant line; the conjecture as ``the agreement of the line's two trivialisations'' {[}S04, p.~v{]} & ``a register of twelve conjectures with stated difficulty, an atlas of fourteen obstructions with attack plans, a computational and formal-verification architecture, and a staged construction programme with explicit criteria for abandonment'' {[}S04, p.~v{]} & ``The Birch and Swinnerton-Dyer conjecture remains open. This work does not prove it, proves no case of it that was not already known'' {[}S04, p.~v{]} \\
\emph{The Archimedean Prism} {[}S05{]}: the Hodge conjecture & algebraicity as ``a descent datum that a class carries along a prism'' {[}S05, p.~v{]} & ``a master equivalence of five formulations, a ledger of nine obstructions of which exactly two are live, a computational and formal-verification architecture, eleven named falsifiers, and sixty problems'' {[}S05, p.~v{]} & ``The Hodge conjecture remains open. This work does not prove it, and proves no case of it that was not already known.'' {[}S05, p.~v{]} \\
\emph{Strained Prismatic Geometry} {[}S06{]}: the \(abc\) conjecture & a substrate over which \(\operatorname{Spec}\mathbb Z\) ``acquires a relative cotangent direction'', bad reduction read ``as strain in that direction'' {[}S06, p.~v{]} & Theorems A and B, ``both conditional on a named ledger of ninety-eight obligations''; Theorem C, ``an unconditional categorical theorem of trace invariance'' {[}S06, p.~v{]}; fourteen obstructions; twenty-two critical experiments & ``The \(abc\) conjecture remains open. This work does not prove it.'' {[}S06, p.~vi{]} \\
\emph{The Arithmetic Topos} {[}S07{]}: the Langlands programme & a global arithmetic curve carrying ``a six-functor formalism with a primitive trace'' {[}S07, p.~v{]} & ``a statement ledger of one hundred and eleven items, twenty-eight axioms and eighty-three entries, fifty-three of them conjectural'' {[}S07, p.~v{]}; seventeen falsification tests; four gaps of the first rank of difficulty; fourteen research problems in dependency order & ``This work does not prove the Langlands correspondence, and no case of its Main Conjecture is established unconditionally in it'' {[}S07, p.~vi{]} \\
\end{longtable}

\endgroup

\section{The method and its discipline}\label{the-method-and-its-discipline}

The method is called recursive mathematical discovery. In the words of the Series Note, ``a proposed structure is tested, what survives the test is abstracted into a new setting, and the question is posed again in that setting.'' {[}S03, p.~iv{]} \figref{method} draws the cycle. The tests are fixed before the construction is judged: four published counter-models for every mechanism proposed for the Riemann Hypothesis {[}S03, p.~iv{]}; divisors, dimension at most three, cubic fourfolds and abelian surfaces for the Hodge conjecture {[}S05, p.~v{]}; the function-field case, the de Rham limit, the local fields, the abelian case and the curve of conductor eleven for the Langlands programme {[}S07, p.~v{]}.

What does not survive a test is kept, in a form that can be used again. In {[}S03{]} ``A mechanism that failed for a structural reason became a no-go theorem'' {[}S03, p.~iv{]}; in {[}S04{]} and {[}S05{]} what fails ``is recorded as an obstruction'' {[}S04, p.~v{]}; in {[}S06{]} ``What fails is recorded as a proof obligation.'' {[}S06, p.~v{]}; in {[}S07{]} ``What fails is recorded where it fails.'' {[}S07, p.~v{]}

Every work prints a status with each statement, and the Series Note of each of the five research subjects states the same rule: ``No result is presented at a strength greater than its proof.'' {[}S03, p.~iv; S07, p.~vi{]} The notations differ. {[}S01{]} distinguishes the seven kinds of statement quoted above; {[}S02{]} grades the licence of each claim; {[}S03{]} marks every substantive claim with one of six labels {[}S03, p.~v{]}; {[}S04{]} and {[}S05{]} use four, KNOWN, CONDITIONAL, NEW and OPEN {[}S04, p.~v; S05, p.~v{]}; {[}S06{]} adds REPROVED and DISPUTED {[}S06, p.~vi{]}; {[}S07{]} uses five marks, of which DESIGN carries no truth claim and FORMAL TARGET marks a statement written for a proof assistant and not yet checked by one {[}S07, p.~vi{]}. Status attaches to the parts of an argument separately: in {[}S03{]} an open premise together with a proved implication ``yields an open route to RH, not a theorem of RH.'' {[}S03, p.~v{]}

\begin{figure}[tbp]
\centering\input{fig-method.tex}
\caption{Recursive mathematical discovery, as the Series Note of the five works
states it: a structure is proposed, tested against the cases in which
the answer is known, abstracted into a new setting if it survives, and
the question is posed again there. What does not survive is kept. Below,
the status labels with which each work reports its results.}\label{fig:method}
\end{figure}

\section{The series and its records}\label{the-series-and-its-records}

The seven works comprise 34 volumes, 26,021 pages and 995 chapters. Counted by two independent methods on their sources and on the sealed PDFs, and taking the smaller count where the two differ, they contain more than 349,000 formulas, more than 10,500 numbered statements (theorems, propositions, lemmas, corollaries, definitions and conjectures), 714 numbered algorithms and 1,434 numbered figures and plates {[}S00{]}. These numbers measure size, not correctness.

All eight works are released as Research Architecture Edition 1, version 1.0.0, under the Creative Commons BY-NC-ND 4.0 licence (\figref{series}). Each has a Zenodo record with a concept DOI that resolves to every version and a version DOI for the edition, a public GitHub repository holding the release files, and a signed list of the checksums of its files, so that a correction can name the exact edition it corrects. The records are collected in the Zenodo community \emph{The Grothendieckian Programme}, and the author's records are linked to an ORCID iD. The overview volume {[}S00{]} gives five routes through the works, for a first reading and for mathematical, machine-reasoning, formal and sceptical readers {[}S00, Table 4{]}.

\begin{figure}[tbp]
\centering\input{fig-series.tex}
\caption{The series and its records. Above, the eight works in the order of their
release, with the date, the number of volumes and pages, the concept DOI
and the repository of each. Below, the three papers released together
and the repository of the problems, through which solutions and
corrections are submitted and recorded.}\label{fig:series}
\end{figure}

\section{Research plan and taking part}\label{research-plan-and-taking-part}

The plan is the one the works state. Each ends with what it leaves open, stated precisely enough to be taken up (Table 1, third column); {[}S01{]} and {[}S02{]} leave specifications to be implemented and experiments to be run {[}S01, Vol. III; S02, p.~xvi{]}. The second work names the contributions that would count, and the overview volume applies them to every work {[}S00{]}: ``Three kinds of contribution would matter most.'' The first is refutation --- ``a counterexample to a theorem, a failure of a stated degeneration, or an experiment in which a module fails the gate it names''; the second is completion, since ``the obligations printed as open are stated precisely enough to be taken up''; the third is construction, an implementation run against a programme fixed in advance {[}S02, p.~xvi{]}.

The process is public. The third of the papers released together selects fifty-seven of the open items, each with a statement, its source and page, the status the source gives it, a literature check and a criterion that decides when it is solved. Each has its own thread in the repository of the papers, where a solution, a partial result, a counterexample, a report that a problem is already solved, or a correction can be submitted. A solution that meets its criterion is recorded under the solver's name in the next version of the papers and in the next edition of the work from which the problem comes; corrections are listed with the version in which they are made. The works keep their own instruments: ``Corrections are welcome and will be maintained in a public errata.'' {[}S05, p.~xix{]} No date is set for the next editions.

\section{Limits}\label{limits}

None of the seven works claims a proof of the conjectures that are its research subjects; each states its boundary in its first pages (Table 1). The works are first drafts and have not been peer-reviewed. Much of the architecture is specified and not implemented: Volume III of {[}S01{]} is a specification, and {[}S02{]} reports that nothing has been trained or measured. Lean verification of the works is incomplete. The counts of Section 5 are of the published sources and PDFs. The declaration below states how AI tools were used in the preparation of the works and of this paper.

\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 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 volume, each with a Zenodo DOI given in the references. The sources of this paper, its figures with their data and source code, and the scripts that checked it and the records of the checks 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 volume 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; the image of the rising sea is his, as reported in {[}McL07{]}.

\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

{[}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

{[}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

{[}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

{[}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

{[}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

{[}JQ93{]} Arthur Jaffe and Frank Quinn, \emph{``Theoretical mathematics'': toward a cultural synthesis of mathematics and theoretical physics}, Bull. Amer. Math. Soc. (N.S.) \textbf{29} (1993), 1--13, doi:\href{https://doi.org/10.1090/S0273-0979-1993-00413-0}{10.1090/S0273-0979-1993-00413-0}.

\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

{[}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

{[}Liu26c{]} Vincent Liu, \emph{The 57 Grothendieckian Problems: Open Problems for Mathematics and Machine Reasoning from the Grothendieckian Programme}, 2026, preprint, Zenodo; the third of three papers released together, doi:\href{https://doi.org/10.5281/zenodo.23734426}{10.5281/zenodo.23734426}.

\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

{[}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

{[}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

{[}Thu94{]} William P. Thurston, \emph{On proof and progress in mathematics}, Bull. Amer. Math. Soc. (N.S.) \textbf{30} (1994), 161--177, doi:\href{https://doi.org/10.1090/S0273-0979-1994-00502-6}{10.1090/S0273-0979-1994-00502-6}.

\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}.

\end{RSreferences}

\end{document}