To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.
I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-fre...
which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
I don't dispute the truth of the theorem (since I possess my own proof of it, much more concise than the putative Lean or Wiles proofs, i.e. just a few pages).
The Lean system has already experienced soundness bugs.
The question is, will future generations doublecheck this proof with a frozen Lean system of today? There is a lot of incentive in having LLM's be the first to find high profile theorems like this.
I wouldn't vouch my hand in fire in asserting the validity of this gigantic proof.
Proofs are erasable. If you don't doubt it exists why do you care? Understanding is a side effect. Only people who want to understand the proof would need to care about it.
First I have to say this is sooner than expected, even though I never doubted that this could be done. I am grateful that they dedicated resources to accomplish this. It is clear that agents are very good at discerning and holding onto very weak signals from RL traing on long horizon tasks, so much so that in my own experience even very chaotic agent thinking can converge to meaningful solutions if there is a verifier. I have not dug through the proof yet so I don't know how readable it is to a human. But it has been a dream of mine to understand the FLT proof. I think LLMs will be a big part of making it truly accessible to humans.
Taste or vision? They are hill climbing and they can't see the other side. And sometimes that is because they don't live in your head and don't know what you want.
Very insightful actually. Taste and vision are both instances of holding a model that predicts a good result beyond the threshold of validity in theory but reality happens to align. Is it luck then? Perhaps meta-luck where lucky weights produce “accidentally great” results with some predictability.
Steve Jobs had a mental model that brought the iPhone. No one really wanted it but something in his life biased the result.
So creativity is having weights so good you can project way out into latent space beyond what is reasonable.
I hope you’re not actually trying to compare human cognitive processes to an LLM, because that would be incredibly reductive, not to mention lacking in any empirical grounding.
Nice to get some resonance. And if I may, past --> taste; vision --> future. And to compensate for our poor memory, taste<=>value network while vision<=>policy network, borrowing from RL parlance.
Linear layers use decays (like IIR filters) that naturally provide relative positions. Full attention layers can then be free to develop concepts that attend to each other regardless of distance.
That's not true. First there is still a licensing and quota scheme on the US side for the H200s. Secondly China blocked them for use in inferencing. Thirdly Chinese companies don't want them for training because newer chips are more cost effective.
He says he needs 200,000 GB300s or Huawei Ascend 950s. Now, the GB300 is much faster. So, probably he's just paying a little lip service to the 950 because of political pressure and would prefer the former. It's a moot point though because Hauwei can't manufacture with a low enough defect rate currently.
This also comes with significant capability reduction. deepseek-v4-flash is very good in the < 250K range, then degrades between 250-500K, and is practically unusable after 500K.
[edit]
This is my observation from using it without an specific context engineering to optimize for Deepseek's cache compression and sparse attention mechanisms. I am pretty sure that if you specifically structure your context to align to the cache compression boundaries you can significantly improve performance in the full 1M context, but there is not much reason to do this, because if you design your outer loop to work with shorter contexts that solution is portable and more efficient, so I haven't bothered with a optimizing for DS at this point.
Btw - assuming NeurIPS reviews aren’t garbage tomorrow, I’ll have a paper out which claims that most long context problems in models are really sampling problems in disguise
Switch to a modern sampler like min_p or ideally a better one like top-n-sigma (it’s in llamacpp) and your “my model gets stupid at long context problems” will basically go away.
Unfortunately this fact is still not well appreciated yet despite nearly every modern sampling technique getting an oral wherever they get presented. Min-K just got an oral at ACL 2026, for a hyper recent example of this. There’s a reason they keep getting orals.
The field massively ignored sampling for mostly safety reasons and now the whole field incorrectly believes long context doesn’t work on small models. Long context is an out-of-distribution problem. Your sampler configured properly keeps you in distribution.
Oh and this is doubly true for quantized models. I run my qwen 3.6 27b with 4bit quants from unsloth and get excellent performance because my sampler stack is good and not the garbage that is top_p and top_k. Also, yes, you need to ignore the trash recommended sampler settings from the Chinese labs (they’re wrong/bad).
Interesting. I am not familiar with model internals at this level because I have only been working at the application layer so far, but will definitely research this further. When you get the paper published would appreciate if you can drop a comment with the link so I can read it.
Well, so far as the governments get VAT from the manufacturers, they are getting a return on their investments. They are more like mutualizing the companies than subsidizing them, that is the successful or mature ones are getting taxed to help the nascent ones.
What do you mean? Yield is a function of the chip size and density as well as the process. Plus it's a commercial secret so your bet can't be adjudicated.
As soon as China can get their yields up, they will go all in on exporting these. Until then, they will subsidize them for domestic use. So you can kind of tell where they are by what they do with the chips.
Yield is generally not an issue over time, at least not as big as someone outside of the industry would think, if you get enough chips to work in the first place. For high volume chips, fabs will tune their process specifically for your chip over time. And you can do mask changes just to address yield problems and you can add redundancies if you have to. For example Huawei is no longer bottlenecked by the quantities of chips they can get for their handsets. Their problem is that they can't get the performance they could get with a better process.
Performance is generally limited by the process. Yield not so much. Assuming you can make it at a meaningful level at all, yield is generally a learning process.
reply