Human mathematicians are being outcounterexampled

Genuinely insane result. I recall my multivariable calc prof last year jokingly stated this conjecture as a bonus problem--it is really very well-known, and quite accessible. A couple points:

• If you are familiar with algebraic geometry--not me!--there seems to be a natural-ish route to constructing the counterexample after the fact (and LLMs are able to give this intuition). So the counterexample is not pulled out from thin air.
• Again in hindsight, there were signs pointing to the conjecture being false--namely there were human-constructed counterexamples to variants of the conjecture prior to this news.
• The conjecture in dimension 2 is still open (the counterexample is a function C^3 -> C^3 in three variables.) there are results showing that a counterexample in dimension 2, if it exists must be quite gnarly, unlike the one here.

That said, I don't think any of the above diminishes how cool this development is: the conjecture is very well-known and mathematicians have spent much time thinking about it over the years. Unlike, say, the unit distance conjecture, my impression is also that the expert opinion on the validity of the conjecture was split, so it's not that no one tried to find a counterexample. Finally, contrary to some nonsensical speculation I've seen, it's not feasible to find this result via brute-force search; the model was certainly not blindly enumerating counterexamples.

There is no doubt this is very impressive. Jacobian conjecture is certainly one of top 100 unsolved math problems, which I can't say about GPT's unit distance conjecture (it is probably top 1000 though). At the end of the 20th century, people proposed successors of Hilbert's problems: I think the contest was won by Millennium Prize Problems, but Smale's problems was the close second. Jacobian conjecture is one of Smale's problems.

A caveat is that you probably shouldn't say AI solved one of Smale's problems which is the 20th century version of Hilbert's problems, because 2 dimension case is open. In case of Poincare conjecture, >4 dimension was proved in 1961, 4 dimension in 1982, until 3 dimension was proved in 2003. Many people thought Jacobian conjecture is false for >2. To prove this is not a post-hoc justification, let me quote Peter Woit from 2004. Here Woit stands for a nonspecialist mathematician, not a notorious string theory skeptic:

The Jacobian Conjecture is one of the most well-known open problems in algebraic geometry. It now seems that a proof has been found by Carolyn Dean of the University of Michigan, for the case of polynomials in two complex variables (for more variables, many people believe it is not even true).

This really feels like the path forward for LLM-directed program search. Formalizing a single kernel was a massive undertaking but I now suspect we are much closer to the dream of stating formal correctness properties of a module and deriving a (proven correct) implementation. There’s still much creativity left for us in choosing and formalizing the theorems and guiding the implementation practicalities. I find it quite exciting.

ooh, thanks for fixing the "merged posts got their comment threads jumbled together" issue!!

Not a mathematician but my intuition is that there must be some overlap in vulnerability search and counterexample search. Both involve finding ways to make complex systems behave badly.