1 Introduction

1.1 The principal open problem

In the synthesis paper concluding our prior series , which builds on Riemann’s foundational 1859 paper , we surveyed six topics where homotopy type theory (HoTT) interfaces — or fails to interface — with mainstream twenty-first century mathematics. Topics 1, 3, 4, 5, and 6 (cohesive geometry, $\infty$-toposes, derived algebraic geometry, motives, and condensed algebra) admit varying degrees of HoTT formulation. Topic 2, analytic number theory, does not. We wrote:

Algebraic number theory and parts of arithmetic geometry — schemes, sheaves, étale cohomology — admit $(\infty ,1)$-topos and condensed mathematics treatments that connect cleanly to univalent foundations. But $\zeta (s)=0$ as a HoTT-native statement, with $\zeta$ a HoTT-native object, remains unrealised. We frame this as the principal open question for the synthesis.

This paper develops that question.

1.2 Why $\zeta (s)=0$ is hard in HoTT

A HoTT-native statement of $\zeta (s)=0$ requires four ingredients, each of which is non-trivial:

1. A HoTT-native object ${\mathbb{C}}_{\mathsf{c}}:\mathcal{U}$ of complex numbers, complete with the notion of meromorphicity. Constructive Cauchy reals  exist, but a univalent algebraic closure that is well-behaved with respect to univalence requires care: classical algebraic closures are unique-up-to-isomorphism, while a HoTT-native one is unique up-to-equivalence in the sense of univalence .

2. A HoTT-native notion of holomorphic function $\mathsf{Holo}:({\mathbb{C}}_{\mathsf{c}}\to {\mathbb{C}}_{\mathsf{c}})\to \mathcal{U}$. The classical definition uses a metric limit (Newton quotient) which is constructive but not synthetic. A more native approach uses cohesive HoTT : holomorphicity becomes a modal predicate.

3. A HoTT-native definition of $\zeta :{\mathbb{C}}_{\mathsf{c}}\setminus \{1\}\to {\mathbb{C}}_{\mathsf{c}}$ that agrees on $\mathrm{Re}(s)>1$ with ${\sum }_{n\ge 1}{n}^{-s}$ and analytically continues elsewhere. This requires either a higher inductive-inductive construction (HIIT) or an internal universal property of meromorphic extensions.

4. A HoTT-native interpretation of the proposition $$\Pi (s:{\mathbb{C}}_{\mathsf{c}}).\zeta (s)=0\to \neg \mathsf{trivialZero}(s)\to \mathrm{Re}(s)=1/2.$$ Even getting to this statement is a research project.

By contrast, in classical foundations Loeffler and Stoll have just (March 2025) formalized in Lean 4 / Mathlib the entire infrastructure: $\zeta$, the analytic continuation, the functional equation, the Basel problem, non-vanishing on $\mathrm{Re}(s)\ge 1$, Dirichlet’s theorem on primes in arithmetic progressions, and the formal statement of the Riemann hypothesis. Their work runs to roughly 3300 lines of Lean for the analytic continuation alone. We have nothing comparable in any HoTT proof assistant.

1.3 What this paper does (and does not do)

This paper:

• Identifies and motivates the prerequisite chain for a HoTT-native $\zeta$. (2)

• Proposes three candidate HoTT-native definitions of $\zeta$, analyses their tradeoffs, and conjecturally proves their pairwise equivalence. (3)

• Places the picture in the broader geometric Langlands landscape via $(\infty ,1)$-toposes and Lurie’s higher topos theory . (4)

• Compares HoTT and Clausen–Scholze condensed mathematics, identifying where they overlap and where the bridge is missing. (5)

• Compares with the Loeffler–Stoll 2025 Lean formalization, both as a benchmark and as a translation target. (6)

• Provides a six-sub-problem roadmap that, if solved, would yield a HoTT-native proof that $\zeta (2)={\pi }^2/6$. (7)

• Re-states the Riemann hypothesis as a HoTT proposition and discusses its modal-logical structure. (8)

This paper does not:

• Prove the Riemann hypothesis.

• Provide a complete HoTT formalization of $\zeta$.

• Claim that HoTT methods will, in principle, prove RH; we are agnostic on this question.

The companion code repository contains a Haskell implementation of partial zeta sums, Dirichlet series operations, the formal Euler product identity (modulo a convergence axiom), and a Lean 4 sketch indexed against Loeffler–Stoll’s Mathlib code.

1.4 Algebraic vs. analytic number theory

A clarifying distinction. Algebraic number theory studies ${\mathcal{O}}_K$, the ring of integers of a number field $K/\mathbb{Q}$, its ideals, class group, units, and reductions modulo primes. The objects are discrete-finite or, at worst, countable; their morphisms are algebraic; and the topology is the Zariski or étale one. HoTT formalisation is straightforward in principle: rings are sets with operations satisfying identities, and ideals are subsingletons of the underlying set.

Analytic number theory studies $\zeta (s)$, Dirichlet $L$-functions $L(s,\chi )$, and automorphic $L$-functions $L(s,\pi )$, where $\pi$ is an automorphic representation of $GL(n,{\mathbb{A}}_{\mathbb{Q}})$. The objects are holomorphic / meromorphic functions of complex variables; morphisms are analytic transformations; and the topology is the Euclidean (or condensed) topology on $\mathbb{C}$. HoTT formalisation is presently absent.

The Langlands programme  unifies these worlds: it asserts a precise correspondence between automorphic representations and Galois representations, transforming questions about zeros of $L$-functions into questions about Galois cohomology. Geometric Langlands  is the function-field analogue and was proven in 2024 in five papers using $(\infty ,1)$-categorical methods throughout.

1.5 Outline

2 traces the prerequisite chain. 3 defines $\zeta$ as a candidate HoTT object. 4 treats geometric Langlands in $(\infty ,1)$-topoi. 5 compares condensed mathematics and HoTT. 6 compares with Loeffler–Stoll Lean. 7 gives the six-sub-problem roadmap. 8 discusses RH as a HoTT statement. 10 concludes.

2 The Prerequisite Chain

We trace, with care, the dependency chain culminating in a HoTT-native $\zeta$.

2.1 HoTT-native real numbers ${\mathbb{R}}_{\mathsf{c}}$

2.2 HoTT-native complex numbers ${\mathbb{C}}_{\mathsf{c}}$

There are at least three approaches:

2.2.0.1 Pairs.

${\mathbb{C}}_{\mathsf{c}}:={\mathbb{R}}_{\mathsf{c}}\times {\mathbb{R}}_{\mathsf{c}}$ with multiplication $(a,b)(c,d):=(ac-bd,ad+bc)$. Simple, but does not capture the universal property that ${\mathbb{C}}_{\mathsf{c}}$ should be an algebraic closure of ${\mathbb{R}}_{\mathsf{c}}$.

2.2.0.2 Algebraic closure of ${\mathbb{R}}_{\mathsf{c}}$.

2.2.0.3 Quotient construction.

${\mathbb{C}}_{\mathsf{c}}:={\mathbb{R}}_{\mathsf{c}}[X]/(X^2+1)$. Concretely realisable via Schwartz / set-quotient.

In what follows, we treat ${\mathbb{C}}_{\mathsf{c}}$ axiomatically: a propositional Univalent Algebraic Closure of ${\mathbb{R}}_{\mathsf{c}}$, equipped with a continuous structure inherited from ${\mathbb{R}}_{\mathsf{c}}\times {\mathbb{R}}_{\mathsf{c}}$.

2.3 Holomorphic functions in HoTT

The classical definition of holomorphicity is: $$f:\mathbb{C}\to \mathbb{C}\text{ is holomorphic at }z\text{iff}\underset{h\to 0}{\lim }\frac{f(z+h)-f(z)}{h}\text{ exists.}$$ This translates straightforwardly to ${\mathbb{R}}_{\mathsf{c}}$- and ${\mathbb{C}}_{\mathsf{c}}$-limits, but is not HoTT-native in the sense of using only $\mathcal{U}$, $=$, and the universe-polymorphic constructors.

2.4 Dirichlet series

2.5 Putting it together

The chain in 1 terminates at $\zeta$, but the rightmost arrow — analytic continuation from a Dirichlet series convergent on $\mathrm{Re}(s)>1$ to a meromorphic function on ${\mathbb{C}}_{\mathsf{c}}\setminus \{1\}$ — has no canonical HoTT-native realisation. This is the central technical gap of the present paper.

2.6 Detailed account of analytic-continuation obstacles

To clarify why the rightmost arrow is hard, we list the obstacles in ascending order of severity.

1. Unique factorisation of meromorphic extension. In classical complex analysis, the identity theorem (19) guarantees uniqueness of analytic continuation. In HoTT, “connected open” needs a precise definition, and the proof that the agreement locus is clopen requires constructive analogues of Bolzano–Weierstrass.

2. Existence of meromorphic extension. Classical proofs of analytic continuation of $\zeta$ use one of:

   • Hurwitz zeta method: define $\zeta (s,a)={\sum }_{n\ge 0}(n+a{)}^{-s}$ and continue via the integral representation. This requires Mellin transform.

   • Theta-function method: $\theta (t):={\sum }_{n\in \mathbb{Z}}{e}^{-\pi n^{2}t}$ satisfies modular invariance, and Mellin transforming gives $\zeta$.

   • Contour integral method: integrate $\frac{x^{s-1}}{e^x-1}$ around a Hankel contour.

   Each requires a substantial fragment of HoTT-native analysis: integration theory, modular transformation laws, residue calculus.

3. Computation in HoTT. Even given the existence and uniqueness, computing $\zeta$ at, say, $s=-1$ to obtain $\zeta (-1)=-1/12$ requires either (i) symbolic manipulation of the analytic continuation, or (ii) numerical methods. HoTT proof assistants like Cubical Agda do not currently support efficient arbitrary-precision real arithmetic.

4. Naturality. Classical proofs treat $\zeta$ as one specific function. A fully-categorified HoTT-native account would treat $\zeta$ as part of a family — Dirichlet $L$-functions, Hurwitz zeta, Hecke $L$-functions, automorphic $L$-functions — with naturality with respect to characters and lifts. This expands the existence obstacle by a constant factor of the size of the family.

2.7 HoTT-native Cauchy reals: explicit example

To make the discussion concrete, we sketch how $\sqrt{2}:{\mathbb{R}}_{\mathsf{c}}$ is a HoTT-native object.

These three examples illustrate that named real-number constants in HoTT require an algorithmic Cauchy modulus, not just an existential statement.

3 The Riemann Zeta Function as a HoTT Object

We now propose three approaches to defining $\zeta$ inside HoTT.

3.1 Approach 1: $\zeta$ as a higher inductive-inductive type

Inspired by the construction of ${\mathbb{R}}_{\mathsf{c}}$ as a HIIT, we sketch a specification pattern for what a HoTT-native $\zeta$ should satisfy. We emphasise that what follows is a wish-list of constructors, not a self-contained HIIT definition; both consistency and existence of such a HIIT are open questions.

First, define the convergent partial-sum function on the half-plane of absolute convergence: $$\begin{array}{c}\text{label}eq:zetaSeries{\zeta }_{\mathrm{series}}:\Pi (s:{\mathbb{C}}_{\mathsf{c}}).\mathrm{Re}(s)>1\to {\mathbb{C}}_{\mathsf{c}},{\zeta }_{\mathrm{series}}(s):=\sum _{n=1}^{\infty }{n}^{-s}.\end{array}$$ This map is well-defined because $\mathrm{Re}(s)>1$ ensures absolute convergence of the series in ${\mathbb{C}}_{\mathsf{c}}$, and the limit is the (HoTT-native) limit constructor of ${\mathbb{R}}_{\mathsf{c}}$ applied component-wise.

3.2 Approach 2: $\zeta$ as analytic limit of Euler product

Recall the Euler product (): $$\zeta (s)=\prod _{p\text{ prime}}\frac{1}{1-p^{-s}},\mathrm{Re}(s)>1.$$

3.3 Approach 3: $\zeta$ via universal property of meromorphic continuation

3.4 Equivalence of the three definitions

3.5 The functional equation

3.6 The critical strip

We will analyse this statement modal-logically in 8.

3.7 Worked example: $\zeta (2)={\pi }^2/6$

To illustrate what HoTT-native machinery is needed, we trace one of the oldest results — the Basel problem.

4 Geometric Langlands in $(\infty ,1)$-Topoi

4.1 Brief history

The Langlands programme  predicts a correspondence $$\{\text{automorphic reps of }GL(n,{\mathbb{A}}_F)\}⟷\{\text{n-dim Galois reps of }\mathrm{Gal}(\overline{F}/F)\}$$ for a global field $F$. The number-field case ($F$ a number field) is analytic in nature; the function-field case ($F={\mathbb{F}}_q(X)$ for a curve $X$) is geometric, hence the name geometric Langlands.

Geometric Langlands has a categorical formulation due to Beilinson–Drinfeld and Frenkel–Gaitsgory: the conjecture is the existence of an equivalence $$\mathsf{D}\text{-mod}({\mathsf{Bun}}_G(X))\simeq \mathsf{QCoh}({\mathsf{LocSys}}_{G^{\vee }}(X))$$ of $(\infty ,1)$-categories, where $G$ is a reductive group, ${\mathsf{Bun}}_G$ its moduli stack of $G$-bundles, $G^{\vee }$ the Langlands dual, and $\mathsf{LocSys}$ the de Rham moduli of local systems. This was proven in 2024 by Gaitsgory, Raskin, Rozenblyum, Arinkin, Beraldo, Chen, Cheng, Faergeman, Lin, Lysenko in five papers , awarded the 2025 Breakthrough Prize.

4.2 $(\infty ,1)$-categories vs. HoTT

By Lurie’s higher topos theory  and higher algebra , $(\infty ,1)$-categories admit a model in simplicial sets (quasi-categories). Cisinski et al.  have begun a programme of type-theoretic foundations of $(\infty ,1)$-category theory in which $(\infty ,1)$-categories are types satisfying a Segal condition.

By Shulman’s theorem , every $(\infty ,1)$-topos $\mathcal{X}$ admits HoTT as its internal language. Hence, in principle, the Gaitsgory equivalence is statable in HoTT internally to a fixed $(\infty ,1)$-topos.

4.3 Geometric vs. analytic Langlands

The 2024 proof is geometric: it lives in the world of moduli stacks over ${\mathbb{F}}_q$-curves or, in characteristic 0, over $\mathbb{C}$-curves with the de Rham stack (cf.  for the complex-analytic side). It says nothing directly about $\zeta$ or about analytic number theory.

The analytic Langlands programme (Etingof–Frenkel–Kazhdan ) attempts a Hilbert-space variant: the $L^2$-spectrum of certain operators on ${\mathsf{Bun}}_G(\mathbb{C}\text{-curve})$ should match a spectral side built from ${\mathsf{LocSys}}_{G^{\vee }}$. This is the program closer to $\zeta (s)=0$, but it is much less developed than the geometric version.

4.4 Implication for HoTT-native analytic NT

If a HoTT-native analytic Langlands programme could be developed, then $\zeta (s)=0$ would translate to a statement about the spectrum of an operator on ${\mathsf{Bun}}_G(\mathbb{Q})$, which is at least syntactically a HoTT statement modulo standard moduli-stack constructions. We do not develop this direction in detail; we flag it as a concrete research direction.

4.5 Detailed example: $GL(1)$ Langlands and Hecke characters

The simplest case of Langlands is $G=GL(1)$, and even this case shows where HoTT-native infrastructure is needed.

4.6 Geometric Langlands as an internal HoTT statement

We give a more precise version of the Gaitsgory equivalence as a HoTT internal statement. Let $\mathcal{X}$ be the $(\infty ,1)$-topos of derived algebraic stacks over $\mathbb{C}$. By Shulman , $\mathcal{X}$ has an internal language extending HoTT (after fixing a universe-of-types issue).

This is conjectural in the sense that we have not verified all the type-theoretic encodings; the underlying mathematical content is theorem (Gaitsgory et al. 2024).

4.7 Physical interpretation: 4d $\mathcal{N}=4$ super-Yang–Mills

Kapustin and Witten  interpreted geometric Langlands as electric–magnetic duality (S-duality) of 4d $\mathcal{N}=4$ super-Yang–Mills compactified on a Riemann surface. This physical perspective suggests:

• A HoTT-native treatment of 4d $\mathcal{N}=4$ super-Yang–Mills via synthetic differential cohesive HoTT .

• S-duality as an automorphism of the underlying type; eigenvalues of S-duality giving the spectrum.

• Connection to the synthesis paper’s QFT formulation.

We flag this as a research direction; we do not develop it further here.

5 Condensed Mathematics and HoTT

5.1 Pyknotic / condensed sets

Clausen and Scholze  defined the condensed sets as sheaves on the site of profinite sets with finite jointly-surjective covers. Pyknotic sets, due to Barwick–Haine, are an essentially equivalent variant. The category $\mathsf{Cond}$ is a topos, and $\mathsf{Cond}(\mathrm{Ab})$ — condensed abelian groups — has much better homological properties than topological abelian groups.

The crucial example: $\mathbb{C}$ becomes a condensed ring which is analytic-friendly in a way that $\mathbb{C}$-as-topological-ring is not. The 6-functor formalism of analytic stacks (Clausen–Scholze 2024) gives a geometric foundation for analytic-number-theoretic objects.

5.2 Why this matters for $\zeta$

The condensed approach gives a uniform setting in which:

• Smooth manifolds, complex-analytic spaces, schemes, formal schemes, adic spaces, and rigid spaces all live as condensed objects.

• Cohomology operations (six functors: $f^{\ast },f_{\ast },f_{!},f^{!},\otimes ,\mathrm{Hom}$) all exist with clean adjunction structure.

• $\zeta$, viewed as a meromorphic function on $\mathbb{C}$, becomes an object in $\mathsf{Cond}(\mathrm{Ab})$-modules over a suitable condensed analytic stack.

5.3 Bridging to HoTT

33 is open; preliminary work by Mahmoudvand–Riehl and others has explored the syntactic side, but no complete bridge exists.

5.4 Solid abelian groups in HoTT, sketch

A HoTT-native version would replace “profinite set” with a HoTT-internal type (e.g., a limit of finite types in $\mathcal{U}$) and “continuous” with the appropriate cohesive-HoTT modality. We sketch a candidate:

5.5 Six-functor formalism in HoTT

The Clausen–Scholze 6-functor formalism for analytic stacks  is expressed in $(\infty ,1)$-categorical language as follows. Given a category $\mathcal{C}$ of geometric objects (analytic stacks) with two classes of morphisms “proper” $\mathsf{P}$ and “open” $\mathsf{O}$, a 6-functor formalism consists of:

• A symmetric monoidal $(\infty ,1)$-category $\mathcal{D}(X)$ for each $X\in \mathcal{C}$, of $\infty$-sheaves on $X$.

• For each morphism $f:X\to Y$ in $\mathcal{C}$, an adjunction $f^{\ast }⊣f_{\ast }:\mathcal{D}(Y)\rightleftarrows \mathcal{D}(X)$.

• For each $f$ in $\mathsf{P}\cup \mathsf{O}$, an additional pair $f_{!}⊣f^{!}:\mathcal{D}(X)\rightleftarrows \mathcal{D}(Y)$.

• Coherent base change, projection formula, and proper / open recollement.

A successful resolution of 37 would, indirectly, give a HoTT framework for analytic objects (including $\zeta$ as a section of a suitable line bundle).

5.6 Solid modules over $\mathbb{Z}$ and $p$-adic interaction

In condensed mathematics, the category of solid abelian groups ${\mathrm{Solid}}_{\mathbb{Z}}$ contains $p$-adic objects naturally: $${\mathbb{Z}}_p\in {\mathrm{Solid}}_{\mathbb{Z}},{\mathbb{Q}}_p\in {\mathrm{Solid}}_{\mathbb{Z}},{\mathbb{C}}_p\in {\mathrm{Solid}}_{\mathbb{Z}}.$$ For ${\mathbb{Z}}_p$, the topology comes from the profinite structure ${\mathbb{Z}}_p={\underleftarrow{\lim }}_n\mathbb{Z}/p^n$. For ${\mathbb{C}}_p$, completing the algebraic closure of ${\mathbb{Q}}_p$ uses metric completion plus algebraic closure plus completion again — this is awkward classically and equally awkward in HoTT.

6 Comparison with Loeffler–Stoll Lean Formalization

6.1 What Loeffler–Stoll have

The 2025 paper  formalizes in Lean 4 / Mathlib:

1. The Riemann zeta function $\zeta$ via Hurwitz zeta and analytic continuation, $\sim$ 3300 lines.

2. Dirichlet $L$-functions $L(s,\chi )$ for primitive characters $\chi$.

3. The Euler product $\zeta (s)={\prod }_p(1-p^{-s}{)}^{-1}$ on $\mathrm{Re}(s)>1$.

4. Analytic continuation via Mellin / theta-function method.

5. The functional equation $\zeta (1-s)=2(2\pi {)}^{-s}\Gamma (s)\cos (\pi s/2)\zeta (s)$.

6. Basel: $\zeta (2)={\pi }^2/6$.

7. Non-vanishing on $\mathrm{Re}(s)\ge 1$.

8. Dirichlet’s theorem on primes in APs.

9. Formal statement of the Riemann hypothesis:

   def RiemannHypothesis : Prop :=
     ∀ s : ℂ, riemannZeta s = 0 → ¬ trivialZero s → s.re = 1 / 2

This is roughly $10^4$ lines total across the relevant Mathlib files.

6.2 What Lean / Mathlib provides that HoTT lacks

• Classical $\mathbb{C}$ as a complete normed field, with Cauchy integrals.

• Mathlib’s Complex.differentiable, HolomorphicAt, ContourIntegral.

• Mellin transforms, Gamma function, Riemann zeta function (ZetaFunction in Mathlib).

• All of measure theory, including Lebesgue integration on $\mathbb{C}$.

6.3 What HoTT could offer

• Univalence: the multiple definitions of $\zeta$ (14, 16, 20) become propositionally equal via univalence, not merely equal up to some isomorphism.

• Higher inductive types: the Riemann surface of $\zeta$ (or of $L$-functions) is naturally a HIT, capturing branch-cut data syntactically.

• Internal $(\infty ,1)$-topos language: the Langlands functor and its adjoints can be expressed in the same language as the underlying analytic objects.

6.4 Strategy: HoTT as classical-foundation transport

A pragmatic approach: transport the Loeffler–Stoll Lean formalization to HoTT not by re-doing all the analysis, but by treating $\mathbb{C}$ axiomatically as a HoTT type with the same operations and properties as Mathlib’s $\mathbb{C}$. We sketch this in 7.

6.5 Code-level comparison: signature against signature

To make the comparison tangible, we present the key Lean signatures from Loeffler–Stoll alongside conjectured HoTT analogues.

6.5.0.1 The zeta function itself.

In Mathlib (Loeffler–Stoll):

noncomputable def riemannZeta : ℂ → ℂ

In HoTT (proposed): $$\zeta :{\mathbb{C}}_{\mathsf{c}}\setminus \{1\}\to {\mathbb{C}}_{\mathsf{c}}\text{(with explicit pole at s=1)}.$$ Here Lean uses “noncomputable” to encode that $\zeta$ is defined by non-effective analytic continuation. HoTT, lacking a built-in concept of “noncomputable”, must encode this via a propositional truncation.

6.5.0.2 The functional equation.

In Mathlib:

theorem riemannZeta_one_sub : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 →
  riemannZeta (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s
                      * cos (π * s / 2) * riemannZeta s

HoTT analogue (proposed): exactly the corresponding $\Pi$-statement, modulo the conditional $s\ne 0\wedge s\ne 1$.

6.5.0.3 Non-vanishing on $\mathrm{Re}(s)\ge 1$.

In Mathlib:

theorem riemannZeta_ne_zero_of_one_le_re :
  ∀ (s : ℂ), 1 ≤ s.re → s ≠ 1 → riemannZeta s ≠ 0

HoTT analogue: same statement; the proof uses the Euler product (no analytic continuation), so should be tractable HoTT-natively.

6.5.0.4 Riemann hypothesis.

In Mathlib:

def RiemannHypothesis : Prop :=
  ∀ s : ℂ, riemannZeta s = 0 → ¬ trivialZero s → s.re = 1 / 2

HoTT analogue: 25.

6.6 Quantitative comparison

7 Six Sub-Problems for HoTT-Native $\zeta$

We propose six concrete sub-problems whose collective resolution would yield a HoTT-native proof of $\zeta (2)={\pi }^2/6$ and a formal HoTT statement of the Riemann hypothesis.

Sub-problem 1: HoTT-native ${\mathbb{C}}_{\mathsf{c}}$ with full algebraic-closure axiom

Status: partially done in HoTT Book setting; algebraic closure not yet done.

Sub-problem 2: HoTT-native holomorphic functions

Status: possible by direct constructive analysis. Estimated effort: $\sim$5000 lines of Agda or Cubical Agda.

Sub-problem 3: HoTT-native Dirichlet series machinery

Status: our companion Haskell code provides a finite-precision prototype; HoTT formalisation pending.

Sub-problem 4: HoTT-native analytic continuation

Status: this is the key technical bottleneck.

Sub-problem 5: HoTT-native functional equation

Status: requires 41–44 first.

Sub-problem 6: HoTT-native formal RH statement

Status: doable now (25), modulo 41–44.

7.1 Composition diagram

7.2 Estimated effort and milestones

• 41: $\sim$1000 lines, 1–2 graduate-student-years.

• 42: $\sim$5000 lines, 2–3 g-s-y.

• 43: $\sim$1500 lines, 1 g-s-y.

• 44: $\sim$3000 lines, 2–3 g-s-y; key conceptual work.

• 45: $\sim$5000 lines, 2 g-s-y.

• 46: $\sim$200 lines, weeks. The hard part is the infrastructure, not the statement.

Total: $\sim$15000 lines, 8–12 graduate-student-years. Comparable to the total effort behind Loeffler–Stoll plus its Mathlib dependencies.

8 Open Conjectures: Riemann Hypothesis as a HoTT Statement

8.1 Modal-logical status of RH in HoTT

25 states $\Pi (s:{\mathbb{C}}_{\mathsf{c}}).P(s)\to Q(s)$, where $P$ and $Q$ are propositions. By the propositional structure, $\mathrm{RH}$ is itself a proposition (in HoTT-Set sense, an $(-1)$-truncated type).

In particular, $\mathrm{RH}$ is either inhabited or empty; we cannot have “two non-equivalent proofs” of RH. This is in contrast to a structural statement like “the type of complex numbers admits an algebraic structure” which has no such uniqueness.

8.2 Decidability and constructivity

8.3 Connections to the Langlands programme

The Riemann hypothesis is a special case of the Generalized Riemann Hypothesis (GRH): all non-trivial zeros of all $L$-functions $L(s,\chi )$ attached to primitive Dirichlet characters $\chi$ lie on $\mathrm{Re}(s)=1/2$. The Langlands programme conjecturally extends this to automorphic $L$-functions $L(s,\pi )$.

In a HoTT framework where automorphic representations are types in a suitable $(\infty ,1)$-topos, 49 is a $\Pi \Pi \Pi$-statement — syntactically clean, semantically deep.

8.4 The von Koch theorem in HoTT

This connects the analytic statement $\mathrm{RH}$ to a discrete one. A HoTT-native proof would proceed via the explicit formula for $\pi (x)$ in terms of zeros of $\zeta$, all of which lives downstream of 41–46.

8.5 What if RH is independent of HoTT-set theory?

A speculative possibility: $\mathrm{RH}$ might be independent of (some extension of) HoTT, similar to the way the continuum hypothesis is independent of ZFC. In that case, HoTT might admit two consistent extensions: $\mathrm{HoTT}+\mathrm{RH}$ and $\mathrm{HoTT}+\neg \mathrm{RH}$. This is purely speculative and reflects no current consensus; it is offered only as a contrast with the classical view that RH “simply has a truth value”.

8.6 Density theorems and zero-free regions

Classical analytic number theory has many results about the distribution of zeros of $\zeta$ short of RH:

• Hadamard / de la Vallée-Poussin (1896): $\zeta (s)\ne 0$ on $\mathrm{Re}(s)=1$. Formalized in Lean by Loeffler–Stoll.

• Vinogradov-Korobov: explicit zero-free region $$\mathrm{Re}(s)>1-\frac{C}{(\log |t|{)}^{2/3}(\log \log |t|{)}^{1/3}}.$$

• Selberg’s density theorem: the proportion of zeros within distance $\delta$ of the critical line is $\ge 1-O({\delta }^{-1})$.

• Levinson–Conrey: at least $40\%$ of zeros are on the critical line.

Each of these is, in principle, a HoTT-native theorem once we have 41–45. In particular, the $\mathrm{Re}(s)=1$ non-vanishing requires only the Euler product and basic inequalities — no analytic continuation. This is the natural second target after 26.

8.7 Effective vs. ineffective HoTT statements

A subtle point about HoTT: some statements about $\zeta$ are naturally effective (algorithmic), while others are not.

These distinctions matter for HoTT formalization: parts of the theory are algorithmic-friendly (Cubical Agda can compute them), other parts are not.

9 Discussion

9.1 Why is analytic NT specifically hard?

Algebraic objects (rings, modules, groups, schemes) are small: their data fit on a finite page or in a computer’s memory. Analytic objects ($\mathbb{R}$, $\mathbb{C}$, holomorphic functions, contour integrals) are large in two senses:

• Type-theoretic size: ${\mathbb{R}}_{\mathsf{c}}$ is uncountable, so any property of ${\mathbb{R}}_{\mathsf{c}}$ is in some sense a $\Pi$-statement over an uncountable type.

• Logical complexity: $\zeta$ involves nested quantifiers over reals, limits of limits, integrals, and analytic continuations.

HoTT, like any type theory, is well-suited to data of small or medium complexity; encoding heavy analysis requires either substantial primitive infrastructure or a transport from a classical foundation.

9.2 Comparison: Lean Mathlib’s effectiveness

Lean Mathlib’s success at formalizing analytic NT (Loeffler–Stoll 2025) relies on:

1. Classical logic everywhere.

2. A large prebuilt library of measure theory, integration, and complex analysis.

3. Decidability assumptions where appropriate.

4. Set-theoretic ambient foundations (Lean 4 type theory is ZFC-equivalent in strength).

HoTT can match (1)–(3) at extra cost; (4) is a deeper foundational issue.

9.3 The role of cohesive / differential HoTT

Differential cohesive HoTT  extends HoTT with shape, flat, and sharp modalities. In this setting, smooth / holomorphic / meromorphic become synthetic. Examples like show that synthetic differential geometry is viable in HoTT.

A natural research direction is to lift the Loeffler–Stoll work into differential cohesive HoTT, treating $\mathbb{C}$ as a $\mathsf{S}$-modal type and $\zeta$ as a synthetic meromorphic function. This is a substantial project but appears feasible.

9.4 Limitations of this paper

• We do not give a working HoTT formalization; we give a research roadmap and partial Haskell prototypes.

• We do not prove the conjectures of 21 or 22; we sketch proofs that depend on currently-unavailable HoTT-native infrastructure.

• Our proposed bridge (33) between condensed mathematics and HoTT is open; we have not constructed the bridging $(\infty ,1)$-topos.

9.5 Future directions

1. Implement 41–43 in Cubical Agda.

2. Develop the cohesive-HoTT bridge for analytic continuation (44).

3. Translate Loeffler–Stoll Lean to HoTT-axiomatised classical $\mathbb{C}$ as a first benchmark.

4. Use the synthesis from  to attack 49 via geometric Langlands in $(\infty ,1)$-topoi.

5. Explore the analytic Langlands programme of EFK in HoTT.

9.6 Connection with directed type theory

A recent development is directed type theory (DTT) of Riehl, Shulman, Verity, North . DTT extends HoTT with a notion of directed morphism — paths that are not invertible. This gives a potential synthetic foundation for $(\infty ,1)$-categories.

Why is DTT relevant to analytic NT?

• Automorphic representations are functors, not equivalences. DTT captures functorial structure natively.

• Hecke operators on $L$-functions act as endomorphisms, not automorphisms; DTT distinguishes these.

• The Langlands functor $\sigma :\mathsf{Aut}(G{L}_n)\to \mathsf{Galois}$ is a functor between $\infty$-categories of representations; DTT gives a type-theoretic home.

9.7 Connection with synthetic algebraic geometry

Synthetic algebraic geometry  works inside HoTT internally to a Zariski (or étale) topos, and develops algebraic geometry without external schemes. The relevant facts:

• Schemes become types satisfying a Zariski-locality condition.

• Sheaf cohomology is internal cohomology.

• Group schemes, including reductive groups for Langlands, become types in the internal language.

A natural research line: use synthetic AG plus cohesion to define analytic moduli stacks, and develop $\zeta$ as an internal object.

9.8 The role of computer-checked proofs

A practical question: should we even attempt HoTT formalisation of analytic NT, given that classical Lean Mathlib is so much more advanced?

Three answers:

1. Foundational interest: HoTT and Lean differ at the foundation level. Univalence simplifies certain isomorphism / equivalence arguments. A HoTT formalisation would be qualitatively different.

2. Internal-language gain: working inside an $(\infty ,1)$-topos gives access to the topos’s internal logic. For instance, condensed mathematics has its own internal language (the Solid topos), distinct from classical set theory; HoTT might bridge these.

3. Educational value: a HoTT formalisation forces clarity about what data $\zeta$ “really is”. The exercise of distinguishing the three candidate definitions and identifying their pairwise equivalences is foundationally illuminating.

10 Conclusion

We have formulated, with technical care, the principal open problem of our prior synthesis: HoTT-native analytic number theory. The Riemann zeta function does not yet exist as a HoTT-native object; the statement $\zeta (s)=0$ is not yet a HoTT-native proposition. Closing this gap requires the prerequisite chain of 2, the candidate definitions of 3, the $(\infty ,1)$-topos perspective of 4–5, the comparison with Loeffler–Stoll Lean of 6, and the six concrete sub-problems of 7.

We do not solve the principal open problem. We formulate it precisely, show it is not vacuous, and provide enough structure for future workers to take concrete steps. The roadmap of 7 estimates 8–12 graduate-student-years to deliver a HoTT-native analogue of Loeffler–Stoll 2025. This is significant, but tractable; the much harder Riemann hypothesis itself remains untouched.

The dialogue between HoTT and analytic number theory is just beginning. Geometric Langlands has been proven (2024) using $(\infty ,1)$-categorical machinery that overlaps with HoTT’s intended models. Condensed mathematics provides a uniform setting for analytic objects. These two streams will, we conjecture, converge on a HoTT-native analytic number theory in the coming decade. This paper aims to map the territory.

11 Appendix: HoTT axioms for analytic NT

For reference, we collect the HoTT axioms / definitions that any HoTT-native analytic NT should respect. We work in MLTT with one universe $\mathcal{U}$ and the following axioms.

A.1 Univalence

$$\begin{array}{c}\text{label}eq:univ\mathsf{ua}:\Pi (A,B:\mathcal{U}).(A\simeq B)\simeq (A=B).\end{array}$$

This is the standard univalence axiom of . It implies function extensionality and propositional extensionality.

A.2 Higher inductive types

We assume HITs of the form needed in this paper:

• Cauchy reals ${\mathbb{R}}_{\mathsf{c}}$ as a HIIT (1).

• Set quotients $A/\sim$ for relations $\sim$ on $A$.

• Propositional truncation $\Vert A{\Vert }_{-1}$.

• $n$-truncations $\Vert A{\Vert }_n$.

A.3 Cohesion (optional)

For synthetic-analytic statements, cohesive HoTT adds:

• Shape modality $\mathsf{S}:\mathcal{U}\to \mathcal{U}$ (left adjoint to $♭$).

• Flat modality $♭:\mathcal{U}\to \mathcal{U}$ (right adjoint to $\mathsf{S}$).

• Sharp modality $♯:\mathcal{U}\to \mathcal{U}$.

These satisfy the cohesive triple-adjunction $\mathsf{S}⊣♭⊣♯$ and natural-transformation laws between them.

A.4 Choice (optional, classical)

For some classical analytic-NT results we may need: $$\begin{array}{c}\text{label}eq:choice\mathrm{AC}:\Pi (A:\mathcal{U}).\Pi (B:A\to \mathcal{U}).(\Pi (a:A).\Vert B(a){\Vert }_{-1})\to \Vert \Pi (a:A).B(a){\Vert }_{-1}.\end{array}$$

Equivalent to set-theoretic AC for sets. Required for classical existence of algebraic closures, classical functional equation proofs.

A.5 Excluded middle (optional, classical)

$$\begin{array}{c}\text{label}eq:lem\mathrm{LEM}:\Pi (P:\mathsf{Prop}).P+\neg P.\end{array}$$

Required for the statement of $\mathrm{RH}\vee \neg \mathrm{RH}$ as “there is a fact of the matter”.

12 Appendix: Companion code overview

The companion repository at src/langlands-analytic-number-theory/ contains:

• Main.hs — driver illustrating partial $\zeta$ sums and Dirichlet series operations.

• Zeta.hs — partial zeta computations with explicit truncation.

• Dirichlet.hs — Dirichlet series machinery, Dirichlet convolution, multiplicative functions.

• Properties.hs — QuickCheck properties for the algebraic laws on Dirichlet series.

• Proofs.hs — equational proofs of the Euler product identity, modulo a finite-truncation axiom.

The Lean component at lean/langlands-analytic-number-theory/ contains:

• Zeta.lean — a Lean 4 / Mathlib sketch indexed against Loeffler–Stoll, marking which lemmas would translate cleanly to HoTT.

These are illustrative prototypes, not formal verifications. Their purpose is to make the prerequisite chain (2) and the candidate definitions (3) executable, so that future HoTT-native work has computational benchmarks.

13 Appendix: Worked sub-roadmap for sub-problem 4

We sketch a plausible HoTT proof strategy for analytic continuation of $\zeta$, addressing 44 in more detail.

C.1 The Hurwitz integral representation

Classical analytic continuation of $\zeta$ via the Hurwitz integral representation : $$\zeta (s)=\frac{1}{\Gamma (s)}{\int }_0^{\infty }\frac{x^{s-1}}{e^x-1}dx,\mathrm{Re}(s)>1.$$ The integrand is integrable for $\mathrm{Re}(s)>1$ near $0$ and is exponentially small at $\infty$. To analytically continue, one deforms the contour: $$\zeta (s)=\frac{\Gamma (1-s)}{2\pi i}{\oint }_C\frac{(-x{)}^{s-1}}{e^x-1}dx,$$ where $C$ is the Hankel contour: from $+\infty$ along ${\mathbb{R}}^{+}$, around $0$ counterclockwise, back to $+\infty$.

C.2 What HoTT needs

To carry out the contour-integral proof in HoTT we need:

1. HoTT-native $\Gamma$ function: $\Gamma (s):={\int }_0^{\infty }{t}^{s-1}{e}^{-t}dt$ extended via the functional equation $\Gamma (s+1)=s\Gamma (s)$ to all ${\mathbb{C}}_{\mathsf{c}}\setminus \{0,-1,-2,\dots \}$.

2. HoTT-native contour integration: a path $\gamma :[0,1]\to {\mathbb{C}}_{\mathsf{c}}$ and an integral ${\int }_{\gamma }f(z)dz$, satisfying linearity, change-of-variables, and Cauchy’s theorem.

3. HoTT-native version of Cauchy’s theorem: holomorphic functions integrate to zero around closed contours.

4. HoTT-native deformation lemma: integral over homotopic contours agree.

5. HoTT-native passage from real integral to contour integral (Mellin-Barnes type).

C.3 Estimated effort

Each item above is a self-contained HoTT formalisation problem of moderate size. Cumulatively, this is the heart of 44, and we estimate it at $\sim 3000$ lines of Cubical Agda.

C.4 Alternative strategies

• Riemann’s theta-function method: $\zeta (s)$ via Mellin transform of $\theta (t):={\sum }_{n\in \mathbb{Z}}{e}^{-\pi n^{2}t}$. Requires the modular transformation $\theta (t)=t^{-1/2}\theta (1/t)$.

• Hardy’s symmetric form: $\xi (s):=\frac{s(s-1)}{2}{\pi }^{-s/2}\Gamma (s/2)\zeta (s)$, satisfying $\xi (s)=\xi (1-s)$. Cleaner but uses the same infrastructure.

• Cohesive synthetic approach: Inside differential cohesive HoTT , define $\zeta$ via the synthetic functional integral. Speculative.

14 Appendix: A glossary of HoTT-native synonyms

For readers more familiar with classical analytic NT than with HoTT, we provide a short translation glossary:

The bottom row is the principal open problem of this paper.