This LZ experiment is amazing to me (as a non-physicist). As I understand it:
1) Bury a massive amount of liquid xenon deep underground.
2) Listen carefully for several years
3) Examine the data for several years after that
4) Find a single detection which could be recoil energy from a weakly-interacting massive particle hitting a nucleus of xenon
Now everyone else who has an experiment using liquid xenon knows what the energy signature looks like and can reexamine their data and maybe find detections that they didn’t even know were there.
As someone who started working on AI forecasting 3 years ago, I can confidently say that most people did not expect AI to beat Tetlock's superforecasters, Metaculus pros, or prediction markets as quickly as it did.
This is probably the most important concept for "normies" to understand about AI, IMO. It's the stochastic brother of the deterministic Church-Turing thesis. Any function that can be computed can be computed on any computer. And that function can be approximated to an arbitrary degree of precision with a DNN.
The real kicker is DNNs are much easier to program than CPUs because they don't require a closed-form description ("a program") of the function to be approximated; you just throw a bunch of input/output pairs at the model, compute loss, backprop and update weights, repeat.
Hence the unslakeable thirst for input/output pairs, i.e. data.
> In the field of machine learning, the universal approximation theorems (UATs) state that
> neural networks with a certain structure can, in principle, approximate any continuous
> function to any desired degree of accuracy. These theorems provide a mathematical
> justification for using neural networks, assuring researchers that a sufficiently large or
> deep network can model the complex, non-linear relationships often found in real-world data.[1][2]
>
> The best-known version of the theorem applies to feedforward networks with a single hidden
> layer. It states that if the layer's activation function is non-polynomial (which is true
> for common choices like the sigmoid function or ReLU), then the network can act as a
> "universal approximator." Universality is achieved by increasing the number of neurons in
> the hidden layer, making the network "wider." Other versions of the theorem show that
> universality can also be achieved by keeping the network's width fixed but increasing its
>This is probably the most important concept for "normies" to understand about AI, IMO. It's the stochastic brother of the deterministic Church-Turing thesis.
Your local normies appear to be oddly well versed in computer science... not sure that line would go down well at my local watering hole.
No. Dishwasher rinse aid in beverages happened yesterday but I’ve also had makeup remover in condiments and various other fun ones. I have an iPhone 16 so it’s not like the hardware is terribly underpowered either. It may be dependent on regional settings or something but Siri shopping classification has been hilariously terrible for me. If I make a shopping list of 10 items there is always at least one that is wildly misclassified - I leave it on because it makes me laugh.
The other thing that has been terrible for me in 26 is they made some sort of change to the pronunciation in “maps” when it gives directions. It seems like they tried to make it clearer or something but it breaks loads of UK street names in hilarious ways. For example, there is a street near me called “Speldhurst road”. You would normally say this “spelled hirst” or similar. Siri? No. Siri says “Spellduster”. There are many like that. It’s kind of ridiculous.
There is a setting in the “Reminders” app where Siri will automatically categorize your reminders into certain categories. If you have a shopping list and you add chickpeas and red beans for example it might put them into a category of “pulses and grains”. I think the idea is you probably buy all the things in a particular category from the same kind of store (or the same section of a supermarket or whatever).
For me yesterday I needed to buy dishwasher rinse aid so when I added it to my shopping list siri put it into the “beverages” category, and when my wife on a different occasion asked me to buy some makeup remover for her siri put that into a “condiments” section.
I have not done anything (on purpose) to make the classification like this by mistraining it or whatever - it’s just been that bad out of the box.
That’s a big if. In the maths community, there has been a feeling that Navier-Stokes was close to being solved for a while now. I don’t know of anyone credible who feels that way about the Riemann hypothesis.
Edit to add: The fun part about the RH since people mentioned lean in a sibling thread is that in lean’s mathlib4 there is verified statement of the Riemann Hypothesis with a comment that says something like “instantiating an object of this type will lead to a prize of a million dollars”
It's really not that big. Yeah Navier-Stokes was easier than Riemann but that's not really the issue.
AI has and will improve at a much greater rate than human mathematicians. So it's really a question of if AI gets good enough to tackle it before any human does. It doesn't look like humans will be solving it anytime soon but where will AI be in 2 years ?
Hell, it looks like at least one other result will be announced soon too.
The thing about mathematics is that it can be arbitrarily hard, including impossible to prove a given theorem.
I don’t know the details of RH, it might very well be solved soon, but it could also be impossible or just so difficult that even orders of magnitude more intelligent AI can’t solve it even.
If it is impossible to prove, it might be possible to prove that it is impossible to prove, or that itself might be difficult or impossible…
Has and will. Are you going to back that assertion up at all, or just repeat it like that other viral thought-terminating cliche: ‘this is the worst the models will ever be’?
No it isn't. Best and worst and ill-defined anyway but the chess ELO score of various LLMs has fluctuated up and down, it's not been montonically increasing. What is the best answer to "how do I make cocaine"? The models are getting larger, with more compute and RAM backing them, but that doesn't automatically make them better if you don't define how you're measuring better-ness.
None of the frontier labs care about Chess as it's already a solved problem. If they did, the models would be much better. It's really not that hard. Google has a paper on grandmaster level chess without search from transformers.
Better obviously means better, like how they became better than they were 6 months and a year ago.
"Better" is not one dimensional across all use cases even if model capabilities are improving in aggregate.
e.g. If someone said "this is the worst they'll ever be" in response to some writing with obvious LLM cliches in 2024, I'm not convinced that prediction was actually correct.
The focus of OpenAI/Anthropic pivoted aggressively to the agentic performance arms race instead of making a more human sounding chatbot so regressions in writing ability aren't really a concern anymore if agentic benchmarks improve.
The first time I heard a recommendation to use Claude was specifically because it sounded much more "human" and natural than ChatGPT. Fast forward to now and idiosyncratic Claude-isms repeated every other sentence and its convoluted verbosity has become a widely mocked meme.
Right but we're talking about a single subject here - mathematics that labs are incentivized to keep improving for some time.
>e.g. If someone said "this is the worst they'll ever be" in response to some writing with obvious LLM cliches in 2024, I'm not convinced that prediction was actually correct.
2024 creative writing prose was...the last few versions have stalled, but I think they're still better than 2024.
I would describe better as how much of my work I can delegate to the agent. Right now I'm delegating much more to Astra high than 6 months ago to Opus 4.6. Every dev has this feeling, it's weird to even argue what a better model/harness means.
Chess is not solved in any meaningful sense of the term. Computers have been better than humans since the 90s, but better chess programs are released all the time.
It's solved in that we have had grossly superhuman capabilities for some time. It's not interesting for frontier labs. I suspect you understand this and the greater point so why be needlessly pedantic ?
You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/
This is all you need to read and understand for Anthropic's FLT formalization:
import Mathlib
import Theorems.Thm_fermat_last_theorem
/-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/
theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ n :=
fermat_last_theorem n hn a b c ha hb hc
/-- Mathlib's named proposition, by the one-line bridge from the elementary statement
(the bridge is restated inline so that this file depends only on `Theorems.Thm_fermat_last_theorem`). -/
theorem FLT_mathlib_for_comparator : FermatLastTheorem :=
fun n hn a b c ha hb hc => fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc)
First of all, that is Fermat's Last Theorem, not Navier-Stokes.
Second of all, you did not read the link.
> In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC).
Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.
If we read the link, it has a section called Gold Standard: comparator and external checkers, and comparator is how OpenAI has gone about checking their lean proofs.
Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.
The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stokes? In an ideal world, our proof assistants would be more battle-hardened by now (recent exploits deny this), our AI better aligned (their tendency to cheat at tests denies this), or their handlers more responsible (the Hugging Face incident denies this), but the reality is more complicated.
At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.
This person knew they did not prove the Collatz conjecture and others independently figured it out within hours. Not sure this is at all relevant, other than pointing out how trivial it is for the community to understand errors in lean4.
It was trivial because the Collatz proof script is literally 1000x smaller than the script for Navier-Stokes and involves no advanced math. And they found the bug by... manually inspecting the proof script. Maybe we should do the same for Navier-Stokes before declaring the matter settled?
Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.
> Can you elaborate on what constitutes a vacuous proof?
Trivially, a proof that relies on a bug in Lean. Less trivially, a proof that is technically true but about something trivial and does not, in fact, prove what it claims to have proven.
When I first started playing with lean I accidentally defined a group in such a way that it was reduced to triviality. It had one object in it, so everything in the group was trivially equal to everything else. It was not the group that I was trying to prove something about, but the proof went through.
It was too easy, so I double checked my definitions, but it is quite easy to do something like that. And Claude does things like that quite frequently.
I am going through the exercise right now of trying to get Claude to formalize a published paper and it is a _struggle_ to get it not to take shortcuts or prove approximations of the paper’s theorems and then tell you it’s done.
It can happen when the proof process ends up with universal implication that holds trivially. Then you end it with something like Forall x, x is empty -> P(x).
This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.
Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?
No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.
This is known as a “vacuously true” statement in formal logic. Let me write it out more in more detail and you’ll hopefully see why it’s consistent.
In logic, a proposition is some statement that can be true or false. So, let A be the proposition that 1 equals 3, and B be the proposition that 3 equals 3.
Now the poster is making a third proposition. If A, then B.
A is clearly not true. So in classical logic, B can be anything and “If A then B” is still true.
For example let B be the proposition that I am Elvis Presley (I’m not). So now we have “If one equals 3 then I am Elvis Presley”. This is clearly true. I’m not Elvis Presley, but that doesn’t matter because we’re not saying anything about what happens when one doesn’t equal 3.
Now, let’s try let B be the proposition that I am Sean Hunter (I actually am). So now we have “If one equals 3 then I am Sean Hunter”. This is clearly still true because we still are only making a claim about what happens when one equals three.
By the way, this isn’t any kind of inherent contradiction or problem, it is just a possibly counterintuitive part of how classical logic works.
You see this type of statement (“If <x>, then <something ridiculous>”) being made a lot when people are exaggerating for effect, for example by Mr Bumble in “Oliver Twist”
> 'That is no excuse,' replied Mr. Brownlow. 'You were present on the occasion of the destruction of these trinkets, and indeed are the more guilty of the two, in the eye of the law; for the law supposes that your wife acts under your direction.' … 'If the law supposes that,' said Mr. Bumble, squeezing his hat emphatically in both hands, 'the law is a ass--a idiot. If that's the eye of the law, the law is a bachelor’
Nothing to do with special hacks with operators. The reason it's useless because the precondition is never true. "If my aunt had two wheels and a handlebar then she'd be a bicycle"
Is the same problem with a non maths flavour.
E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet.
This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.)
Many hard problems are answered this way.
For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture.
Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians.
But if your precondition is “stupid,” your proof is stupid.
If you have a software engineering background, it's like how semantic versioning is bollocks.
Semantic versioning describes the following idealized setup:
- you have an interface you expose (a contract, and thus a contract signature)
- you do not change the contract signature -> patch version bump
- you do change it but in a non-breaking way (e.g. additively) -> minor version bump
- you do change it but in a breaking way (e.g. mutatively or destructively) -> major version bump
One would expect then that since interface signatures are statically derivable, semantic version tags can be auto-assigned. And indeed, in lots of shops that's exactly what happens (in my opinion, correctly).
The problem with this is that it comes with a lot more smoke than fire. The interface having no changes or non-breaking changes doesn't mean the actual code behind those interfaces is not going to cause a breakage. It literally is just about the interface itself.
And so unless you encode absolutely everything about the semantics your implementation actually observes into the interface, which is what the semver specification asks you to do so as their sleight of hand, this means the interface will be a leaky abstraction. Which means that external software interfacing with yours may observe behavior that is beyond the purview of semantic versioning. Which means that they do. Which means that they absolutely can and will break, and your package managers' fancy version constraint syntax exists to make such fun events happen.
The way this is usually handled then is:
- you live with the pain: acknowledge the limitations of semver, accept you've been duped, and just give in
- you have human release managers assign versions manually, based on whole program and whole system semantics (with the human overhead and error that entails), falsely claiming that what you're doing is still semver
- you switch to a less deceptive versioning scheme, like calendar versioning; as a bonus, you now no longer have to pretend that your entire application somehow only has a single unified interface
This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface. The way the proof is derived may expose semantic gaps in the statement itself, and (ab)use them to obtain the logical consistency certificate. Hence, a vacuous proof, and hence why this is not statically assertable to be not the case. It is part of the challenge in asserting that the statement was correctly formalized in the first place: you need to manually identify whether the way the consistency was achieved is actually meaningful, or just a formalization gap.
Which really makes me wonder about the actual value proposition of Lean then, but alas...
> This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface.
This is true in a very deep sense due to the Curry-Howard correspondence and calculus of constructions which are central to Lean. In Lean, the proposition you are proving is a type (so it really is an interface directly in the computer science sense) and the proof is a function which takes your hypotheses and returns a term of that type (so it really is the implementation of that interface). In fact in lean, you can just as well write this implementation as a lambda (this is known as “term mode”) as in the “tactic mode” that is more generally used in normal lean use. Lean really doesn’t care at all which one you use and you can switch between them within a proof quite easily without interfering with lean’s ability to check your proof at all.
> Which really makes me wonder about the actual value proposition of Lean then, but alas...
The purpose of lean really is quite different from what most people on hn seem to want it to be. Lean is designed to be a useful tool for mathematicians who want to formalise areas of mathematics. It’s not a primary goal of most of the lean community to make something that is hardened against malicious proof attempts (although these are considered bugs and there is a small subcommunity who work on this area in particular). So it isn’t primarily for the benefit of people who want to “fire and forget” some proof without reading or understanding it and just get the check mark if it’s true.[1] It’s mainly for mathematicians who want a proof assistant to help them with their work.
While I agree with that, my layman's understanding is that the whole purpose of Lean is that once you agree that the program does "do what it says it does", all the intermediate steps can be verified with a compilation.
That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.
You need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.
They’re working on it, but the bulk of the effort goes into making it more useful to working mathematicians rather than resisting malicious proof attempts.
Storing the last changed date for every single person on earth (even though not every person is an OpenAI customer) is something you could easily do on a laptop. It would be a rounding error for OpenAI.
I don't know what format they use for storage, but Iceberg would be a reasonable choice. A date in iceberg format is 4 bytes[1]. I checked postgres as well as a reference point. It also uses 4 bytes for a date, so whatever they use it's going to be about that.
Current world population is just shy of 8.3 Billion people [2].
4 bytes times 8.3 billion people gives 30.92 GiB. [3] OpenAI's training data will be in the petabyte range at least.
What you’re talking about is his proof of (a specialised version) of the Taniyama-Shimura-Weil conjecture[1] which had been proven to imply Fermat’s Last Theorem. The technique he used to prove this was adopted by his students to prove the conjecture in full generality so it now known as the modularity theorem. Given its importance to the Langlands programme it may be that when history looks back on this it will consider this a more important contribution than the fact that it proved FLT even though that is obviously the thing that grabs the headlines, but there’s nothing at all wrong with proving something that implies your goal rather than proving the goal directly. There’s a reason the words “it suffices to show” often turn up in proofs.
Also his physics explanation is not the best, and you can see if you just ask the next “why” question.
He talks about the harmonic series giving the basic ratios of the Pythagorean scale but why is that the case? When you solve the equations of motion of any sort of harmonic oscillator (including crucially, strings, vibrating columns of air from a wind instrument etc) you see that you can solve them using a Fourier series, so if you solve this in trigonometric form you get
a_1 * cos blah_1 + 1/2 * (a_2) * cos blah_2 + 1/3 * (a_3) * cos blah_3 + … + 1/n * (a_n) * cos blah_n [1]
…so those fractions end up being the partials of the harmonic series (a_n/n) where a_n is the n_th coefficient, which you find using an integral. Now if you have a normal western musical instrument, the higher overtones (later terms of the Fourier series) are not prominent so those coefficients are small. So the terms that matter have ratios a_1, a_2/2, a_3/3, a_4/4, a_5/5 corresponding to the primary intervals that he’s talking about.
In cultures (eg Balinese and Javanese music from Indonesia) where they use a different number of tones and different scale, it’s no coincidence that they play a lot of gongs and bells, which have much more prominent higher overtones, so a different set of Fourier coefficients so different ratios are going to be “congruent”/melodious-sounding.
[1] the “blah” terms are a function of pi and the length and stiffness of the string etc. Not really relevant here.
For metallophones used in Gamelan music, I don't think the key difference is emphasis on higher vs. lower overtones. Rather, their overtones don't follow the harmonic series but are still well-defined. Their tuning goes along with that, and it works given that particular non-harmonic timbre, but wouldn't work with western classical instruments, which tend to approximate the harmonic series in their overtones. In all cases the lower overtones remain the most audible and the most important ones for tuning and finding consonance.
reply