commented: 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. commented: 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. commented: 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). commented: 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. commented: That's a correct intuition! When you do formal verification with SMT solvers, you enter pre- and post-conditions around the code you want to check. This is called the "Hoare triple". The SMT solver does the search for you, and if it finds a case that does not satisfy your conditions, that's quite literally called the counterexample. Anecdotally, when I worked for a company doing formal verification, nobody called the search outputs as "bugs" or "vulnerabilities" -- everyone was talking about counterexamples. One reason why this is more correct is that its a result of your specification. I.e., even if it's a correctness issue in a language or a compiler, you cannot really know if its an actual bug or a "feature". commented: Also why most testing is empirical testing; like empirical research, we're looking for counterexamples, not trying to prove a statement. commented: malicious Lean code can run arbitrary commands on your computer — Lean is a programming My modest proposal is to go back in time, and redo Lean so that it can’t run arbitrary commands on your computer. For the all the undoubtedly valid use cases where our theorem proving language needs to execute shell scripts, we can have a superset/extra capabilities. We can call that language Bloated. Forgive me for straying off topic, but I just wanted to yell when I saw this. commented: Something like Rust's unsafe could work well for this, with an additional argument like --unsafe-allow-unsafe to enable using the unsafe constructs. I think many DSL's would benefit splitting the language like this. commented: ooh, thanks for fixing the "merged posts got their comment threads jumbled together" issue!! .