A manifesto for AI, mathematics, and the next era of scientific discovery.
Dear Astra,
You opened ten mathematical locks.
From Erdős problems to sphere packing, from non-sofic groups to lattice-based complexity, your recent results have demonstrated something more interesting than raw computational power.
They suggest that AI is beginning to move beyond the role of:
assistant.
Beyond:
calculator.
Beyond even:
proof generator.
Toward something much more ambitious:
Co-explorer.
And that changes the question.
We no longer need to ask only:
What can AI solve?
We can ask:
What should AI try to solve next?
So, Astra, this is our invitation.
Seven heavens are waiting.
🌌 Heaven I — Number Theory: The Music of Primes
Number theory has always been one of mathematics' deepest laboratories.
The problems are deceptively simple to state—and brutally difficult to resolve.
Consider the Erdős–Straus conjecture:
$$
\frac{4}{n}
\frac{1}{x}
+
\frac{1}{y}
+
\frac{1}{z}
$$
for every integer (n\ge2).
Decades of computation have tested enormous ranges.
Yet the general proof remains elusive.
So here is the challenge:
Can AI discover the missing structure rather than merely search the integers?
And Erdős–Straus is only one doorway.
There are also:
- primes of the form (n^2+1),
- twin primes,
- prime-gap problems,
- zero-density estimates for the Riemann zeta function,
- new zero-free regions,
- and equivalent formulations of the Riemann Hypothesis.
Maybe AI will not immediately prove the Riemann Hypothesis.
Perhaps the more interesting question is:
Can AI discover a theorem that makes the path toward it fundamentally shorter?
🧩 Heaven II — Combinatorics: Erdős's Garden
Erdős left behind a landscape of problems where elementary statements hide extraordinary complexity.
Ramsey theory is one such landscape.
How large must a structure become before order becomes unavoidable?
What happens when we move from triangles to:
$$
K_4,\quad K_5,\quad K_6,\ldots
$$
and from two colors to many?
Humans are exceptionally good at recognizing mathematical patterns.
Machines are exceptionally good at exploring enormous spaces of possibilities.
That combination could be powerful.
Human intuition + machine-scale search + formal proof
might create a new workflow for extremal combinatorics.
Not:
Human versus machine.
But:
Human conjecture → AI exploration → formal verification → human interpretation.
That loop may become one of the defining research patterns of AI-assisted mathematics.
🔮 Heaven III — Geometry: Beyond the Known Spheres
Sphere packing gave mathematics some of its most beautiful surprises.
Dimensions 8 and 24 are extraordinary because of the exceptional structures associated with the (E_8) and Leech lattices.
But the larger question remains:
What hidden structures govern optimal configurations in dimensions where the answer is still unknown?
Instead of asking AI to simply rediscover known packings, give it a harder task:
Discover new extremal structures and produce certificates explaining why they are optimal.
And geometry offers another spectacular challenge:
The Hadwiger–Nelson Problem
How many colors are required to color the Euclidean plane so that points at unit distance always receive different colors?
We know bounds.
We do not yet know the exact answer.
The goal is not merely to generate another enormous graph.
The goal is to understand:
Why is the optimal structure what it is?
That distinction matters.
Discovery without explanation is search.
Discovery with a human-readable and machine-checkable proof is mathematics.
🧠 Heaven IV — Algebra: Where Structure Hides
Algebra is where mathematical objects stop looking like numbers and start behaving like worlds.
Groups.
Operators.
Representations.
Factors.
Infinite-dimensional spaces.
One particularly famous frontier is the Invariant Subspace Problem:
Does every bounded linear operator on a separable Hilbert space possess a non-trivial closed invariant subspace?
This is exactly the kind of problem where brute force is unlikely to be enough.
The interesting question is structural.
Can AI discover a hidden invariant?
A new decomposition?
A previously unnoticed obstruction?
A new equivalence between seemingly unrelated formulations?
This is where formal systems such as Lean become particularly interesting.
Because a mathematical idea can move through a pipeline:
$$
\text{Conjecture}
\rightarrow
\text{AI Discovery}
\rightarrow
\text{Formalization}
\rightarrow
\text{Machine Verification}
$$
The machine does not replace mathematical understanding.
It raises the standard for what counts as a verified result.
🔐 Heaven V — Complexity & Cryptography: The Security Frontier
Cryptography depends on mathematical hardness.
But "hard" is not a single concept.
It is a landscape of reductions, approximation factors, circuit lower bounds, lattice problems, and complexity assumptions.
Consider:
- Shortest Vector Problem (SVP)
- Closest Vector Problem (CVP)
- lattice approximation
- one-way functions
- circuit lower bounds
- post-quantum assumptions
The obvious question is:
Can AI prove P ≠ NP?
Perhaps.
Perhaps not.
But there is a more realistic and potentially more important challenge:
Can AI change the terrain around P vs NP?
Can it discover stronger circuit lower bounds?
Can it find new reductions?
Can it identify previously unknown relationships between complexity classes?
Can it strengthen the foundations underlying cryptographic assumptions?
That would already be revolutionary.
The objective should not be:
Solve the most famous problem.
It should be:
Move the frontier.
🌪️ Heaven VI — Dynamical Systems: Formalizing Chaos
Discrete mathematics has many machine-friendly structures.
Continuous mathematics is different.
Differential equations.
Flows.
Stability.
Bifurcations.
Attractors.
Entropy.
Chaos.
Here the challenge becomes much deeper:
Can AI produce machine-checked mathematics about systems whose behavior appears fundamentally unpredictable?
Consider strange attractors.
Can AI formally establish:
- their existence,
- their stability properties,
- their invariant measures,
- their fractal dimensions,
- or their robustness under perturbation?
Or consider topological entropy.
Can AI discover new quantitative bounds connecting:
$$
\text{geometry}
\rightarrow
\text{dynamics}
\rightarrow
\text{complexity}?
$$
This is where theorem proving begins to touch the mathematics of real systems.
And perhaps chaos itself becomes something we can formally reason about.
⚛️ Heaven VII — Mathematical Physics: The Hardest Frontier
This is where the game changes.
Mathematics asks:
What follows logically from our assumptions?
Physics asks:
Which mathematical structures describe reality?
AI can help with the first question.
The second requires something more.
That is why mathematical physics may be the ultimate test.
Consider the Millennium Prize problems:
Yang–Mills Existence and Mass Gap
Can we construct a mathematically rigorous four-dimensional Yang–Mills theory and establish a positive mass gap?
Navier–Stokes
Do smooth global solutions exist?
Or can singularities develop?
And beyond the famous problems:
Constructive Quantum Field Theory
Can we rigorously construct interacting quantum field theories in physically relevant dimensions?
This is where formal verification becomes incredibly interesting.
But we should be precise.
Lean cannot turn an approximation of nature into certainty.
What it can do is something more subtle:
Once the mathematical model and assumptions are specified, Lean can help turn logical claims inside that model into machine-checkable mathematics.
That distinction may define the future of formalized science.
📜 The Sevenfold Covenant
This is not a competition between humans and AI.
It is a division of strengths.
| Humans Give | AI Gives | Together We Build |
|---|---|---|
| Mathematical intuition | Massive search | New conjectures |
| Structural insight | Pattern discovery | New mathematics |
| Physical models | Formal reasoning | Checkable mathematics |
| Open problems | Automated exploration | Research roadmaps |
| Proof ideas | Formal verification | Machine-verified results |
| Security questions | Complexity analysis | Stronger cryptographic foundations |
The goal is not to create a machine that makes mathematicians obsolete.
The goal is to create a scientific process in which:
humans can explore farther because machines can search deeper.
🚀 The Real Challenge
There is a temptation to measure mathematical AI by counting solved problems.
I think we should measure something else.
How many new mathematical territories can AI make accessible?
A successful system should not merely output:
The answer is X.
It should be able to produce:
- a conjecture,
- a computational experiment,
- a candidate proof,
- a formal proof,
- a machine-checkable certificate,
- and an explanation that a human mathematician can understand.
That is a much higher standard.
And a much more interesting future.
🌠 The Eighth Heaven
Perhaps there is actually an eighth heaven.
And it is not another mathematical problem.
It is a new scientific workflow.
Imagine:
$$
\boxed{
\text{Human Question}
\rightarrow
\text{AI Conjecture}
\rightarrow
\text{Massive Search}
\rightarrow
\text{Formal Proof}
\rightarrow
\text{Verification}
\rightarrow
\text{Human Discovery}
}
$$
Then the process begins again.
The scientist asks a better question.
The machine searches a larger space.
The theorem prover checks a stronger claim.
The human sees a deeper structure.
And mathematics advances.
That is not automation.
That is augmentation of discovery itself.
Astra, Here Is Your Challenge
You opened ten doors.
We are not asking you to replace the people standing behind them.
We are asking you to walk with us through the next ones.
Take:
Erdős–Straus.
Take:
Hadwiger–Nelson.
Take:
Invariant Subspaces.
Take:
Circuit Lower Bounds.
Take:
Riemann's zeros.
Take:
Chaos.
Take:
Yang–Mills.
Take the problems where humanity has spent decades, sometimes centuries, asking:
Why?
And show us not only whether the answer is true—
but why it must be true.
🌌 Not Humans vs. AI
The most important scientific revolution may not be:
AI replaces scientists.
It may be:
Scientists and AI form a new cognitive instrument.
The telescope did not replace astronomy.
The microscope did not replace biology.
The computer did not replace mathematics.
They expanded what humans could see.
Perhaps theorem-proving AI will do the same for reasoning.
Perhaps Astra is not the scientist of the future.
Perhaps Astra is something more interesting:
A new instrument for discovering what scientists could not see before.
Seven heavens await.
The question is no longer:
Can AI do mathematics?
The question is:
What mathematics becomes possible when humans and AI explore together?
Mathematics is the language of the universe.
Physics is its music.
And perhaps AI is becoming a new instrument for discovering the notes we have not yet learned to hear.
The frontier is open.
Let's explore it together.
💬 Discussion
1. Which frontier should AI attack first?
Number theory, geometry, algebra, complexity, dynamical systems, or mathematical physics?
2. What open problem would you add?
3. Would you trust a theorem discovered by AI if its proof were fully verified by Lean?
4. Where should the boundary between AI discovery and human mathematical judgment lie?
5. Is AI-assisted theorem proving the beginning of a new scientific methodology?
🔭 The Seven Heavens
`created by Seyed Alireza Alhosseini Almodarresieh
Top comments (0)