Jweb_Guru

Correct.

Because anything you can do easily with AI is by definition not valuable. I suppose if they really had a monopoly that would not be the case.

Then you aren't actively seeking out interesting things.

The typical human math paper does not have multiple unfixable errors, no.

Literally every single one of these papers was developed with an internal model that not even most OpenAI employees have access to.

Some people seem to absolutely refuse to understand that a lot of open source is done for the authors' personal enjoyment. There is absolutely no reason they have to accept AI contributions, no matter how much the author of this tweet wishes, and plenty of excellent reasons why they might not (e.g. they actually enjoy programming and the practice of programming). This would be true even if AI generated code were completely indistinguishable from human authored code, which it is not.

Unless you are using Anthropic's super secret model that won't be released until 2028 this is a pretty laughable assertion.

Employees at the companies that do this stuff know exactly what these regulations are for and are violating them quite deliberately. They don't actually think it's "government bureaucracy" whatever they tell the public.

The article claims that "for the first time, string theory is testable," when in reality:

* the tests here concern particles that aren't actually known to exist yet * lots of variants of string theory can be invalidated by the (non)existence of particles at particular masses or with particular properties * moreover, this kind of invalidation has already happened on many occasions * as usual it's only some models of string theory that are ruled out

So the headline and article are both kind of rubbish. In this case I wouldn't even say it's just a misleading headline because the article acts as though some (or even lots of) models of string theory getting hypothetically ruled out by a particle having a certain mass is a brand new thing.

Yeah people don't seem to get that the whole point of having a tightly checked kernel is so you don't have to care so much about the rest of it. Tactic heavy proofs have been "slop" long before LLMs got involved, and they lean heavily on the kernel rejecting nonsense.

Yes, clearly it's completely absurd to think that shredding rare books to more cheaply train LLMs is anything but a moral good, which is why there is this entire thread is full of people jumping through hoops to explain how it's technically legal (and therefore fine) and "you wouldn't have bought those books anyway" (I suppose we don't have the choice anymore!) and, most amusingly, "they're actually becoming digitized and searchable this way" (are LLMs stochastic parrots or aren't they?).

People are very desperate to try to claim that something that's somewhat obviously morally wrong is actually highly nuanced, because it makes them feel uncomfortable.

I think maybe a better way of explaining it would be that an uninformative proof by definition needs to be based on proving that the set under consideration must be inhabited without ever defining an object in that set. This generally means you must show the set is inhabited by exploring some abstract properties of the set itself. A single counterexample, by contrast, by itself is a direct proof that the set is inhabited, so you don't necessarily learn any other interesting properties about the set. So it's not really about constructive vs. non-constructive, I think it's closer to e.g. the idea that point-free stuff tends to be more beautiful and meaningful than pointed stuff (which I think most mathematicians would agree with and which really has nothing to do with intuitionism per se).

In this case, I think part of the problem is that there was kind of no good reason to think the Jacobian conjecture was true in > 2 dimensions other than it being kind of hard to find counterexamples. So a really interesting disproof would be one that, e.g., was able to exhaustively classify the counterexamples, or showed why it seemed in practice to be hard to come up with functions violating the conjecture. AFAIK, this doesn't really accomplish either of those things, not even after you learn the procedure that constructed the function -- it kind of tells you why we should have expected to find a counterexample but not how rare such counterexamples are.

Ah, I didn't realize this was a generational thing. I am definitely a "new" intuitionist, so that probably greatly influences my perspective. I suppose that before results like this, the setoid model, etc. were known constructivism was indeed a much more hardline position to have to take!

A direct counterexample is more "informative" in a very literal sense (its truth value doesn't collapse). But the extra proof relevant content we can use here is not that large -- all it means in this case is that we can directly compute the object and its Jacobian, a well as two points evaluating to the same result. That's nice, but it's not that interesting by itself unless I can use the exact constructed form to prove other interesting stuff (and we can! Most of the followup results that immediately followed from the disrpoof come from being able to directly transform this object into counterexamples to other conjectures; if we didn't have constructive proofs of thoe counterexamples, we wouldn't have such procedures). But being more interesting than a completely uninformative counterexample still doesn't mean it's inherently interesting or enlightening. If anything I'd indeed argue constructive arguments are generally less mysterious and magical than nonconstructive proofs -- in some sense, the constructive proof pulls back the curtain and shows you where the trick is.

Because you literally don't have to actually understand the proofs, just the definitions and proposition chain. Most of the code is going to be proving auxiliary lemmas or building up internal definitions that aren't needed to understand the final proposition. Then all you have to do is make sure the proof doesn't use any axioms and you're good. Being able to confidently do this is why proof assistants like Lean are really not just another programming language.

(That's not to say there's no value to making the proof themselves nicer--compilation time and reusability can actually be a really big deal in formalized mathematics!--but it's way less important than it is in software).

I think the constructive position is basically that people's entire issue with lack of excluded middle being absent is just that people like being able to say "P" instead of "~~P" because it sounds better, considering you can prove ~~P for all the classical propositions that use excluded middle.

As a constructivist: we don't disagree :) We just distinguish between "don't disagree" and "agree." Constructive mathematics says it's fine if you want to claim that there's not no counterexample -- you just can't use that in a situation that demands an actual counterexample (like an algorithm that produces a result). This tends to guide people towards looking for results that don't require this kind of indirection, since they apply more broadly and in more kinds of logics -- orthodox constructive results are kind of a lowest common denominator of consistent truth and remain broadly compatible with most axioms, while nonconstructive results often fail in particular models. Which seems like a pretty sane stance to me, but maybe I'm too thoroughly indoctrinated to see how unreasonable it is :P

(Note that this is about excluded middle. There ARE constructive logics with interpretations of excluded middle, e.g. some forms of classical linear logic, but they do not play as nicely with other logics. Constructivists often reject even weak forms of choice for largely the same reasons--there are some forms of choice that are constructively valid in some logics, but these results often fail to hold true in more conventional logics. And the same is true for a whole host of related notions that proof assistants like Rocq reject by default, propositional extensionality (which says that two proofs of the same proposition are equal) and function extensionality (which says functions are equal whenever their results are equal on all the arguments in their domain -- which might seem obviously acceptable until you realize that it's false in most programming languages!) being prominent but much less discussed examples. It's all about remaining broadly compatible with lots of different types of reasoning, not because people think the reasoning is invalid per se).

"Anthropic and OpenAI" it's basically been all ChatGPT outside of this one.

You can go through my commenter history and know I'm no fan of LLMs. I don't overstate LLM capabilities and am highly skeptical of them in general. 5.6 Pro is genuinely pretty good at certain kinds of math problems that just require trying out lots and lots of solutions, mostly because it's stubborn and can run a bunch of instance in parallel. It is NOT good at coming up with unique ideas or recognizing when its proof approach is doomed, and if the correct approach isn't in its "bag of tricks" for tackling a specific kind of problem, it is not going to get it without a lot of guidance. That said: I 100% believe that it's solved the problems people are claiming that it solved.

The way you should read this is (IMO) not that LLMs have somehow achieved AGI, but that a lot of mathematical research is more about knowing a huge amount of mathematical background, being stubborn, and getting lucky with an approach than it is about brilliant insight. Many people who don't think of themselves as particularly mathematically gifted could have made progress on these problems if they were given enough time and were interested enough. What's notably different about 5.6 (and born out in benchmark after benchmark) is that it does seem to genuinely "reason" through stuff at all -- without that, persistence is pretty worthless because the LLM just goes wildly off the rails if it's put to work for long enough (5.6 itself will still do this if it can't find an answer in a reasonable amount of time).

> Why is it only GPT doing this, why not Claude?

Because Claude can't do it. Anyone who tells you that Fable is better than GPT 5.6 at pure math is lying to you.

If you really believe this, try to use GPT 5.6 to prove an open problem you know nothing about. You might get lucky, but if you don't, you will soon discover that 5.6 can make "progress" towards a theorem without actually getting anywhere pretty much indefinitely.

Oh boy this is a cool blog post. Encourage everyone to read it.

I'm honestly not familiar enough with how well-developed graph theory is in Lean to be able to say. The paper is mostly using pretty old results, so it's mostly a matter of whether that stuff has already been formalized or not. Like anything else in software (and Lean proofs are very much software) a lot of it's about infrastructure. It wasn't so long ago that no area of mathematics outside of type theory and formal verification was really built up enough to do "serious" math -- that's changed a lot within the last few years.

What I'm more saying is that we're a ways away from being able to straightforwardly go from an LLM having a paper proof to having that proof formalized in Lean in the general case. Not so much because it's hard for LLMs, more just because it's hard in general unless all that background work has already been done. As more and more of foundational mathematics gets mechanized, it will be easier and easier to check your work in Lean while you work on the proof. For example, AFAIK unit distance has already been mechanized (though the quality of the mechanization effort sounds not great, it still greatly increases our assurance in the proof's correctness).

"But LLMs are prone to hallucinations which can really impact a string of interdependent logic like a proof. So I’m assuming it would respond with something that’s not complete nonsense to this proof most of the time."

Unfortunately in my experience that's not really the case. For me, very often GPT 5.5 (which was a good deal better than Opus at this kind of task) would just get stuck for long periods when working in a logic like Iris. It wouldn't necessarily outright prove nonsense, but it would vastly overclaim what it had proved and failed to get anywhere without a lot of hinting. 5.6 is hopefully a lot better about this.

I absolutely think that with the rise of LLM generated theorems we need mechanization more than ever, yeah. But I felt that was already pretty important for human proofs, too, and people are just more amenable to the idea now that it doesn't take such heroic effort to formalize things.

As far as whether something like Lean could evaluate this proof: sure, if it were mechanized rigorously. But the amount of work that takes to do varies with both subject and complexity of result. In this case, from what other people are saying, the infrastructure for doing graph theory proofs like this isn't as built up as it is for some other areas of mathematics, so it might take a while.

Frontier labs have had multiple major announcements in the past about supposedly novel LLM generated theorems that turned out to be vastly overstating what actually happened. That's part of why they were so (appropriately) cautious with the unit distance proof.

As someone who's used proof checkers a fair amount, if you don't have some high level idea about the proof, it's an open problem, and the hard part isn't some extremely tedious finite case analysis, it's extremely unlikely you'll get anywhere by trying to mechanize by throwing stuff against the wall to get it to typecheck. When people talk about mathematics being a closed formal system as though this trivializes any creative component, what they're omitting is that in type theory like that used by Lean or Rocq, there are two kinds of terms (match statements proving dependent elimination and fixpoints that provide proof by induction) where there's no real way to infer the type from the term. i.e., there are cases where you have to get creative and try to prove something more general than what you actually care about in order to get the proof about the original case to go through. What does "more general" mean? It could mean anything... that's the problem. That's why it's usually advantageous to reformulate the problem in terms of a different abstraction and build on top of existing results, knowing a lot about the literature and the way these kinds of problems tend to be attacked, rather than just chuck random terms over to a proof assistant and hope for the best.

Yeah it's a very very short proof that uses no mathematics developed within the last 30 years. Which doesn't necessarily make it wrong, but in the absence of mechanization in Lean or proper peer review I think this it is premature to post this. Notably the unit distance proof did not fall into this category.

Mostly true on Earth, but not on other planets with lower gravity, and AFAIK it depends on the rock type. Hence why you have Olympus Mons on Mars (or insanely tall ice mountains on Pluto, when that material couldn't form such a steep talus angle on Earth).