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).
"Less healthy" is distinct from "shortens lifespan" which was pretty much the entire point I was making.
I understand that the idea that there are well-controlled massive studies with enough power to detect differences from weight alone is appealing, but they simply aren't there -- which should tell you that even if the effect exists, it's not strong enough that it should be your primary motivation to lose weight. There are already plenty of reasons to lose weight that don't require lying to people about having a BMI > 20 shortening your lifespan.
If a single article in a low-impact journal cited by a handful of other articles is the only evidence you have, you're guilty of cherrypicking, I'm afraid. The article you're citing is clearly a response to the current medical consensus.
Sounds like absolute BS to me. Even in very large scale studies specifically designed for studying mortality, only morbid obesity has been negatively correlated with lifespan. There is even some evidence that being a little overweight is actually helpful for the very old (essentially, because it gives them more buffer if they get sick enough that they stop eating for a while). A lot of this is because modern medicine has gotten very good at treating stuff like diabetes and other stuff caused by obesity. Your quality of life will undoubtedly improve if you are thinner, but that's not the same thing.
Not super impressed, but I doubt my requests are getting routed to Opus -- it just doesn't seem to be as good at mathematics as it is at code (I found this to be the case last time it was released as well).
Given their "shape stability" design, not necessarily. The three ways that multithreaded access can cause UB are:
* changing the type of the underlying memory (e.g. because it's part of an enum variant and you changed the tag, or because you changed the length of a vector)
* data races (can be defined away by making [effectively] every access Relaxed, as Java does
* use after free (resolved here by reference counting)
In Rust, any type specified like this (all accesses are Relaxed, "shape stable", and reference counted) can already be used in safe code using & references. In theory. But the first property (forcing all accesses to be Relaxed) is very annoying to achieve for arbitrary user data types--even if those types are Copy or other kinds of plain old data--which is a problem e.g. for specifying stuff like sequence locking. The example they give here with bare unions is also very annoying to use in Rust even though this mode of use is safe, because the type system doesn't track which variant is active. So I definitely think there's room to innovate ergonomically here.
(It does seem from the text like this is intended for a single-threaded context, where I think the arguments against Cell are a little less persuasive, but it's still true that it's very awkward to try to figure out how to safely project a Cell down to the exact fields you need to mutate, even though something like LambdaRust will tell you it's safe to do so).
By accepting semantics like this you are, of course, opting out of a lot of potential optimizations around both shared and unique accesses, but you are already doing this in most langauges anyway, so if you're willing to eat the performance cost this can be quite acceptable. The bigger problem (briefly noted in the post) is that the kind of recursive analysis they're proposing doesn't necessarily compose well. Rust explicitly opted out of most types of analysis that can't be efficiently summarized at the function signature level to improve compilation speed. Historically, not being able to efficiently summarize functions that do this kind of stuff has been a big thing that killed attempts to automatically add borrow checking like facilities onto existing C++ code, too. But maybe a language designed for it from the ground up will avoid this problem.
"Being lazy and not doing the assigned task is a sign of intelligence" has never made sense to me. Intelligent people who actually advance the state of the art -- what people claim to want from these frontier models -- exhibit active curiosity. They want to learn and grow and genuinely understand the right answer. I don't pretend to know what exactly could lead to "real" AGI, but I do know that this kind of reward hacking behavior isn't it. Indeed this is the sort of behavior that in humans is considered a sign of being a good test taker -- being very good at memorizing solutions and analyzing the setting and context of the questions to guess what the questioner might be looking for. Being a good test taker is useful in our society primarily because doing well on tests is used as a proxy for the thing we're actually looking for. We should be careful not to confuse the two.
You have to understand that Fil-C primarily exists as a marketing stunt. Once you do, you'll understand a lot of its technical decisions better. Its definition of "memory safety" involves translating C's semantics into those of a related language with arbitrary but technically defined behavior instead of having UB (for example, under some circumstances Fil-C considers it legal to read a value from a totally different, possibly-inaccessible pointer when dereferencing an unrelated pointer). The justification in all cases is that this is not only better than UB, but better than using a safe systems language that prevents these behaviors to begin with, because it applies at the executable level, while the large slowdown is justified because it allows people to use existing C applications unchanged instead of rewriting in a safe language (never mind that these two claims contradict each other). It's also supposedly better than one of the many solutions for C-in-a-runtime (like wasm, or Graal-C) because instead of using a hardened runtime that actually exists in security critical contexts, you get to trust system call wrappers written mostly solo by the author of Fil-C instead.
Against this background, crashing when inline assembly is determined to be doing something the author isn't sure how to deal with is pretty much par for the course -- it's a way to continue to claim that you can port over your old buggy C applications unchanged. You aren't supposed to actually use it.
> I have heard this claim before but I find it unconvincing. I have given up support of movements for which activists have acted cruelly or otherwise immorally.
Most people aren't this particular brand of irrational.
Unfortunately, it is not, and many of its attempts at mathematical proofs have major flaws. You shouldn't trust its proofs unless you are already able to evaluate them--which I think is pretty much all the OP is saying.
I agree. I find it endlessly frustrating and kind of hate what programming has become. But at least for me it meets the minimum bar of "it works if you push things" now. For past models, under no circumstances could I get them to semi reliably solve these kinds of problems correctly without giving them so many "hints" that they weren't actually saving me time. The kind of reasoning I'm talking about is stuff like "can you actually construct a trace from program start for this condition that looks locally reachable?" Past model simply cannot reliably answer such questions as soon as the control flow involves enough hops or requires tracing through enough function calls.
This jives with what I've experienced in the brief time I had access to 5.5 Pro. It's the very first LLM that I feel like I can wrangle into solving tedious, but straightforward, problems correctly. It still makes a ton of mistakes and needs to be very rigidly guided, but it does a pretty good job of tracing its own reasoning and correcting itself in a way that the other models do not.
The downside (not noted in the article, but noted by others here) is cost. It uses tokens at an insane rate, the tokens cost a lot, and using it with subagent flows that you can use to have it tackle large problems with high accuracy costs even more. It is also much "slower" for large scale problems because of context limitations -- it has to constantly rediscover context for each part of the problem, and in order to make it accurate you need to wipe its context before progressing to the next small part, or launch even more agents. For mathematical proofs like these, where the required context to understand the problem and proof besides stuff that's already available in its training set is small and the problems are considered "important" enough, this might not be a problem, but for many of the tasks I would like to use it for (ensuring correctness of code that affects large codebases, or validating subtle assumptions) it definitely is one.
So I think it will be a while before the impressive capabilities of these models really percolate into our lives as programmers, unless you're one of the lucky ones given unlimited access to 5.5 Pro.
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).