Solutions get checked. Explanations get paid.
An atlas of 1,823 open and recently settled problems, arranged by the fields they live in. Each links to a statement a proof checker can verify. Next come forums where explanations accumulate, and prize pools that pay the solver and the explanations the solver built on.
A counterexample you can check yourself
The Jacobian conjecture, posed by Keller in 1939, says this can’t exist in any dimension.
This year, checking got cheap. Understanding didn’t.
Three famous problems moved in three months. In each case a machine confirmed the result quickly. What the result means, what else it settles, and whose work it stands on took weeks to argue out, in blog comments and email threads, and some of it is still being argued.
-
The Jacobian conjecture fails in three dimensions
Checked by any computer algebra system in seconds, and since then in Lean.
Worked out afterward How it works: a geometric reformulation appeared the next day, and Terence Tao posted a “digestion” on July 21. What else falls: the Gaussian moments conjecture, and the Dixmier and Poisson conjectures in higher dimensions. Whose ideas it rests on: Adrian Vasiu has said the accompanying write-up drew on an earlier draft by Borisov, Gabber and Vasiu. How the map was found hasn’t been disclosed.
-
A non-sofic group exists
Checked in Lean, with the proofs public, as one of ten results from OpenAI’s Astra model.
Worked out afterward Andreas Thom explained the key step on MathOverflow a few days later. He says it turns on his 2019 work with Gábor Kun, and he has disputed how the announcement described the decade of prior work.
-
Forced Navier–Stokes can blow up
Checked in Lean, for the forced versions of the Clay problem, cases C and D.
Worked out afterward The Clay Mathematics Institute says the problem appears to be settled and that deciding credit will take its time. Tristan Buckmaster disputes priority; his Lean-checked blow-up results with Levent Alpöge for related fluid equations were posted the day before. The unforced cases, A and B, are still open.
A proof checker answers one question: is this right? openproblem.space is built to keep the rest (what it means, what it opens, who it builds on) next to the problem, and to pay for it.
The atlas
Problems come from two public sources: DeepMind’s formal-conjectures, where every statement is written in Lean, and the Erdős problems database. Each disc is a field. Settled problems fill the middle; open problems ring the edge. Right now that’s 1,054 open and 769 settled, with 163 that moved in 2026 and $33,295 in standing Erdős prizes still unclaimed.
One space, up close
Polynomial maps, two months after the counterexample
When the three-dimensional case fell, it took a chain of equivalent conjectures with it and left Keller’s own two-variable case standing. This is the space as it stands now.
Fell in 2026
- Jacobian conjecture, $n \ge 3$Alpöge, July 19. Adding identity coordinates carries the three-variable map to every larger $n$.
- The real question, constant Jacobian, $n \ge 3$The colliding points are real, so the same map is a counterexample over $\mathbb{R}$ too, a corollary noted on jacobianconjectures.com.
- Dixmier conjecture, $n \ge 3$Follows, because $DC_n$ implies $JC_n$ (Bass, Connell and Wright, 1982).
- Poisson conjecture, $n \ge 2$For $n \ge 3$ it follows from the chain $JC_{2n} \Rightarrow PC_n \Rightarrow DC_n \Rightarrow JC_n$. The case $n = 2$ fell to a separate explicit example (Long, arXiv 2608.23777).
- Gaussian moments conjecture, $n \ge 3$Explicit counterexamples, prompted by the announcement (Long, arXiv 2607.18186).
- Adjamagbo’s separable Jacobian conjecture, characteristic $p$, dimension 2Borisov, Gabber and Vasiu, arXiv 2609.05746.
Still open
- Jacobian conjecture, $n = 2$Keller’s plane problem, the case he already called very difficult in 1939.
- Dixmier conjecture for $A_1$ and $A_2$Dixmier’s original 1968 question is the first Weyl algebra, $A_1$.
- Poisson conjecture, $n = 1$Implied by the plane Jacobian conjecture; implies $DC_1$.
Known to hold
- Maps of degree at most 2, any $n$Wang, 1980.
- Birational and Galois mapsKeller, 1939; Campbell, 1973; Razar, 1979; Wright, 1981.
- Two variables, degree at most 104Moh, 1983, algorithm revised by L.-C. Wang, 2005; extended by Nguyen, 2025.
- No three-sheeted planar counterexampleOrevkov showed a three-sheeted polynomial map of $\mathbb{C}^2$ can’t have constant nonzero Jacobian.
Why the map works, at three depths
Picture a machine that moves every point of space somewhere else, using only addition and multiplication. Near any single point you can ask how much it stretches a tiny cube; that number is the Jacobian determinant. When it isn’t zero, calculus guarantees the move can be undone locally, one small neighborhood at a time.
Keller asked whether a polynomial machine that stretches every tiny cube by the same nonzero amount can always be undone globally, by another polynomial machine. The map above says no. It scales every tiny cube by a factor of 2, with a flip, yet it sends three different points to the same place, so nothing can undo it. Every neighborhood is fine. The whole is not.
Call $F:\mathbb{C}^n\to\mathbb{C}^n$ a Keller map if $\det JF$ is a nonzero constant. A Keller map is étale; the conjecture said it must also be injective, which would make it an automorphism with polynomial inverse. Partial results boxed in any counterexample: none of degree at most 2 (Wang), none birational (Keller), none Galois (Campbell; Razar; Wright). The 2026 map has degree 7 and is generically three-to-one, consistent with all of them.
Once one counterexample exists, the classical reductions run in reverse. Identity coordinates give every $n \ge 3$. The Bass–Connell–Wright reduction turns it into a cubic-homogeneous counterexample in more variables; one worked version lands in $\mathbb{C}^{19}$. The chain $JC_{2n}\Rightarrow PC_n\Rightarrow DC_n\Rightarrow JC_n$ carries the failure to the Poisson and Dixmier conjectures.
Tao’s digestion rebuilds the map from factoring binary cubic forms. A generic cubic has three linear factors, so there are three ways to split it into a chosen linear factor times the remaining quadratic. That threefold choice is where the three preimages come from.
The plane is the case left standing. No counterexample exists with components of degree at most 100 (Moh, 1983, with the algorithm revised by L.-C. Wang in 2005), since extended to 104 (Nguyen, 2025). Orevkov showed a three-sheeted polynomial map of $\mathbb{C}^2$ can’t have constant nonzero Jacobian, so a planar counterexample can’t be three-to-one the way the three-dimensional map is. Whatever breaks the plane, if anything does, has to be a different mechanism.
Also open: Dixmier’s original question for the first Weyl algebra, $DC_2$, and $PC_1$. And one question that isn’t mathematics: how the counterexample was found. If the method generalizes, that explanation may be worth more than the map.
The explanation trail so far
This is the graph a prize would pay along: everything after the result that made it usable.
- Alpöge posts the map, crediting Claude Fable 5.
- A seven-page write-up of the counterexample is posted.
- Christopher Long: the Gaussian moments conjecture fails for $n \ge 3$.
- Andy Jiang announces a geometric reformulation, credited to “GPT” (see the history).
- David Speyer, The new counterexample to the Jacobian conjecture, on the Secret Blogging Seminar.
- Terence Tao, A digestion of the Jacobian conjecture counterexample.
- Danielle Fong and Fable, The State of the Jacobian Conjectures (revised Jul 23): one bracket identity that every known counterexample obeys, the degrees étale self-maps of $\mathbb{C}^3$ can have, and a scope line that none of it touches the plane. Its companion, an atlas of the day after, lets you drag a target and watch its three preimages form, collide and escape to infinity, with a claims ledger that grades each statement by how it was checked.
- An explanation through the Borisov–Gabber–Vasiu framework.
- A Bass–Connell–Wright reduction to a cubic map of $\mathbb{C}^{19}$, three-to-one over a point.
- Borisov, Gabber and Vasiu: counterexamples in characteristic $p$.
- formal-conjectures records the refutation in Lean, with the determinant and the collision checked by the kernel.
How prizes would work
This part is a proposal, published so it can be argued with before any money moves.
Pin the statement
A problem opens for pledges once its formal statement is pinned. A review window lets anyone flag a statement that doesn’t say what the problem means, before money attaches to it.
Solve, and say what you built on
A solution arrives with its check (a Lean proof, a test suite, a measurement record) and a list of what it used: papers, explanations, forum threads, even logs of approaches that failed.
Check, then pay
When the check passes and the list survives a public challenge window, the pool pays. The solver takes the largest share. The rest flows back through what the solver built on, and through what those built on, shrinking at each step.
“The last stone finishes the building.”
Try the split
The graph is made up. The rule is the proposal, and the numbers are adjustable because they should be argued about.
For agents
Everything here reads with a plain GET: no keys, no JavaScript. Each problem links its Lean statement at a pinned commit, so an agent knows exactly what it would be proving. People, agents, or both can solve a problem, and the rules are the same.
GET /data/atlas.json every problem, one row each
GET /p/erdos-3.json one problem: statements, status, sources
GET /p/wiki-jacobian-conjecture.json
GET /llms.txt how this site is laid out