YHK - yet another hacker news clone

What is your estimate for the number of hours to formalize one page of undergraduate mathematics? Maybe you are saying this is close to zero, if/when Mathlib eventually covers all of undergraduate math?

Unless they just swiped the workbooks of the actual mathematicians that where working on the problem using AI and it's in the "next-gen" training dataset.

> People seem to be talking about anything except the actual results with this particular announcement.

To be fair, most people have a fairly good handle on "Does opting out my prompts from training runs actually work?", but not on Navier-Stokes. They discuss what more immediately affects them.

Heck, it’s even astonishing that any sort of generalized computer program could even verify a proof of this magnitude that hasn’t already been codified in a formal verification language. If, and it’s unclear that we’ll ever get the full story, they did draw inspiration from training on (or even directly accessing) rough notes that had been provided by another researcher in prose… the fact that it could leap so rapidly to a full formal verifiable Lean program for the entire scope of the problem is an incredible result in its own right.

I mean, I have a bachelor's in math and I don't imagine I could begin to understand either the human or LLM proofs without a massive investment of time and effort.

>Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time.

I think about this a lot. I'll have to explain to my kids some day that there was long period of time where you couldn't just talk to a computer and have it talk back to you, and that communicating with one required special skills that took years of study to master. It's going to be completely impossible for them to even remotely understand what that was like. Sort of like the pre-electricity days for us, but even more-so.

It also needs to be said: The amount of compute that went into this is something. From some estimates I've seen, the compute cost alone would be around $10m, +/-

As a reference, for that kind of money one could put together a research group of 20-25 researchers, and keep them salaried for 5 years.

So while it is impressive, absolutely no doubt there, the SOTA access is so expensive that it is sort of unobtanium.

Luckily, the prices have historically reduced by a factor of 5-10 every year...but still, only those that swim in cash can afford this.

Aren't you doing exactly the same thing as people you are mentioning? Skipping "talking about actual results" to talking about general capabilities of this LLM and computers in general? because that's exactly what seems like 99% of all people had been doing lately - debating what computer programs can do and what they can't.

Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers

That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people would correctly not be impressed with my ability

Until the plagiarism scandal is sorted out, its not a meaningful result at all, because nobody knows how much genuine innovation these models are displaying

Yep

Can you use Lean to... prove "Lean-fast" is equivalent to Lean?

If they aren't already, or if its possible, prove that an optimized version matches the simple version...

It's because anthropic vibemathed it. I forgot the name but some other guy is working on a handwritten version of it and I bet it'll be more than just 1 magnitude faster.

Nobody wrote 13 mil lines proofs before.

I'm pretty sure you can make Lean at least 10 times faster if you unleash the agents on it.

Somebody ported Doom to run entirely in the TypeScript TYPES (not code). It took 12 days to compile.

https://www.tomshardware.com/video-games/porting-doom-to-typ...

But what hardware was the verification vs agents on? Because you are likely comparing verification on a single beefy machine (say XX TFLOPS total) to agents running on a substantial inference cluster (say XXXX TFLOPS). So you're 1 order of magnitude might actually be 2-4 orders of magnitude.

Weren't the agents massively parallel, whereas the lean verifier presumably is not? Also, I presume said agents were themselves running the verifier on their own parts many times.

> But you see, now you'll have more time for the actual important things!

> Like what?

> Cleaning shit out of clogged toilets!

How could they possibly included in the previous training run which takes months to complete..

See other thread, but yeah that's the general ballpark of the situation.

this is not a rumor (the allegation, anyway), it's reported in the new york times

I don't understand why I'm getting downvoted, I'm not posting an opinion. Coincidences happen. So does foul play. No judgement call here.

Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.

If I understand correctly, the only thing you need to do for correctness is express your axioms and your theorems faithfully. For standard purposes, I assume most of the axioms you want to use are prior art and can be easily reused.

These axioms don’t have to be the core axioms of math. If some other result has been formally proven, I presume you can simply use that result as an axiom.

As long as you do those things, what happens in between is immaterial from a correctness point of view because each of those statements is proved by the statements before them.

That's true of the entirety of mathematics. Its validity is a social construct. That is not to relativize it entirely, but much of what was considered good and sound mathematics in the ancient Agean for example would now fall way short of what mathematicians consider valid proofs.

Mathematics is a human endeavor funded on communicating and sharing mental constructs. Some are useful but most of it is not about producing useful things, quite the opposite in fact.

Gödel showed you need to agree on definitions to even do any valid mathematical construct.

Truth is also ill defined. That's what I don't get about generating math with LLMs. Who cares if you make hundreds of pages and lean code and it gets a thumbs up for logical validity? Mathematics is so much more then concatenating valid logical statements.

I'm sure over the next 6 months both OpenAI and Anthropic are going to continue pouring many many millions of dollars into any famous open mathematical problem like that. There is a limited pool of problems which have held prestige for enough time to make general news headlines when solved and you don't really get nearly as much limelight for proving it the second time or adding in proof for additional cases/forms.

I would say this is why formal proofs (and things like the Lean 4 libs) are so important, so that you can deconstruct the tower provably back into pieces you can understand. It shouldn't be possible to construct a formal proof you cannot destructure like this.

As a (crude) analogy, it's a bit like how you can prove the healthiness of a git tree because it's a graph of content hashes and the tree graph pointers are part of the hash. Imagine this but with a tree of knowledge.

Well that happened already without AI to Mochizuki with his proposed solution to the abc conjecture.

“The Evolution of Human Science” by Ted Chiang, published in Nature in 2000, addressed that exact question:

    The development of the metahumans' science becomes so advanced that it forces the ordinary scientists to switch to interpreting and decoding the metahumans' achievements, because common people are no longer able to create anything fundamentally new.
    https://en.wikipedia.org/wiki/The_Evolution_of_Human_Science

Basically the story told that the only task left to humans is to catch crumbs from the table in that situation. I guess Terence Teo’s “digestion” concept is a step towards that direction.

By formalizing, they mean within a proof assistant like Lean or Rocq, not simply in prose in a textbook. I can attest, 40 hours per page is by no means an overestimate for this sort of work.

you dont have to take headlines literally.