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.
Cache, stack, heap, process, thread, socket, file, tcp, http, tls, websocks, socks, soc2???, deadlock, stack, queue, race, atomic, event loop, coroutine, async, database, transaction, index, replication, sharding, consistency, serialization, DNS, load balancer, container, namespace, and so on.
Every sub fields (web/kernel/backend/etc.) has a million/bazillion weird words used in a dozen different contexts and if you read a paragraph of even semi technical software text you will feel like an over stuffed turkey.
Even cache could mean the CPU caches, the page cache, a browser cache, a CDN cache, a Redis cache, or imagine the flurry of words we have that have real world meaning. Session, handle, pool, buffer, stream, channel, event, task, worker, or queue. Generally there is some overlapping meaning but often there isn't.
Learning anything in maths requires weeks of hard effort, learning enough to be broadly comfortable in how an 8086 CPU works can be done in a weekend.
I mean, we do for some things, especially algorithms (Boyer-Moore). Probably for the same reason the mathematicians do -- there aren't readily available real-world analogies.
And I won't even mention the branded future, with its "Google HyperZipper String Search" and "OpenAI/Red Bull speedmaxx distributed consensus algorithm"...
Nah, math is much harder because there is not just the lingo, but also all the math machinery behind it. Each math definition represents some long process behind it, which builds on another process, etc. The knowledge builds on itself , too much more so than computer science.
Similarly, at some point somebody pointed out to me "the reason you're confused is that the bold on that variable means it's a matrix"
whether he succeeded, is debatable. But APL is definitely powerful, succinct and "regular".
In APL you don't infer the operation from the types at all. × is elementwise, +.× is inner product /always/, on scalars, vectors, matrices, whatever. The glyph tells you what happens. Nothing is bold, nothing is inferred, nothing depends on what your professor assumed you'd absorbed.
I've been trying to get into Iversonian languages myself with the book: Calculous on J
https://www.jsoftware.com/help/learning/23.htm is the closest i've found, but wondering if i'm missing something perhaps, Julia?
tyvm
A decade or so ago I wondered if the reason maths was hard was the names being optimised for writing by hand. Everything's single letters if they can get away with it, so when mathematicians run out of Latin alphabet, they use Greek, bold, etc.
Even integration's ∫ is a fancy elongated s.
CS version would be e.g. integral(function=some_named_function, from=a, to=b, with_respect_to=argument_of_function), which may be longer, but is less opaque, especially when you get in so deep there's 3 other people in the world who've looked into this specific problem and you had to invent your own operations.
But that's all an outsider's perspective. I stopped with two A-levels in maths and further maths.
e.g. to use a very simple example on a white board "3" is "overloaded" as:
- the integer 3
- the rational number 3
- the whole number 3
- etc
When you write a proof in Lean, you have to specify the the type of "3" you mean.
Having using Python/Perl and Java over the years, I get that some math folks found handling this daunting or at a minimum friction to getting into using Lean.
LLMs seem to have been a big help here just for the "translate my math notation into a proof" feature.
but then I take a look at literally anything the Haskell people do and realize that it probably wouldn't have helped.
This is one of the great things about Lean becoming used for more and more mathematics: understanding exactly how an operator/function is defined is just an IDE click or few away. It completely removes the ambiguity present in hand-written proofs, although it still can require a lot of reading to actually meaningfully understand the definitions.
That, as well as how long we've been doing it (thousands of years!) and so how much of the more accessible parts we've explored very thoroughly.
Computer science/engineering strays from this, binary systems don't really track nature much, and hence a lot of their own unrelateable nomenclature arises, and then there is math, which is just way far out there on it's own plane of existance.
I like to emphasize that the ideas are usually very simple at their core. Sometimes they map to kinds of objects or reasoning that non-mathematicians use implicitly all the time in their daily lives, mathematicians just have words for them and so are able to use them explicitly.
And I suspect the density of the language/terminology may give the wrong impression about how mathematicians think about the math they are working on. I mean, different people think / experience / practice math differently of course but IME the underlying thought about a particular problem tends to be much looser and concrete than formal math writing would imply.
That more formal language is needed of course because at the end of the day, it is how we communicate our thoughts in the way that other mathematicians can understand them, not to mention how we can check our own thinking
"The special fiber is the associated graded ring.....and that the filtration admits sufficiently simple homogeneous lifts of the three generators, then one might prove"
In any other context I would at least have some degree of intuition about what is being discussed, but in in math? Absolutely no idea. And usually if I start digging and turning over stones to uncover meaning, I'm just met with even more totally dense code-word language. Unlike other fields were digging is usually quick to relieve ignorance, somehow in math it tends to get worse.
I'm sure I am capable of grasping this if I took the time, and perhaps even what is being discussed it rather intuitive, but the incredibly density of the nomenclatic swamp you have to trudge through for math is totally unrivaled.
One unfortunate feature of published pure math research is that often the ideas are quite accessible and straightforward and don't really require special abstractions or terminology, but those get used anyway because for someone who already has a math PhD it saves a bit of effort.
Big wrapping operations like sums, integrals, and matrices, then what's nearby them, give you a very good idea of where things are going context wise.
Some areas are hard in different ways. I could never quite wrap my head around the way logicians have to think. A clever combinatorial bijection is a work of art you probably can explain to a undergrad class easily but good luck coming up with it. And number theorists will throw the kitchen sink at their problems: no area of math is safe from getting used by them.
People who do this have spent years of their life thinking in this language and studying it, so it is going to be hard. We're also not good at communicating the intuition which for algebraic geometry often comes from other fields.
I'm sure having a compact notation is absolutely invaluable for people who dedicate their lives to maths, but for someone with just a passing interest, I find it more obscuring than helpful. I feel the same way about music notation.
Many mathematicians do what you do as well!
Math isn’t necessarily hard, but it’s incredibly dense
A simple statement like let f(x) be a continuous function can carry a lot of definitions
In that statement, if you missed the day in class where they covered continuous functions it might not even register that it’s a well defined term
And that’s the most over simplistic example I could think of
As a math major, I remember that being one of the first lessons I learned, that every single word could be carrying a lot of weight so to look things up in detail if I was ever struggling on a problem. One of the oldest entries in my memory.md file
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.
LLM: This package hasn't made it to production.
ME: are you sure? i see it right here!
LLM: You're right to push back. I inferred that based on weak data. I see now that the package has been deployed!
If the above conversation is typical for me, how could one expect to achieve a sound result by repeatedly prompting an LLM to simply "keep going" in dense mathematical proofs? Perhaps the user in this case had actually checked the LLM's work before issuing the prompt, but I think you see my point anyway.
For posterity, this indeed works for most problems where an agent might give up. LLMs don't inherently know something is impossible.
The phrase I tend to use in my harder prompts to automate this with a sane loop breaker:
> **REPEAT THIS PROCESS UNTIL CONVERGENCE AND YOU ARE OUT OF OPTIMIZATION IDEAS.** You have permission to keep iterating.
"Worked for 88m 24s... >"
"<h1>Complete finite counterexample</h1>"
...
> You should do a breakthrough
This is just as funny and ridiculous as those "make no mistake" prompts.
without someone independently verifying it, it just dangles there
...
I started using "[leave-open" for those.
It lasted for a couple of years, until someone went through and "fixed" them all.
I can use AI for coding after decades of coding. I can't use it for theoretical physics because I can't evaluate the responses.
That is what will happen though to future generations: they won't be able to use it for anything because none of them will have the "decades of coding" experience that you have had the privelege to have without AI.
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.
At the end of the day, even if they are some insane oracle (pun intended), they're still bounded by training data and how it relates to the real world. Even if they're a near perfect tool, we are still the interface between them and our lived experience. If that stops being the case then why do we care about the output?
This assumes it doesn't graduate to just killing all of us and doing it's own thing, but within this paradigm it doesn't really have goals.
A community of those who distract themselves from the perfectly fixable problems in their lives corruptly self-evaluates. They validate each other's stagnation and unwillingness to move by finding flaws in each day that will enable shutting off the flow of any new data while condemning the world and any actions in it. The lay-z-boy they collectively protect appears as corroboration with a broad population but is in reality a repetition whose independence is meaningless since they are all copies of one system, one kind of person in the same kind of trap.
Immobile. Clogging the Suez with their sandbagging ways. Nothing to add except reasons to stay put. No aspiration. Only cynicism. They deserve nothing but all of our contempt.
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.
Another satisfied customer!
"What am I going to do with these?"
"Try to trade them up for a Volkswagen?"
High IQ bros.
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.
It's actually a bit annoying because it primes you to think that the caveats are real, but most of the time it's just something terribly obvious and not a real caveat, but the model probably has some system prompt that tells it to always consider caveats or something like that.
Same as the model starting every reply with a commitment to be "honest". LLMism are fun but I tend to just suppress them via AGENTS.md because they distract me
Where will we be in another 4 years? What a time to be alive!
Possibly somewhere amazing, but see also: https://x.com/pronounced_kyle/status/1768852493092680036
What image hosts work for you? Imgbb? Postimages?
/s
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.
What I do notice however is that LLMs are becoming capable of doing an increasing part of the intellectual work I can do, and usually a lot faster.
Just today I presented an agent framework that can take an informal incident statement and propose infrastructure changes to fix it, all evidence backed. This did nothing I could not to, but it did all 5 test cases in 6 - 12 minutes each. I would have found all of the monitoring indications it did, but it would have taken me a day per test case. The LLM also included sass to silly tickets. ("This is not even worth spending monitoring resources on. It's obviously a configuration problem.")
That's how this is reading to me as well. It's just fast at slogging through a certain level of "simple" transformations.
[0] https://gwern.net/scaling-hypothesis#gwern-difference--effic...
There is clearly intelligence there. We have no way to recognise intelligence other than the appearance of intelligence and this very clearly displays that.
It's also quite clearly different to human intelligence in some notable ways, but not in any that preclude describing it as intelligent. At least for normal non-pedantic definitions of the word.
But there's no way the thinking times would have been that short, of course.
It's clearly much more than that.
We have no way to recognise intelligence other than the appearance of intelligence and this very clearly displays that.
There is about 150 years of cognitive science experimentation in animals that have clarified a little bit how you can actually measure intelligence. Ooorrrrr we can use medieval contempt for scientific thinking and pretend "intelligence" is just some higher intuition that can never be falsified. You know it when you see it, bro! Don't listen to Emily Bender, she's a socialist witch.The point of those cognitive science experiments is that they apply to any animal with a brain and plausibly show a real shared concept of "intelligence" that isn't limited to humans. According to this concept, orcas might be smarter than humans, despite their physiological inability to make tools. It's not a "normal, nonpedantic definition" of intelligence because such a definition would be scientifically meaningless.
Indeed, AI's fundamental sin, going back to Alan Turing, is embracing a definition of intelligence that applies to civilized humans, but not to hunter-gatherers, let alone apes, corvids, and cetaceans. Frustratingly, our modern society has two concepts of intelligence:
- an intuitive, social sense of "how smart is this guy?", which is well-understood and, being highly correlated with IQ, a totally pseudoscientific artifact of human psychology
- the poorly-understood scientific concept I mentioned earlier
If AI researchers cared about scientific thinking, they would be intensely focused on the brains of bees. Insteac they love money and sci-fi but have pure contempt for science, even Demis Hassabis. This is why AI researchers have yet to build a robot that navigates real-world 3D space as intelligently as a cockroach. I don't think any of our grandchildren will live to see a computer smarter than a mouse. (It seems like Fable still struggles with small-number arithmetic. Rodents don't.)
Basically every academic AI researcher in history was doing what you described. The AI industrialists stopped caring 6 years ago once they realized LLMs seem to have been the only thing in 80 years that actually seems to work at any useful level.
There are plenty of pioneering scientists who are either returning to actual AI research (Yann Lecun, Ilya, etc), and plenty who never left (Richard Sutton) who are doing exactly what you are talking about.
That is not true. Alan Turing did not view things that way, his test would say that a dog has zero intelligence. Neither did any of the MIT Lispers. And neither do Lecun or Sutskever or Sutton! They are all focused on human intelligence. None of them are even slightly concerned about an AI which is intelligent before it learns any language.
> the only thing in 80 years that actually seems to work at any useful level
This isn't true either! Mathematica / Maple / etc are "old-fashioned AI" and they obviously work. The Lisp expert systems were also useful, though less so than an LLM.
A second corollary is that rational consciousness and thought is less likely to be contained in language than previously thought, because if language is so simple that a machine can process it, it can't contain consciousness.
Da hole raisin y nat-lang be v. hard is dat i kan rite lik dis an it be cool 4 native engrish speekrs 2 unerstand. LLMs are of course fine with this sentence in exactly the way that Zork's engine couldn't be.
example For, semi-randomise I word order can this like, Yoda worse than, and be understood.
> is no problem for a machine that takes context and probability into account when translating words to the underlying grammar structure.
We had to invent Transformers to be able to do that with reliability anything close to being worth caring about. Transformers have to learn from examples, not be pre-programmed.
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.
Fork Tao’s convo and prompt this (with your own math level described).
GPT did a great job of translating Tao’s questions and concepts (e.g. “pre image”) into a progression I could understand.
“Ok I have a PhD in financial math and undergrad in engineering math. I have almost zero knowledge of polynomial algebra / geometry, I know what a polynomial is and what roots are but not much beyond that. Could you try and explain to my level what questions the user I the conversation has asked and what the agent has responded with, we can probably go user query by user query to build up”
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
Is there any way to tell a conversation's model and thinking level?
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.
The problem is that, what happens to human expertise as people start to use AI earlier and earlier in their careers, so that in 50 years? The problem is that Terry Tao spent decades as a mathematician before ever encoutering AI. Of course he and people his age will be able to drive AI somewhat sanely and use it to their advantage.
But as more people grow up with AI, they will likely not reach levels like Terry Tao because their exposure to AI and the temptation to use it will certainly dull raw human intellect over time.
I feel like to get to Terry's level you need a combination of passion and aptitude for the subject. People that don't want to learn about a topic will always look for shortcuts, which I think represents the vast majority of people. Terry Tao is quite exceptional, and I think exceptional people will still exist even when the "easy" button is bigger than it's ever been.
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.
Is this a breakthrough of something or 'kinda interesting'?
I'll cherry pick a few comment I like. I think they are worth reading but I'll quote a highlight of each one.
From kingstnap https://news.ycombinator.com/item?id=49000867
> If the Jacobian is a nonzero constant everywhere this means that nowhere does the the function flatten out. [...] What was conjectured is that this local invertibility property everywhere would mean global invertibility.
From mswphd https://news.ycombinator.com/item?id=48999959
> it doesn't overturn much. [...] the resolution of this is a "surprise" in that it is a very long open with many failed proof attempts. But the direction it resolved was not surprising.
Can I quote myself? https://news.ycombinator.com/item?id=49007165
> From a comment by j2kun https://news.ycombinator.com/item?id=49000833 , someone asked Fable and there was an almost counterexample in 2d but it uses division too. [Instead of f=x^2+7xy they have something like f=x^2+7x/y so it's not a polynomial.] It looks like the new trick was to use a third variable to avoid the division.
The flow of the whole conversation, with Tao guiding and the model calculating, gave me the feel of Tao perhaps talking to himself - just that each of those model responses would have taken him much longer to calculate by hand.
It would be fascinating to hear Tao talk about what he may have learnt from this, and if it suggests approaches to other problems he might not have considered, as well as an analysis of the original Fable counter-example construction.
Is it something "revolutionary" or just another small brick that will pile up until something really "revolutionary" will happen?
By itself, no consequence. But over time, provided we keep pumping out talented and qualified mathematicians and keep subsidizing costs, we could maybe hit a breakthrough... somewhere... that has real impact.
It's not quite the Reimann hypothesis, but many prominent mathematicians have spent years working on this problem. Yitang Zhang wrote his PhD thesis on it.
Maybe they'll find a solution where P=NP.
That could really throw a wrench into the whole internet thing.
It seems they need an expert human driver for now.
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
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.
In this case, it takes me 12 seconds to see content when first opening the link, and about 18 to re-render content when scrolling.
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