Terrence Tao's ChatGPT Conversation about the Jacobian Conjecture Counterexample
410 points - today at 5:30 PM
SourceComments
Sorry it's a bit of an aside, but I imagine many other otherwise "technical" folks feel the same unfamiliar sense of total loss like when encountering hard mathematics.
The first one was someone proving another conjecture false by just repeatedly saying "keep going" to ChatGPT: https://x.com/DmitryRybin1/status/2079904005652893709
What a world we live in.
1. The counter example wasn't just a brute force selection, the polynomial is structured in a very specific way that ends up getting the result.
2. Terry Tao's questions are very specific and prompts the AI in a useful way, that without high math training you are not going to get the same information out of it. Terry seems to see some aspects of the problem and counter example and uses AI to brute force some parts of it.
Just awesome to see new knowledge hit an incredible mind like this. Having these "what if" discussions is what I miss most from JPL and academia.
a) The model thinks on some questions while straight answers on others. (I wish I'd knew from the questions if this is somehow correlated to hard tasks or "inventive" tasks, but that's way out of my league).
b) The model sometimes pushes back. Again, I'd wish I knew if it was warranted, but I counted 2 instances where it said "yes, but with caveats", one where it said "mostly yes but with this correction" and one where it said "careful here, because x y z".
c) The model did q&a + pdf ingestion + code writing + more q&a + thinking + more q&a, for a looong while, while seemingly staying on topic (at least Terrence Tao seems to think they're still productive, so I'll trust that).
This is what model progress is, not number goes up on xBency or yBencher. Damn.
Another satisfied customer!
Where will we be in another 4 years? What a time to be alive!
The fascinating this is that the LLM is not acting as a tool here AFAIk, but very much like a colleague.
I have no knowledge of the domain and have only PhD EE level math knowledge, so maybe my bar is too low.
```
A question is salient to the degree that its answer changes what we do next. Operationally, saliency = the product of four things:
- Decision-leverage — would resolving it one way vs another force a different design or invalidate a stated decision? (No leverage → drop, however interesting.)
- Residual uncertainty given current evidence — is it still genuinely open after reading the docs and the code? (Already settled → drop, however deep.)
- Load-bearing-ness — how much rests on the premise.
- Cost of finding out late — architecture-deciding / expensive-to-unwind raises priority; cheap-to-fix-later lowers it.
```
There are a few things to note about this prompt
1. There is no reason from looking at it that it should work, it even has the word load-bearing which people loathe, but it remarkably produces a stable design with questions from claude (atleast from claude Opus 4.8 and even better from Fable5). Otherwise the design document claude likes to really write are implementation level(code or otherwise). I usually pair this with matt pocock's grilling skill to make claude behave.
2. From design -> implementation, its is generally about understanding when claude is trying to trick you into making something sound like a good/easy solution but has tons of untested assumptions. Here you have to read and patiently spot if a how you would get to the solution is not clear. A common error here are when claude makes a big deal based on what it read and interpreted too seriously without questioning the assumptions. There are several more.
But it also comes down to your experience as a SWE, much like a mathematician's. The frustrating thing about it is, it feels tha a skilled mathematician working with AI can make them productive in ways that are more reliable as compared to a SWE (e.g. lean is deterministic and can provide very strong feedback and LLMs are very good at using that feedback). Maybe a mathematician can chime in on that?
One thing I notice is many models say statements along the lines of “okay we have exhausted this thread it’s diminishing returns from here and we should stop and move on”
It’s funny because I’ve been building a tiny neural network maze solver (23 bytes solves 92.75% of unseen 2D mazes)
When I asked ChatGPT/Fable if we had anymore threads to pull to increase capability and decrease byte size, they both basically said no way - back when I was at ~166 byte models with a ~85% solve rate.
Throughout the experiment I just kept trying different approaches and eventually had 3 mini “breakthroughs” in this particular niche. But if I had listened to the models…
Anyway, these models are amazing to experiment with quickly, but they are dumb as hell and so absolute
Two, at some point AIs will be able to use other context like the fact that this is Terrence Tao and not your average Joe and change how it answers, either in tone or structure.
Is there any way to tell a conversation's model and thinking level?
Modern AI feels like a godsend to mathematicians. It helps them break down boundaries and connect concepts in ways a mere mortal couldn't imagine.
I don't think chatgpt could have come to this on its own without the amount of steering he did, which just validates the idea that AI is not a replacement for human expertise but an amplifier.
Is this a breakthrough of something or 'kinda interesting'?
Expand the entire expression, then change the representation to find the core axis. You can't see the axis from just one perspective, so you change the representation. In programming terms, it's like applying multiple domain models. Then break it down into small contract units. Why is it a Jacobian monomial? Why does x satisfy a cubic equation? And so on.
Then swap out the modeling under a hypothesis, assemble it all back together, and verify it through the equation.
This feels similar to modeling in programming.
Observe the whole -> explore better modeling -> decompose local problem -> verify independently -> reason about the highre level structure -> integrate back into the original problem.
This feels similar to when I receive work from a client and write a programming proposal
Is it something "revolutionary" or just another small brick that will pile up until something really "revolutionary" will happen?
Yes—for a continuous-time autonomous system
x ˙ =f(x),f(x ∗ )=0,
this is the standard linearization criterion, with J=Df(x ∗ ):
If every eigenvalue of J has strictly negative real part, then x ∗ is locally exponentially asymptotically stable. If at least one eigenvalue has strictly positive real part, then x ∗ is unstable. If no eigenvalue has positive real part but at least one has real part 0, linearization is generally inconclusive. Nonlinear terms or a center-manifold analysis are needed.
The last case really can go either way. For example, all three scalar equations below have Jacobian J=0 at x=0:
x ˙ =−x 3 , x ˙ =x 3 , x ˙ =0.
Yet 0 is respectively asymptotically stable, unstable, and neutrally stable.
A slightly more precise wording is therefore:
If the spectral abscissa
α(J)= λ∈σ(J) max
Reλ
is negative, the equilibrium is locally exponentially stable. If α(J)>0, it is unstable. If α(J)=0, the Jacobian test is inconclusive.
This criterion concerns the Jacobian matrix of a dynamical system at an equilibrium; it is unrelated to the “constant Jacobian determinant” condition in the Jacobian conjecture.
noncomputable section
open Matrix Function
/-! # A counterexample to the Jacobian conjecture in dimension three
We formalize the polynomial map
F : ℂ³ → ℂ³
whose Jacobian determinant is the constant `-2`, but which is not injective.The final theorem `jacobianConjecture3_false` states the failure of the polynomial-inverse formulation of the Jacobian conjecture in dimension three. -/
namespace MvPolynomial
variable {R : Type} {σ : Type}
/-- The formal Jacobian matrix of a family of multivariate polynomials. -/ def jacobianMatrix [CommSemiring R] [DecidableEq σ] (F : σ → MvPolynomial σ R) : Matrix σ σ (MvPolynomial σ R) := Matrix.of fun i j ↦ pderiv j (F i)
/-- The formal Jacobian determinant. -/ def jacobianDet [CommRing R] [Fintype σ] [DecidableEq σ] (F : σ → MvPolynomial σ R) : MvPolynomial σ R := (jacobianMatrix F).det
/-- Evaluation of a polynomial map at a point. -/ def evalMap [CommSemiring R] (F : σ → MvPolynomial σ R) (p : σ → R) : σ → R := fun i ↦ eval p (F i)
end MvPolynomial
open MvPolynomial
namespace JacobianCounterexample
variable (K : Type) [Field K]
/-- The three components of the polynomial counterexample.
The variables `X 0`, `X 1`, `X 2` correspond respectively to `x`, `y`, `z`. -/ def F : Fin 3 → MvPolynomial (Fin 3) K := ![ (1 + X 0 X 1) ^ 3 * X 2 + X 1 ^ 2 * (1 + X 0 * X 1) * (C 4 + C 3 * (X 0 * X 1)),
X 1
+ C 3 * X 0 * (1 + X 0 * X 1) ^ 2 * X 2
+ C 3 * X 0 * X 1 ^ 2
* (C 4 + C 3 * (X 0 * X 1)),
C 2 * X 0
- C 3 * X 0 ^ 2 * X 1
- X 0 ^ 3 * X 2
]
/--
The formal Jacobian determinant of `F` is the constant polynomial `-2`.
-/
theorem jacobianDet_F :
jacobianDet (F K) = C (-2) := by
simp only [
jacobianDet,
jacobianMatrix,
det_fin_three,
of_apply,
F,
cons_val_zero,
cons_val_one,
cons_val_two,
head_cons,
tail_cons,
map_add,
map_sub,
Derivation.map_one_eq_zero,
pderiv_mul,
pderiv_pow,
pderiv_C,
pderiv_X_self,
pderiv_X_of_ne,
ne_eq,
Fin.reduceEq,
not_false_eq_true
]
simp only [map_neg, map_ofNat]
ringvariable {K}
/-- The point `(0, 0, -1/4)` maps to `(-1/4, 0, 0)`. -/ theorem evalMap_F_p0 : evalMap (F K) ![0, 0, -(1 / 4)] = ![-(1 / 4), 0, 0] := by funext i fin_cases i <;> simp [evalMap, F]
/-- Provided `2 ≠ 0`, the point `(1, -3/2, 13/2)` also maps to `(-1/4, 0, 0)`. -/ theorem evalMap_F_p1 (h2 : (2 : K) ≠ 0) : evalMap (F K) ![1, -(3 / 2), 13 / 2] = ![-(1 / 4), 0, 0] := by have h4 : (4 : K) ≠ 0 := (by norm_num : (2 : K) * 2 = 4) ▸ mul_ne_zero h2 h2 funext i fin_cases i <;> simp [evalMap, F] <;> field_simp [h4] <;> ring
end JacobianCounterexample
open JacobianCounterexample
/-- The Jacobian determinant of the displayed map over `ℂ` is a unit. Indeed, it is the nonzero constant `-2`. -/ theorem F_jacobian_isUnit : IsUnit (jacobianDet (F ℂ)) := by rw [jacobianDet_F] exact (isUnit_iff_ne_zero.mpr (by norm_num : (-2 : ℂ) ≠ 0)).map C
/-- The polynomial map `F : ℂ³ → ℂ³` is not injective. -/ theorem F_not_injective : ¬ Injective (evalMap (F ℂ)) := by intro hInjective
have hp :
(![0, 0, -(1 / 4)] : Fin 3 → ℂ) =
![1, -(3 / 2), 13 / 2] :=
hInjective
((evalMap_F_p0 (K := ℂ)).trans
(evalMap_F_p1 (K := ℂ) (by norm_num)).symm)
exact zero_ne_one (congrFun hp 0)
/--
The injectivity consequence of the dimension-three Jacobian conjecture
is false over `ℂ`.
-/
theorem unitJacobian_does_not_imply_injective :
¬ ∀ P : Fin 3 → MvPolynomial (Fin 3) ℂ,
IsUnit (jacobianDet P) →
Injective (evalMap P) := by
intro h
exact F_not_injective (h (F ℂ) F_jacobian_isUnit)/-! We now formulate the polynomial-inverse version explicitly. -/
/-- Polynomial self-maps of affine three-space over `ℂ`. -/ abbrev PolyMap3 := Fin 3 → MvPolynomial (Fin 3) ℂ
/-- A polynomial map has a polynomial two-sided inverse, viewed as functions on `ℂ³`. -/ def HasPolynomialInverse (P : PolyMap3) : Prop := ∃ Q : PolyMap3, LeftInverse (evalMap Q) (evalMap P) ∧ RightInverse (evalMap Q) (evalMap P)
/-- The polynomial-inverse formulation of the Jacobian conjecture in dimension three. -/ def JacobianConjecture3 : Prop := ∀ P : PolyMap3, IsUnit (jacobianDet P) → HasPolynomialInverse P
/-- The Jacobian conjecture in dimension three is false. -/ theorem jacobianConjecture3_false : ¬ JacobianConjecture3 := by intro hJC unfold JacobianConjecture3 at hJC
apply unitJacobian_does_not_imply_injective
intro P hP
rcases hJC P hP with ⟨Q, hleft, _⟩
exact hleft.injective
#print axioms jacobianDet_F
#print axioms F_not_injective
#print axioms jacobianConjecture3_false