AI FOR MATH FUND 2026 · FULL PROPOSAL

Phaenarete Project

Toward the Resolution of Hilbert's Eighth Problem (Riemann Hypothesis) through Human‑AI Collaboration

Wir müssen wissen. Wir werden wissen.

— David Hilbert, 1930 retirement address

If you could sell your soul for the proof of one theorem, most mathematicians would ask for the Riemann Hypothesis.

— H. Montgomery

The convergence of three windows

Theoretical window

Guth–Maynard 2024: first improvement of zero‑density exponent in 80 years (from 12/5 to 30/13). Zhang 2022: Landau‑Siegel polynomial breakthrough. Rodgers–Tao 2020: de Bruijn‑Newman constant Λ ≥ 0, RH ↔ Λ=0. Random matrix universality, spectral embedding (2026).

AI window

AlphaProof (IMO silver 2024), Gemini Deep Think (IMO gold 2025), Gauss AI (formalized 24‑sphere packing, 200k lines Lean, 30 errors found). AI is now a "trusted junior collaborator" (Tao).

Team window

One living solver of a Hilbert problem (Matiyasevich), two academicians (Liu & Sun), legendary number theorist Yitang Zhang, young prodigy Travor Liu, and cross‑disciplinary architect Ang Li.

Core execution team

Project Leader · Founder

Ang Li

Associate Researcher, Institut de Pratiques Philosophiques · Philosophy, AI & paradigm design

Project Founder, co‑creator of Turn‑Lang and the Maieutica Framework (Socratic midwifery model). Cross‑disciplinary: philosophy, AI, foundations of mathematics.

https://liang.world/

Lead Mathematician

Travor Liu (Zihao Liu)

Stanford Ph.D. Candidate, UCL First‑Class Honours

Independent arXiv author ("Explicit quadratic large sieve inequality"). Mathematics communicator with 82k+ followers on Zhihu. Bridges analytic number theory and AI‑readable logic.

https://travorlzh.github.io/

World‑class advisors

Academician Jianya Liu

Strategic Advisor · CAS Academician

Vice President of Shandong University, PI of National Key R&D Program on RH. Expert in automorphic forms and prime distribution.

direction & resources

Professor Yuri Matiyasevich

Special Advisor · RAS Academician

Solver of Hilbert's Tenth Problem (1970) – the only living solver of a Hilbert problem. Recent work (2025) with Zhiwei Sun on undecidability over algebraic integers.

historical insight

Academician Binyong Sun

Mathematics Advisor · CAS Academician

Expert in L‑functions and representation theory. Provides deep analytical toolkit for RH.

L‑functions & automorphy

Professor Yitang Zhang

Honorary Advisor

Pioneer on Twin Prime Conjecture (2013), Solver of Landau–Siegel Zeros Problem (2022). Legendary number theorist.

strategic compass

⚡ For the first time in history ⚡
a solver of one Hilbert problem (Matiyasevich) + two CAS academicians (Liu & Sun) + legendary number theorist Yitang Zhang + young prodigy Travor Liu + cross‑disciplinary architect Ang Li jointly focus on another Hilbert problem: the Riemann Hypothesis.

The Maieutica Framework & PrimeClaw

Rejecting the "problem‑solving machine" view, we cast AI as a Socratic midwife: human provides intuition, AI performs massive‑scale analogy, lemma search, and verification.

PrimeClaw – multi‑agent system

Knowledge agent – semantic graph of literature (Guth‑Maynard, Zhang, …)
Explorer agent – MCTS + policy network, conjectures new paths
Prover agent – translates paths into Lean 4 proof scripts
Verifier agent – Lean kernel, zero‑defect logic, intercepts hallucinations

Turn‑Lang meta‑language

Foundation‑independent type theory: treat ZFC/HoTT/CIC as algebraic structures. Functorial interpretation system for cross‑foundational proof migration. Confidence‑bounded types to capture AI uncertainty. Laws as first‑class constraints. Solves the "Tower of Babel" of formal proofs. Co‑created by Ang Li, the project founder.

Three‑pillar proof blueprint

Pillar I – Arithmetical spectral constraint
Connes' truncated quadratic form: extremal points converge to zeros with real part 1/2.

Pillar II – Density‑bound coupling
Assume a zero off the line → use Guth‑Maynard upper bound + Zhang‑type lower bound → contradiction for large |γ|.

Pillar III – Statistical universality
GUE statistics imply all zeros on critical line (via averages of log derivative).

History of the Riemann Hypothesis — pivotal moments

Year

Event

People

1859RH formulated in "On the Number of Primes Less Than a Given Magnitude"Riemann

1896Prime Number Theorem proved; zeros lie in 0<Re(s)<1Hadamard, de la Vallée Poussin

1914Infinitely many zeros on critical line; Bohr–Landau theoremHardy; Bohr, Landau

1942Positive proportion of zeros on critical lineSelberg

1948RH for curves over finite fields (Weil conjectures for curves)Weil

1972Montgomery pair correlation / Dyson random matrix connectionMontgomery, Dyson

1974Weil conjectures proved (analogue of RH)Deligne

1989At least 2/5 zeros on critical line (Conrey)Conrey

1999Noncommutative geometry approachConnes

2000Millennium Problem, $1M prizeClay Math Institute

2004Verification of first 10¹³ zerosGourdon, Demichel

2020de Bruijn–Newman constant Λ ≥ 0 (RH ↔ Λ=0)Rodgers, Tao

2022Landau–Siegel zeros breakthroughZhang

2024First zero‑density exponent improvement in 80 yearsGuth, Maynard

2026Spectral embedding conjecture (bypasses density)De Giuseppe et al.

Selected breakthroughs — full timeline in project records.

18‑month baseline deliverables

≥500 lemmas

Lean4 formalized theorem library (RH‑related), reusable for the community

PrimeClaw v1.0

Open‑source (MIT) multi‑agent framework, transferable to other problems

Methodology whitepaper

Formal publication (arXiv+journal) on the "midwifery" paradigm

Talent development

At least 1 mathematician with 3 years dedicated time

Failure records

All dead ends publicly documented – transparent, auditable, learnable

"We are not betting on 'success'; we are betting on the process. Even if RH is not proved within 18 months, the tools, methods, and community built will become permanent assets for human intellect."

All team links point to verifiable institutional pages · open science commitment · MIT license for all code