QuesnayJr

The Navy was phasing out celestial navigation, but after some public outrage from retired naval officers they brought it back.

I've already seen this sentiment expressed in the wild.

Understanding has been the point of mathematics for millenia. The idea that purpose of math is to produce machine-checkable proofs is an entirely modern idea.

I wonder if this is a hint to a more-specific rumor. Weil constructed what are now known as "abelian varieties of Weil type". In low dimensions the Hodge conjecture has been proven for abelian varieties of Weil type, but it's open in higher dimensions. Maybe that's where they found their counterexample.

The idea that logic is a branch of mathematics is itself a modern notion. Aristotle's logic was part of the trivium (grammar, rhetoric, and logic) in classical notions of education, while mathematics made up several parts of the quadrivium (arithmetic, geometry, music, and astronomy).

Of course in retrospect we can see that the syllogistic part of Aristotle's logic can be formalized (as can grammar), but it was viewed as part of language or philosophy. I get the impression that a lot of more traditional philosophers of logic hated the formal turn.

Leibniz anticipated the turn towards formalism, but he didn't publish any of it in his life and it wasn't rediscovered until the 20th century.

If you go to the individual solutions, the text description tells you if it's stable. There's also a slider that allows you to perturb the orbit so you can see for yourself when you perturb it.

This is exactly backwards. Mathematics predates the idea of formal proof by millenia. The purpose of proofs since Euclid is to explain to your fellow human why something is true. The idea that the purpose of math is formal proof alone is a new idea that (some) computer programmers want to impose on the field (for the understandable reason that it makes computers primary).

Formal proof only emerged early in the 20th century, and the standard became that in theory a proof should be formalizable to answer any skepticism, but the real goal in Euclid's time and ours has been to communicate why a theorem is true to your fellow humans. There were a few theorems that are only known via computer proof, like the Four Color Theorem, but this has always been regarded as disappointing or even controversial, and the fact that there hasn't been any conceptual breakthrough has meant that we didn't learn anything other than the sheer fact that the Four Color Theorem is true. Theorems that produce understanding, on the other hand, typically produce many new ideas that lead to more theorems.

The purpose of scholarship is understanding. This is just as true for science as it is for math. If AI produces a unified theory of fundamental physics, but it's just an opaque blob, physicists will find it just as unsatisfying.

I think it's possible that it will play out that way, and that it's just too soon to see it. Tao was very optimistic about AI up until a few months ago, and I think what's changed is that an AI generated proof isn't that informative unless it is understandable by humans. So far experts are finding the solution to Navier-Stokes incomprehensible, so we only learn one thing (it's false), instead of the hundreds of things we learn from reading a proof we can understand.

Maybe this is a one-off, or maybe in a few weeks we'll figure out how to get AI to explain the proof in terms we can understand. Then math research will accelerate. But maybe it's not a one-off, and by this time next year we will have an oracle that just answers all of our questions, but in such a way that we don't even know what questions to ask anymore. Then AI will just mop up the existing and the subject will end.

If it's a counterexample to BSD, that would be pretty surprising.

It would also be a considerably more impressive achievement, because experts had mostly shifted to Navier-Stokes regularity being false, while as far as I know almost everybody thinks BSD is true. Hodge people seem less sure about.

If either conjecture is true and they prove it, that would be an even bigger success, since the techniques might unlock any number of other theorems.

I wouldn't call it "struggle", but it does seem better at proving "there exists" statements than proving "for all" statements.

I brought this up here at HN, and in the ensuing discussion Buzzard himself replied saying he was somewhat joking (https://news.ycombinator.com/item?id=49011950).

I'm not moving the goalposts. I haven't heard anyone, ever, refer to the Navier-Stokes problem as a top 3 problem in mathematics. People were saying that they thought the solution was in reach a few years ago, before AI was at all capable of research-level mathematics (and the expectation that there was a counterexample).

I am not particularly skeptical of claims about AI, compared to the average here on HN, but that doesn't mean every random piece of hype is warranted. What they did is impressive, even though we now know the only reason they threw so much compute at the problem is that they heard a rumor that someone else was already close. Navier-Stokes is not a top 3 problem in mathematics, and it was the one that was thought closest to being solved.

We've heard from Buckmaster, who says that they demanded a condition of cutting Alpöge of all credit. If true, it doesn't make them look too good.

It seems like this is going to be a PR nightmare, because they are now competing with their own customers. If you're using an LLM to help with your bright idea to cure cancer, you're going to have second thoughts about relying on OpenAI.

Someone has to actually check this. I'm guessing OpenAI had someone check it internally, but it's possible to get it wrong.

Of the seven Millenium problems, Navier-Stokes was the one most thought to be in reach.

I'm not sure what the top 3 problems are. You can make a case for the Riemann Hypothesis and P != NP, but I'm not sure what #3 would be. Maybe the Langlands program? (That one is not as precisely stated as the other two.)

This is pedantic, but isn't only Josaphat the Buddha?

"Descriptive set theory" is a good starting point, though it's the bulk of what set theorists in general do.

It's true that there's an infinite possible set of axioms. It does seem that the types of axioms that have consequences that humans are interested in fall into simple families. For example, many seemingly unrelated questions are settled by assume the existence of very large sets (larger than can normally constructed in set theory).

I don't see how you came to that conclusion, since I'm telling you the actual state of play. There's a big literature on what results require the Axiom of Choice, for example. (The book Handbook of Analysis and Its Foundations covers this thoroughly.) There are many results on what follows from the Continuum Hypothesis or other cardinal arithmetic axioms. There is a big literature on what follows from assuming the existence of large cardinals. There's a separate literature on adding "forcing axioms", like Martin's maximum. There are hundreds of papers on open questions that are settled by adding additional axioms to ZFC, and to identifying the weakest axioms to add to settle various open questions.

In another direction, there's even a literature on what happens when you allow sets to contain themselves as members, like Aczel's Anti-Foundation Axiom. There's literatures on purely constructive versions of set theory, where everything has to be computable. Like I mentioned before (reverse mathematics), there's work on what happens when you adopt much weaker axiom sets, like second-order arithmetic but weak choice principles such as taking Kruskal's tree theorem as an axiom.

So while AI would accelerate this work, the existing body of work on alternate axioms is tremendous. A surprisingly large amount of it translates between systems, and there are precise tools to measure how weak or strong a system is, relative to its competitors.

I'm sure AI could contribute to this, but this is already a well-developed field of mathematics, and most of the consequences of additional axioms have been worked out. (The most productive hypothesis has been what's called "projective determinacy", if you're curious.)

Mathematicians have also gone in the opposite direction, and tried to work out what are the weakest foundations where different results hold. This is called "reverse mathematics".

It wasn't clear that LLMs were up to a Lean translation task of this scale until now. The background required to formalize the FLT proof was tremendous, so many people assumed we would have to wait until all of that was formalized in Lean before we could ask it to formalize Wiles' proof. Now it seems like almost any mathematics paper we can ask an LLM to formalize, including all necessary background, and it can just do it.

Lean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).

Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.

Holy shit. The proof of FLT is a giant detour through several different areas of mathematics, so formalizing it is a lot of work.

An interesting next target would be formalizing the classification of finite simple groups. The original proof scattered over thousands of pages of journal articles, plus Aschbacher and Smith's 1300 page 2 volume monograph. It's so long it's hard to know if there are any gaps. Researchers have been working on a streamlined new proof, but it's already many volumes long.

I was thinking about trying this exact problem with AI. I missed that it had already been solved. It's not that surprising that someone else already tried it. What's surprising is that open problems get solved so quickly now that it's impossible to keep up with them all.

Most of what people think about as part of the Arthur myth are from literary sources, like Lancelot, the Knights of the Round Table, or the Grail quest.

Mallory's Morte d'Arthur.

Most of the Arthur "myth" is deliberately constructed fiction by specific authors, rather than folk myths.

As ducttapecrown said in their comment, you can define an addition on points on elliptic curves. (You can think of an elliptic curve as a cubic equation on the plane, so if you take a line that goes through two points, it will go through a third. There's more work to do to turn it into an addition, but that's the basic idea.)

There are different types of addition, though. A rank two addition would mean it looks like (x, y) + (x', y') = (x + x', y + y'). A rank three addition would mean it looks like (x, y, z) + (x', y', z') = (x + x', y + y', z + z'). Here they found the first example of an elliptic curve where the rank is 30.

If you allow negative integers, you get negative exponents. To accomodate negative exponents, you can expand the domain again, to rational numbers. If you allow rational numbers, then you have to allow rational exponents, which means you can take arbitrary nth roots. Which you could do, but now you're most of the way to the complex numbers (plus roots aren't unique anymore).

As it stands now, the frontier models can prove theorems where the techniques exist in the literature, which it knows better than anyone who's ever lived and won't quit where a human would. There's no way to know if that's true of the Riemann Hypothesis until it's proven.

For example, even if Claude could prove the statement "100% of the zeroes lie on the critical line", that's strictly weaker than the Riemann Hypothesis, so even the best possible version of this result would fall short. (It's an asymptotic result, so it just means the percentage of counterexamples to the Riemann hypothesis goes to zero as their magnitude gets large.)