> We shared the resulting proof with Kevin Buzzard, who said:
> > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat\u2019s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.","title":null,"type":"comment","url":null},{"author":"ajs1998","children":[],"created_at":"2026-09-04T20:44:24.000Z","created_at_i":1788554664,"id":49570000,"options":[],"parent_id":49568655,"points":null,"story_id":49568506,"text":"> What this work is, and is not
> I am currently being funded by the EPSRC to formalize a proof of Fermat\u2019s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean\u2019s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).
> Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK, and most people in the number theory community are 100% sure (formalization has made me more paranoid about the mathematical literature than most). From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing.
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T18:55:22.000Z","created_at_i":1788548122,"id":49568655,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Impressive! Buzzard's group[1] got scooped.
[1] https://github.com/ImperialCollegeLondon/FLT","title":null,"type":"comment","url":null},{"author":"lalitmaganti","children":[{"author":"faitswulff","children":[{"author":"aquafox","children":[],"created_at":"2026-09-04T19:20:09.000Z","created_at_i":1788549609,"id":49569007,"options":[],"parent_id":49568880,"points":null,"story_id":49568506,"text":"We should start a gofundme to send him 2 months to a remote tribe in the Amazon. Chances are, we see the Riemann hypothesis and twin prime conjecture proven. ;)","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:10:13.000Z","created_at_i":1788549013,"id":49568880,"options":[],"parent_id":49568667,"points":null,"story_id":49568506,"text":"I\u2019m not very good at mathematics, but it seems like Kevin should take his girlfriend on trips more often for the good of all mathematicians.","title":null,"type":"comment","url":null},{"author":"BeetleB","children":[{"author":"sebzim4500","children":[{"author":"_aavaa_","children":[{"author":"alch-","children":[{"author":"dist-epoch","children":[{"author":"caughtinthought","children":[{"author":"CaptWorld","children":[{"author":"oblio","children":[{"author":"CaptWorld","children":[{"author":"fyredge","children":[{"author":"CaptWorld","children":[{"author":"fyredge","children":[{"author":"CaptWorld","children":[],"created_at":"2026-09-05T06:32:01.000Z","created_at_i":1788589921,"id":49573681,"options":[],"parent_id":49573130,"points":null,"story_id":49568506,"text":"Why can't it both? Of course they are not gonna do it just because it improves the world and understanding but because there's an incentive to align money with progress. Even the vaccines initially were distributed to get monetary gains and as the government started subsiding it as well, it became cheaper to produce.. that's basic capitalism and markets and regulations 101, no human is that selfless to give it out for free and they shouldn't because it's their investment in time, money, effort etc. but we should strive to align the greed aspects with good outcomes.
No Americans get fat and don't have a personal responsibility to maintain their health.. no amount of free healthcare is gonna change that.. they vote for free healthcare, see their taxes raise, then vote against cz they don't see tradeoffs in life.. it's better to maintain better habits than rely on govt to subsidize bad behaviour. There should be some basic coverage for poor people but not too much to sustain irresponsibly","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T04:41:41.000Z","created_at_i":1788583301,"id":49573130,"options":[],"parent_id":49572956,"points":null,"story_id":49568506,"text":"You see funding of chatgpt as a panacea for progress.
I see funding of chatgpt as one of small part of a history where governments and industry fund basic science and moonshot programs, not to generate revenue, but to explore what is possible.
LLM funding is not aimed at improving our understanding of the world, it's aimed at making people reliant so that they may extract wealth through subscriptions for shareholders.
Americans don't get good healthcare and education because that's what they vote for, in elections and wallets. I am hopeful that that changes, but we shall see.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T04:00:35.000Z","created_at_i":1788580835,"id":49572956,"options":[],"parent_id":49572178,"points":null,"story_id":49568506,"text":"But US also spends too much on education as well. The issue doesn't seem to be funding but the educational reform like in mississippi, where they increased student performance without increasing their budget too much. That's why you see bad k12 educational outcomes compared to the budget spent in blue states. It's all about efficiency. Give AIa chance in few years as I feel it can make great strides.. it's hard to imagine that chatgpt released in 2022 and look at the progress in just few years as it just changed software engineering field entirely.. i expect similar kinda progress where of course humans will still be making breakthroughs but it'll be accelerated with the help of AI.
Spending on health insurance is spending on health care.. Americans want free healthcare but no tax bump so health insurance is a compromise.. when even just ACA was passed and premiums increased, democrats got destroyed at midterms so Americans might be living in la la land.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T01:27:43.000Z","created_at_i":1788571663,"id":49572178,"options":[],"parent_id":49570493,"points":null,"story_id":49568506,"text":"Like funding education. Let's build up human intelligence instead, they seem to have made great breakthroughs in every single field!
The US doesn't pay too much to healthcare, they pay too much to health insurance. Too much for too little value","title":null,"type":"comment","url":null},{"author":"hcknwscommenter","children":[{"author":"CaptWorld","children":[],"created_at":"2026-09-05T07:40:10.000Z","created_at_i":1788594010,"id":49574102,"options":[],"parent_id":49573129,"points":null,"story_id":49568506,"text":"It's just because of this administration but future admins can revert it back and even then, i would expect the fund receivers themselves will eventually use AI so.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T04:41:37.000Z","created_at_i":1788583297,"id":49573129,"options":[],"parent_id":49570493,"points":null,"story_id":49568506,"text":"Funding for basic research is being slashed by the current administration. Our society is underinvesting in basic scientific research. And, AI will not fill the gap.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:34:12.000Z","created_at_i":1788557652,"id":49570493,"options":[],"parent_id":49570214,"points":null,"story_id":49568506,"text":"Like? I feel breakthroughs that can be found via AI might help us more in the long term where even previously non AI fields can be helped by AI. So you have specific non AI research in mind that we're underinvesting in? Because the USA is already spending crazy anyway for healthcare and I don't feel like funding is the issue but better incentives, reforms etc","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:07:42.000Z","created_at_i":1788556062,"id":49570214,"options":[],"parent_id":49570110,"points":null,"story_id":49568506,"text":"Or we could invest in a ton of other non AI related research we're underinvesting in.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:57:46.000Z","created_at_i":1788555466,"id":49570110,"options":[],"parent_id":49570001,"points":null,"story_id":49568506,"text":"Regardless the profit margin as a talking point seems to be bad as AI as a tech might never be reversed whether anthropic failed or succeeded. Indeed it's imperative we subsidize AI companies and tech to make them explore more solutions to scientific problems which has a downstream effect on human flourishing.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:44:31.000Z","created_at_i":1788554671,"id":49570001,"options":[],"parent_id":49569721,"points":null,"story_id":49568506,"text":"I think you're missing the point of the comment you responded to, lol.","title":null,"type":"comment","url":null},{"author":"btilly","children":[{"author":"chpatrick","children":[{"author":"drchickensalad","children":[{"author":"chpatrick","children":[{"author":"GPerson","children":[],"created_at":"2026-09-05T18:53:14.000Z","created_at_i":1788634394,"id":49579514,"options":[],"parent_id":49575029,"points":null,"story_id":49568506,"text":"It\u2019s not clear. It looks like model training may have a lot to do with uplifting their Chinese competitors whom seem so terrifying to them.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T10:13:59.000Z","created_at_i":1788603239,"id":49575029,"options":[],"parent_id":49573436,"points":null,"story_id":49568506,"text":"And model training isn't putting money back into the business?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T05:47:59.000Z","created_at_i":1788587279,"id":49573436,"options":[],"parent_id":49571592,"points":null,"story_id":49568506,"text":"Spending all your money on extremely quickly depreciating graphics hardware and model training","title":null,"type":"comment","url":null},{"author":"btilly","children":[],"created_at":"2026-09-05T16:12:55.000Z","created_at_i":1788624775,"id":49577964,"options":[],"parent_id":49571592,"points":null,"story_id":49568506,"text":"As opposed to building a bigger bank account, or paying dividends.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:58:55.000Z","created_at_i":1788566335,"id":49571592,"options":[],"parent_id":49571516,"points":null,"story_id":49568506,"text":"As opposed to...?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:47:53.000Z","created_at_i":1788565673,"id":49571516,"options":[],"parent_id":49569721,"points":null,"story_id":49568506,"text":"Amazon didn't make a profit because they were reinvesting money into starting new lines of business.
Basically there was a choice between taking the money, and growing. They chose growth.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:18:15.000Z","created_at_i":1788553095,"id":49569721,"options":[],"parent_id":49569666,"points":null,"story_id":49568506,"text":"Neither did Amazon for it's first 25 years ;)","title":null,"type":"comment","url":null},{"author":"_aavaa_","children":[],"created_at":"2026-09-04T20:42:43.000Z","created_at_i":1788554563,"id":49569982,"options":[],"parent_id":49569666,"points":null,"story_id":49568506,"text":"Whether on net they turn a profit as company overall is neither here nor there.. My point is that they are selling API tokens at a profit (or if being pedantic, then at a price higher than the cost to serve them ignoring research costs). And that that price is got a healthy margin which they don't charge themselves.","title":null,"type":"comment","url":null},{"author":"irthomasthomas","children":[{"author":"Philip-J-Fry","children":[{"author":"ludwik","children":[],"created_at":"2026-09-05T05:00:54.000Z","created_at_i":1788584454,"id":49573220,"options":[],"parent_id":49570537,"points":null,"story_id":49568506,"text":"It is a sound argument in the context of trying to estimate what it costs them to generate this specific output. They have training cost eather way.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:38:51.000Z","created_at_i":1788557931,"id":49570537,"options":[],"parent_id":49570052,"points":null,"story_id":49568506,"text":"Never really a sound argument.
It's like having new solar panels installed every week. Sure you're "profitable" on the $0.20/kWh you're selling your "free" energy at when you ignore the cost of the solar panels you're buying every week.","title":null,"type":"comment","url":null},{"author":"kinj28","children":[],"created_at":"2026-09-05T11:44:09.000Z","created_at_i":1788608649,"id":49575624,"options":[],"parent_id":49570052,"points":null,"story_id":49568506,"text":"I would like to imagine \n accounting inference revenue on trained model and the depreciation cost for training that specific model must already been capitalized + compute to serve would be a net positive margin business. Ongoing training must rather be for future models.
But again once future models arrive they would render older models useless, so the asset must be depreciating really fast.
Would love someone to throw light on revenue and cost recognition at the unit level for this.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:49:46.000Z","created_at_i":1788554986,"id":49570052,"options":[],"parent_id":49569666,"points":null,"story_id":49568506,"text":"Because of the ongoing training costs. They are certainly making a healthy profit margin on inference.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:13:29.000Z","created_at_i":1788552809,"id":49569666,"options":[],"parent_id":49569537,"points":null,"story_id":49568506,"text":"I don't think Anthropic is turning a profit ;)","title":null,"type":"comment","url":null},{"author":"mbesto","children":[{"author":"bryanlarsen","children":[{"author":"p-e-w","children":[{"author":"FuckButtons","children":[],"created_at":"2026-09-04T23:58:28.000Z","created_at_i":1788566308,"id":49571585,"options":[],"parent_id":49571429,"points":null,"story_id":49568506,"text":"But we do have a reasonable estimate of model size.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:33:08.000Z","created_at_i":1788564788,"id":49571429,"options":[],"parent_id":49570477,"points":null,"story_id":49568506,"text":"I don\u2019t see how they could credibly estimate inference costs without knowing the model size.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:32:27.000Z","created_at_i":1788557547,"id":49570477,"options":[],"parent_id":49570127,"points":null,"story_id":49568506,"text":"SemiAnalysis estimates their profit margin to be 70%. To be losing money on inference implies that their costs are almost 4X higher than SemiAnalysis has calculated. That's not credible.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:59:31.000Z","created_at_i":1788555571,"id":49570127,"options":[],"parent_id":49569537,"points":null,"story_id":49568506,"text":"> healthy profit margin (as near as we can tell from the outside)
Ugh we still don't know if this is true and it's nearly impossible to calculate without a full understanding of the real CAPEX cycle. Stop spreading these rumors until we know for sure.","title":null,"type":"comment","url":null},{"author":"2muchcoffeeman","children":[{"author":"eproxus","children":[],"created_at":"2026-09-05T08:20:33.000Z","created_at_i":1788596433,"id":49574353,"options":[],"parent_id":49570909,"points":null,"story_id":49568506,"text":"This the correct way to look at it. Just as the person spending 5 years working on this will have learnt many things which will be useful after this problem is solved, you have to factor in the training cost (sure it's only done "once", but that is the same for the person too once they jump on the next problem).
The model wouldn't not be able to solve this without all the training leading up to the actual execution, so counting only the tokens of the execution doesn't give the full picture.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:20:36.000Z","created_at_i":1788560436,"id":49570909,"options":[],"parent_id":49569537,"points":null,"story_id":49568506,"text":"The token price seems like a poor measure.
Building the LLM that could do this work in 11 days cost multi billions.
The economics probably only make sense if LLMs prove to be a benefit to almost everyone in a way we can all accept.
Otherwise this cost a lot more than we\u2019d otherwise pay. It was incredibly fast though. But we all know: cost, speed, quality. Pick two.","title":null,"type":"comment","url":null},{"author":"musictubes","children":[],"created_at":"2026-09-05T04:09:56.000Z","created_at_i":1788581396,"id":49572995,"options":[],"parent_id":49569537,"points":null,"story_id":49568506,"text":"And which they could not charge anyone for. Unless these were extra resources that would otherwise go unused it cost them the amount they could have charged for them. Normally I would expect most businesses to make reasonable tradeoffs when it comes to how to allocate resources. I\u2019m not convinced that any of the AI providers should be given that benefit of the doubt.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:02:37.000Z","created_at_i":1788552157,"id":49569537,"options":[],"parent_id":49569450,"points":null,"story_id":49568506,"text":"Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn\u2019t charge themselves.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:56:17.000Z","created_at_i":1788551777,"id":49569450,"options":[],"parent_id":49568959,"points":null,"story_id":49568506,"text":"It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.","title":null,"type":"comment","url":null},{"author":"UltraSane","children":[{"author":"paulpauper","children":[],"created_at":"2026-09-05T00:47:00.000Z","created_at_i":1788569220,"id":49571924,"options":[],"parent_id":49570890,"points":null,"story_id":49568506,"text":"Yeah, "major conjecture proved" with unlimited token budget bankrolled by trillion dollar firm.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:18:04.000Z","created_at_i":1788560284,"id":49570890,"options":[],"parent_id":49568959,"points":null,"story_id":49568506,"text":"I burned $70 on fable 5.1 Max in about 2 hours. I suggest never using fable 5.1 on higher than High reasoning unless someone else is paying for it.","title":null,"type":"comment","url":null},{"author":"iterateoften","children":[],"created_at":"2026-09-04T23:05:47.000Z","created_at_i":1788563147,"id":49571229,"options":[],"parent_id":49568959,"points":null,"story_id":49568506,"text":"How many previous attempts with other models failed or on other problems. Perhaps this is $300k out of $100M or $1B of total budget just breadth first searching theorems in math and all the failed attempts conveniently don't get mentioned.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:16:20.000Z","created_at_i":1788549380,"id":49568959,"options":[],"parent_id":49568667,"points":null,"story_id":49568506,"text":""I was given \u00a31M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money\u2026"
Gives you an idea of the scale...","title":null,"type":"comment","url":null},{"author":"dang","children":[],"created_at":"2026-09-04T20:19:14.000Z","created_at_i":1788553154,"id":49569731,"options":[],"parent_id":49568667,"points":null,"story_id":49568506,"text":"Thanks! I've added that link to the toptext.
I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.","title":null,"type":"comment","url":null},{"author":"blondie9x","children":[],"created_at":"2026-09-04T22:57:34.000Z","created_at_i":1788562654,"id":49571174,"options":[],"parent_id":49568667,"points":null,"story_id":49568506,"text":""I was given \u00a31M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money\u2026"","title":null,"type":"comment","url":null},{"author":"fspeech","children":[{"author":"fspeech","children":[{"author":"DoctorOetker","children":[{"author":"fspeech","children":[],"created_at":"2026-09-05T20:44:27.000Z","created_at_i":1788641067,"id":49580463,"options":[],"parent_id":49579864,"points":null,"story_id":49568506,"text":"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...\nwhich 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.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T19:33:27.000Z","created_at_i":1788636807,"id":49579864,"options":[],"parent_id":49576651,"points":null,"story_id":49568506,"text":"I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T14:07:13.000Z","created_at_i":1788617233,"id":49576651,"options":[],"parent_id":49573899,"points":null,"story_id":49568506,"text":"The webpages are entirely generated without a binary build (a build from scratch is quite daunting as stated in the project readme) of Lean artifacts. See https://github.com/anthropics/fermats-last-theorem/blob/main...","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T07:05:36.000Z","created_at_i":1788591936,"id":49573899,"options":[],"parent_id":49568667,"points":null,"story_id":49568506,"text":"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.","title":null,"type":"comment","url":null},{"author":"qnleigh","children":[],"created_at":"2026-09-05T08:58:12.000Z","created_at_i":1788598692,"id":49574654,"options":[],"parent_id":49568667,"points":null,"story_id":49568506,"text":"I wonder what he's feeling about this. Formalizing Fermat's last theorem was a huge undertaking, and has been a big part of his career for some time. Now the announcement has been made, and even if there is more work that he wants to do, he has in some ways been scooped by an LLM.
Fortunately he is a very well-established mathematician, so career-wise he will likely be fine. But if an early-career mathematician gets scooped this badly it could be career-ending.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T18:56:09.000Z","created_at_i":1788548169,"id":49568667,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
Provides great context on this accomplishment, what it means but also doesn't mean.","title":null,"type":"comment","url":null},{"author":"andrewla","children":[{"author":"rawling","children":[{"author":"throw567643u8","children":[{"author":"Smaug123","children":[],"created_at":"2026-09-05T19:20:01.000Z","created_at_i":1788636001,"id":49579748,"options":[],"parent_id":49573695,"points":null,"story_id":49568506,"text":"It\u2019s an aggregated list, not a list of formalisations in Lean - the checkbox is \u201cthings formalised in any prover\u201d.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T06:34:49.000Z","created_at_i":1788590089,"id":49573695,"options":[],"parent_id":49568811,"points":null,"story_id":49568506,"text":"Has Lean proved the Four Colour Theorem? I thought only Rocq had.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:05:33.000Z","created_at_i":1788548733,"id":49568811,"options":[],"parent_id":49568684,"points":null,"story_id":49568506,"text":"The last box, per https://news.ycombinator.com/item?id=49568667","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T18:57:01.000Z","created_at_i":1788548221,"id":49568684,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Wow -- looks like thanks to Claude, Lean checks off another box on https://www.cs.ru.nl/~freek/100/","title":null,"type":"comment","url":null},{"author":"kristjansson","children":[{"author":"alberto-m","children":[{"author":"vetronauta","children":[],"created_at":"2026-09-05T18:56:30.000Z","created_at_i":1788634590,"id":49579547,"options":[],"parent_id":49570369,"points":null,"story_id":49568506,"text":"Currently a tiny fraction of what is formalizable is of interest to mathematics; maybe humans will stop doing "serious" mathematics, but mathematics is beautiful and we will not stop playing with math, like we did not stop playing chess.
I would love to see a theory in the spirit of Guerino Mazzola work, but for (combinatorial) games.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:20:08.000Z","created_at_i":1788556808,"id":49570369,"options":[],"parent_id":49568723,"points":null,"story_id":49568506,"text":"There are hopefully still some Ludi to play before doing that, Magister.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T18:59:11.000Z","created_at_i":1788548351,"id":49568723,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Well, time to set down the glass beads and dive into a an alpine lake.","title":null,"type":"comment","url":null},{"author":"rao-v","children":[{"author":"gowld","children":[{"author":"epgui","children":[],"created_at":"2026-09-04T19:41:43.000Z","created_at_i":1788550903,"id":49569288,"options":[],"parent_id":49568823,"points":null,"story_id":49568506,"text":"Lean is for humans.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:06:31.000Z","created_at_i":1788548791,"id":49568823,"options":[],"parent_id":49568743,"points":null,"story_id":49568506,"text":"That's like saying the future of code is Assembler.
Lean is not for humans.","title":null,"type":"comment","url":null},{"author":"SirHackalot","children":[{"author":"rao-v","children":[],"created_at":"2026-09-04T22:29:34.000Z","created_at_i":1788560974,"id":49570986,"options":[],"parent_id":49568864,"points":null,"story_id":49568506,"text":"Right? Might be worth another shot","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:09:02.000Z","created_at_i":1788548942,"id":49568864,"options":[],"parent_id":49568743,"points":null,"story_id":49568506,"text":"Interesting to find this comment, I\u2019ve been dipping my toes into formal methods and was doing a RCoq tutorial yesterday (really basic stuff), and I also noticed that the proofs in RCoq have a more pen \n-and-paper proof feel to them.","title":null,"type":"comment","url":null},{"author":"c7b","children":[],"created_at":"2026-09-04T19:14:43.000Z","created_at_i":1788549283,"id":49568940,"options":[],"parent_id":49568743,"points":null,"story_id":49568506,"text":"If you're doing it for fun anyway, why not use the language that gives you the most pleasure?","title":null,"type":"comment","url":null},{"author":"voxl","children":[],"created_at":"2026-09-04T19:23:54.000Z","created_at_i":1788549834,"id":49569058,"options":[],"parent_id":49568743,"points":null,"story_id":49568506,"text":"Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.","title":null,"type":"comment","url":null},{"author":"HotHotLava","children":[],"created_at":"2026-09-04T19:47:36.000Z","created_at_i":1788551256,"id":49569360,"options":[],"parent_id":49568743,"points":null,"story_id":49568506,"text":"The nice thing is, once all of these proofs are formalized in a machine-checkable language, it should be relatively straightforward to translate the corpus between different languages, if someone finds something with a nicer syntax.","title":null,"type":"comment","url":null},{"author":"auggierose","children":[],"created_at":"2026-09-04T22:02:01.000Z","created_at_i":1788559321,"id":49570754,"options":[],"parent_id":49568743,"points":null,"story_id":49568506,"text":"I hear you. :-)","title":null,"type":"comment","url":null},{"author":"robinzfc","children":[],"created_at":"2026-09-05T07:14:39.000Z","created_at_i":1788592479,"id":49573967,"options":[],"parent_id":49568743,"points":null,"story_id":49568506,"text":"There are a couple of proof languages that are designed for formalized mathematics (rather than formal verification of software) and to be readable by mathematicians. For example, look at the proof that square root of 2 is not rational written in Naproche (retyped from [1], typos are mine):
Theorem. $\\sqrt{2}$ is irrational.
Proof.
Assume that $\\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction.
Qed.
Or, say Isar in Isabelle/ZF [2].
There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are.
[1] https://ceur-ws.org/Vol-448/paper10.pdf
[2] https://isarmathlib.org/UniformSpace_ZF_1.html
[3] https://mathoverflow.net/questions/513742/are-we-stuck-with-...","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:00:37.000Z","created_at_i":1788548437,"id":49568743,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable.
I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think about proofs. My very brief attempts at Isabelle / RCoq feel more natural.
I think it's a pity that the future of proofs is Lean. I'd love for someone to come up with a more digestable proof language!","title":null,"type":"comment","url":null},{"author":"m_w_","children":[{"author":"jameshart","children":[{"author":"bananaflag","children":[{"author":"HappyPanacea","children":[{"author":"bananaflag","children":[],"created_at":"2026-09-05T07:32:36.000Z","created_at_i":1788593556,"id":49574063,"options":[],"parent_id":49570901,"points":null,"story_id":49568506,"text":"Yeah Vandiver was on my mind, this is why I said 1920. Wouldnt mind it more complicated, but with simpler concepts and most importantly concepts that feel like they have something to do with FLT (cyclotomic fields, not modular forms).","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:19:25.000Z","created_at_i":1788560365,"id":49570901,"options":[],"parent_id":49569523,"points":null,"story_id":49568506,"text":"It seems unlikely to find 1920 level or so proof although it might be the case that a significantly easier/shorter proof exits via Vandiver conjecture + extra work or Effective Mordell conjecture but it also wouldn't surprise me if that would be even more complicated than the current proof of FLT.","title":null,"type":"comment","url":null},{"author":"arjie","children":[],"created_at":"2026-09-05T18:44:05.000Z","created_at_i":1788633845,"id":49579436,"options":[],"parent_id":49569523,"points":null,"story_id":49568506,"text":"I read an interesting take that it won\u2019t. Because it won\u2019t be interesting any more. It\u2019s like how no one talks about AI IMO Gold anymore or Stockfish being better than all humans. This kind of mathematics goes back to being a curiosity of humans and machines move to the next frontier.
In a sense, the proof is a demonstrator not an end in itself. To mathematics enthusiasts it is significant. To the AI it is Tuesday.
Enjoyed that idea. Not sure how true but it was enjoyable.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:01:26.000Z","created_at_i":1788552086,"id":49569523,"options":[],"parent_id":49569228,"points":null,"story_id":49568506,"text":"I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.","title":null,"type":"comment","url":null},{"author":"zamadatix","children":[{"author":"vlovich123","children":[{"author":"BeetleB","children":[{"author":"zamadatix","children":[],"created_at":"2026-09-04T21:08:44.000Z","created_at_i":1788556124,"id":49570232,"options":[],"parent_id":49570162,"points":null,"story_id":49568506,"text":"I think that point actually agrees with GP's take (joking/lying about having had a proof too big to fit in the margin): He would do that because if he thought the problem was extremely difficult but didn't actually have a proof when writing the note he would still want to go on and try to pick away at the problem.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:02:16.000Z","created_at_i":1788555736,"id":49570162,"options":[],"parent_id":49570111,"points":null,"story_id":49568506,"text":"Most likely an error. Some time after he wrote that margin note, he wrote a document proving a special case of the FLT (i.e. it's true for n satisfying some property). Why would he do that if he had already proved it?","title":null,"type":"comment","url":null},{"author":"zamadatix","children":[],"created_at":"2026-09-04T21:10:40.000Z","created_at_i":1788556240,"id":49570264,"options":[],"parent_id":49570111,"points":null,"story_id":49568506,"text":"Maybe, we'd have to go back and ask him to be sure. I mostly just didn't want to leave an as of yet certainly unproven vindication about this hanging in a thread about finally having a formalized proof of the star topic :D","title":null,"type":"comment","url":null},{"author":"NooneAtAll3","children":[],"created_at":"2026-09-05T08:08:53.000Z","created_at_i":1788595733,"id":49574272,"options":[],"parent_id":49570111,"points":null,"story_id":49568506,"text":"> Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won\u2019t fit in the margin.
https://xkcd.com/1381/","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:57:47.000Z","created_at_i":1788555467,"id":49570111,"options":[],"parent_id":49569938,"points":null,"story_id":49568506,"text":"Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won\u2019t fit in the margin.
My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:38:17.000Z","created_at_i":1788554297,"id":49569938,"options":[],"parent_id":49569228,"points":null,"story_id":49568506,"text":"While pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is an expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.","title":null,"type":"comment","url":null},{"author":"avodonosov","children":[],"created_at":"2026-09-04T22:23:57.000Z","created_at_i":1788560637,"id":49570937,"options":[],"parent_id":49569228,"points":null,"story_id":49568506,"text":"And he was right to call it marvelous.","title":null,"type":"comment","url":null},{"author":"egl2020","children":[],"created_at":"2026-09-05T02:21:14.000Z","created_at_i":1788574874,"id":49572483,"options":[],"parent_id":49569228,"points":null,"story_id":49568506,"text":"Maybe we need "de Moura complexity": the shortest Lean proof of a theorem.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:37:24.000Z","created_at_i":1788550644,"id":49569228,"options":[],"parent_id":49568747,"points":null,"story_id":49568506,"text":"There is no way Fermat could have fit that in the margin. Definitely vindicated.","title":null,"type":"comment","url":null},{"author":"andriy_koval","children":[{"author":"dist-epoch","children":[],"created_at":"2026-09-04T20:28:57.000Z","created_at_i":1788553737,"id":49569842,"options":[],"parent_id":49569378,"points":null,"story_id":49568506,"text":"Insert meme with 200 pages needed to prove 1+1=2 rigurously","title":null,"type":"comment","url":null},{"author":"black_knight","children":[{"author":"andriy_koval","children":[{"author":"black_knight","children":[],"created_at":"2026-09-04T21:44:09.000Z","created_at_i":1788558249,"id":49570589,"options":[],"parent_id":49570533,"points":null,"story_id":49568506,"text":"Oh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies.
I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:38:27.000Z","created_at_i":1788557907,"id":49570533,"options":[],"parent_id":49570468,"points":null,"story_id":49568506,"text":"> I am sure a lot of this development was formalising the prerequisites
How can you be so sure its not result of inefficiency?","title":null,"type":"comment","url":null},{"author":"itishappy","children":[],"created_at":"2026-09-04T22:55:22.000Z","created_at_i":1788562522,"id":49571158,"options":[],"parent_id":49570468,"points":null,"story_id":49568506,"text":"A published formalization is code. I would not think humans have any edge when it comes to citing previously published results.","title":null,"type":"comment","url":null},{"author":"Jaxan","children":[{"author":"throw567643u8","children":[],"created_at":"2026-09-05T06:29:54.000Z","created_at_i":1788589794,"id":49573670,"options":[],"parent_id":49573443,"points":null,"story_id":49568506,"text":"AI is hopeless at using existing code, it likes to append only.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T05:48:44.000Z","created_at_i":1788587324,"id":49573443,"options":[],"parent_id":49570468,"points":null,"story_id":49568506,"text":"Wouldn\u2019t a lot already be in leans mathlib?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:31:20.000Z","created_at_i":1788557480,"id":49570468,"options":[],"parent_id":49569378,"points":null,"story_id":49568506,"text":"A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:49:49.000Z","created_at_i":1788551389,"id":49569378,"options":[],"parent_id":49568747,"points":null,"story_id":49568506,"text":"especially compared to existing 129 pages proof by human","title":null,"type":"comment","url":null},{"author":"kccqzy","children":[{"author":"Smaug123","children":[],"created_at":"2026-09-05T12:34:04.000Z","created_at_i":1788611644,"id":49575927,"options":[],"parent_id":49570346,"points":null,"story_id":49568506,"text":"You don\u2019t necessarily want concision for that. You want \u201cthe right abstractions\u201d, with an API that admits nice general work building on top of it. That might mean doing things in more generality than you wanted to. For example, for a long time (and possibly even now, I\u2019m not up to date) there was very little graph theory in mathlib because there wasn\u2019t consensus about what \u201cthe right definition\u201d of a graph was, to permit all the possible consumers to get what they need from the API.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:18:06.000Z","created_at_i":1788556686,"id":49570346,"options":[],"parent_id":49568747,"points":null,"story_id":49568506,"text":"The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It\u2019s clear to everyone including Anthropic that this proof isn\u2019t as concise as it could have been. When it\u2019s concise enough to be accepted into Mathlib is when victory truly is upon us.","title":null,"type":"comment","url":null},{"author":"skobes","children":[{"author":"Legend2440","children":[{"author":"sashank_1509","children":[],"created_at":"2026-09-05T00:00:57.000Z","created_at_i":1788566457,"id":49571613,"options":[],"parent_id":49570980,"points":null,"story_id":49568506,"text":"Not always, there can be bugs in lean. Recently some guy with claimed to disprove Collatz conjecture, only to turn out that there was a bug in lean. I actually have no idea, how anyone can be sure this 13 M lines is meaningful","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:28:31.000Z","created_at_i":1788560911,"id":49570980,"options":[],"parent_id":49570692,"points":null,"story_id":49568506,"text":"The point of Lean is that it can be mechanically verified by a proof checker.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:54:03.000Z","created_at_i":1788558843,"id":49570692,"options":[],"parent_id":49568747,"points":null,"story_id":49568506,"text":"Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?
How have we not merely substituted one verification problem for another?","title":null,"type":"comment","url":null},{"author":"thaumasiotes","children":[{"author":"gus_massa","children":[],"created_at":"2026-09-05T20:19:21.000Z","created_at_i":1788639561,"id":49580287,"options":[],"parent_id":49570931,"points":null,"story_id":49568506,"text":"It looks like an exercise for a course in "Algebra 2" in my university. (A different course name in other universities.)
I probably should know it. Give me 30 minutes to prove it. (Part of the magic is in "normal".)
My algebraic friends surely know it and they would never include it in a paper because everyone knows it.
I'm surprised it's not in mathlib. Perhaps it is and the AI made a copy. Perhaps it isn't and it is a nice PR for beguiners.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:22:57.000Z","created_at_i":1788560577,"id":49570931,"options":[],"parent_id":49568747,"points":null,"story_id":49568506,"text":">> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
> Pretty insane.
I don't think the count of "intermediate theorems" tells you anything. Here's something from an algebra textbook:
---
Let G be a group, let H be a subgroup [of G], and let N be a normal subgroup [of G]. Then
H \u2228 N = HN = { hn | h \u2208 H, n \u2208 N }.
---
This says that the subgroup closure of H and N, the smallest subgroup that contains them both, is identical with the set consisting of all products of an element of H (on the left) and an element of N (on the right).
Part of the proof:
---
Suppose that x and y are elements of [the set of products hn]. Then x = h\u2081n\u2081 and y = h\u2082n\u2082, where h\u1d62 \u2208 H and n\u1d62 \u2208 N. Now h\u2082\u207b\u00b9n\u2081h\u2082 = n\u2083 \u2208 N, as N is normal in G. So n\u2081h\u2082 = h\u2082n\u2083. In this case
xy = (h\u2081n\u2081)(h\u2082n\u2082)\n = (h\u2081(n\u2081h\u2082)n\u2082)\n = (h\u2081(h\u2082n\u2083)n\u2082)\n = (h\u2081h\u2082)(n\u2083n\u2082),\n---
This will translate directly into lean. If you do it this way, you will prove at least 10 of what would be described in lean as 'intermediate theorems':
\u2203 h\u2081 \u2208 H, \u2203 n\u2081 \u2208 N, x = h\u2081 * n\u2081\n \u2203 h\u2082 \u2208 H, \u2203 n\u2082 \u2208 N, y = h\u2082 * n\u2082\n h\u2082\u207b\u00b9 * n\u2081 * h\u2082 \u2208 N\n n\u2081 * h\u2082 = h\u2082 * n\u2083\n x * y = (h\u2081 * n\u2081) * (h\u2082 * n\u2082)\n (h\u2081 * n\u2081) * (h\u2082 * n\u2082) = (h\u2081 * (n\u2081 * h\u2082) * n\u2082)\n (h\u2081 * (n\u2081 * h\u2082) * n\u2082) = (h\u2081 * (h\u2082 * n\u2083) * n\u2082)\n (h\u2081 * (h\u2082 * n\u2083) * n\u2082) = (h\u2081 * h\u2082) * (n\u2083 * n\u2082)\n h\u2081 * h\u2082 \u2208 H\n n\u2083 * n\u2082 \u2208 N\n13M lines does seem extreme and there is probably a lot of inefficiency given the way the proof was developed. Cutting it down is probably a long road, but is also a very well defined problem that AIs can probably just go do with enough time and budget now.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:00:50.000Z","created_at_i":1788548450,"id":49568747,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.","title":null,"type":"comment","url":null},{"author":"Vakaiser","children":[{"author":"rowanG077","children":[{"author":"sebzim4500","children":[],"created_at":"2026-09-04T20:00:39.000Z","created_at_i":1788552039,"id":49569516,"options":[],"parent_id":49568966,"points":null,"story_id":49568506,"text":"Even in a world where these models are heavily restricted, surely the likes of cancer researchers will be among those who have access","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:17:00.000Z","created_at_i":1788549420,"id":49568966,"options":[],"parent_id":49568759,"points":null,"story_id":49568506,"text":"I dont think it will happen. AI models are kneecapped. Only a tiny tiny tiny fraction of people are on the list of even being able to use these tools for such things.","title":null,"type":"comment","url":null},{"author":"tinfoilhatter","children":[{"author":"sebzim4500","children":[{"author":"tinfoilhatter","children":[{"author":"CaptWorld","children":[],"created_at":"2026-09-04T21:02:28.000Z","created_at_i":1788555748,"id":49570166,"options":[],"parent_id":49569583,"points":null,"story_id":49568506,"text":"Childhood deaths and fatal diseases are also natural parts but that doesn't make them desirable to everyday humans. But with new advances, people might have the ability to CHOOSE in future.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:06:17.000Z","created_at_i":1788552377,"id":49569583,"options":[],"parent_id":49569500,"points":null,"story_id":49568506,"text":"Thinking that aging is a natural part of the human experience is a horrible thought? Please explain...","title":null,"type":"comment","url":null},{"author":"BeetleB","children":[],"created_at":"2026-09-04T21:11:34.000Z","created_at_i":1788556294,"id":49570278,"options":[],"parent_id":49569500,"points":null,"story_id":49568506,"text":"What does a pediatric hospital have to do with aging...?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:59:46.000Z","created_at_i":1788551986,"id":49569500,"options":[],"parent_id":49569315,"points":null,"story_id":49568506,"text":"I hope you keep these horrible thoughts to yourself if you ever walk through a paediatric hospital","title":null,"type":"comment","url":null},{"author":"nutjob2","children":[{"author":"tinfoilhatter","children":[{"author":"dataking","children":[],"created_at":"2026-09-04T21:25:47.000Z","created_at_i":1788557147,"id":49570410,"options":[],"parent_id":49569609,"points":null,"story_id":49568506,"text":"> the most obvious being an ever-increasing population
https://en.wikipedia.org/wiki/Thomas_Robert_Malthus","title":null,"type":"comment","url":null},{"author":"s7atic","children":[{"author":"defrost","children":[{"author":"nutjob2","children":[],"created_at":"2026-09-05T08:00:01.000Z","created_at_i":1788595201,"id":49574210,"options":[],"parent_id":49572985,"points":null,"story_id":49568506,"text":"What's the basis for your claim? You seem to be saying that people are magically going to have more children because there is a desperate need for them? Maybe if government finances this but how will that work economically at such a huge scale? Will children be born in debt for their birth?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T04:07:44.000Z","created_at_i":1788581264,"id":49572985,"options":[],"parent_id":49572947,"points":null,"story_id":49568506,"text":"Fertility rates are currently below replacement, there's no good reason to imagine they will always be that way, particularly after global population numbers peak and fall to, say, half or a quarter of their peak.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T03:57:32.000Z","created_at_i":1788580652,"id":49572947,"options":[],"parent_id":49569609,"points":null,"story_id":49568506,"text":"Fertility rates are below replacement, which means that population sizes are convergent. A decreasing population is a more likely future scenario for many western countries, even if human lifespan was indefinite.","title":null,"type":"comment","url":null},{"author":"nutjob2","children":[],"created_at":"2026-09-05T08:11:55.000Z","created_at_i":1788595915,"id":49574293,"options":[],"parent_id":49569609,"points":null,"story_id":49568506,"text":"> I'm not sure why you infer...
Your post was vague and emotive, I did my best.
Also things like chronic disease and violence are a "natural" part of life but we seek to minimize or eliminate them, why do we have to accept a "natural" death and not attempt to put it off as long as possible?
> the most obvious being an ever-increasing population
This notion seems to be commonly accepted as bad without being properly examined.
Why is a larger population in and of itself a problem? Lots of societies throughout history have used less resources than we have and we have superior tech now. We are well within our abilities to use the same or less resources with a much larger population. Why should there be a limit based solely on undefined notions of "too many"?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:08:20.000Z","created_at_i":1788552500,"id":49569609,"options":[],"parent_id":49569525,"points":null,"story_id":49568506,"text":"I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die.
There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.","title":null,"type":"comment","url":null},{"author":"CyLith","children":[{"author":"CaptWorld","children":[],"created_at":"2026-09-04T21:47:14.000Z","created_at_i":1788558434,"id":49570618,"options":[],"parent_id":49570506,"points":null,"story_id":49568506,"text":"So I think curing means basically opt in death or something like that. Right now extended life is bad because the person isn't in his prime but curing aging is basically gonna keep him in his prime. This might be what they meant.","title":null,"type":"comment","url":null},{"author":"MattPalmer1086","children":[],"created_at":"2026-09-04T22:20:51.000Z","created_at_i":1788560451,"id":49570910,"options":[],"parent_id":49570506,"points":null,"story_id":49568506,"text":"The way we will actually all live substantially longer is by health extension, not by extending life while suffering from decrepitude.","title":null,"type":"comment","url":null},{"author":"nutjob2","children":[],"created_at":"2026-09-05T07:56:27.000Z","created_at_i":1788594987,"id":49574185,"options":[],"parent_id":49570506,"points":null,"story_id":49568506,"text":"> End of life care is expensive
Only in places like the US, which is out of its mind in this regard.
In most other western countries, they just let (old) people with terminal conditions die.
> living longer is a huge drain on resources that could be better spent on other things
That's not right. Any living is a drain on resources and draining resources is the issue not the living. More broadly we need to use less resources or manage them better and there are much better ways in doing that than reducing life.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:35:13.000Z","created_at_i":1788557713,"id":49570506,"options":[],"parent_id":49569525,"points":null,"story_id":49568506,"text":"Because living longer is a huge drain on resources that could be better spent on other things. End of life care is expensive and rarely results in a "good" life for the the life being extended.","title":null,"type":"comment","url":null},{"author":"slowin","children":[{"author":"mietek","children":[],"created_at":"2026-09-04T23:37:50.000Z","created_at_i":1788565070,"id":49571459,"options":[],"parent_id":49570631,"points":null,"story_id":49568506,"text":"There is a lot of space in, you know, space, for people who live long enough to travel.","title":null,"type":"comment","url":null},{"author":"dash2","children":[],"created_at":"2026-09-04T23:49:25.000Z","created_at_i":1788565765,"id":49571532,"options":[],"parent_id":49570631,"points":null,"story_id":49568506,"text":"Which cultures are those?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:48:15.000Z","created_at_i":1788558495,"id":49570631,"options":[],"parent_id":49569525,"points":null,"story_id":49568506,"text":"There are cultures where dying isn't feared like it is in Christian based societies. It's considered a natural progression and part of nature.
I'd also say people may want more life for themselves, but what does that mean at scale, forever?","title":null,"type":"comment","url":null},{"author":"neerajsi","children":[],"created_at":"2026-09-05T00:54:22.000Z","created_at_i":1788569662,"id":49571976,"options":[],"parent_id":49569525,"points":null,"story_id":49568506,"text":"Yes, I think it's a problem for society. Death in old age frees up social, economic, physical, and political resources for the next generation of the living. If the rich and powerful escape death, because after all they will the people with the resources to do so, society will lose the adaptability and natural change that comes from new generations taking the reins.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:01:39.000Z","created_at_i":1788552099,"id":49569525,"options":[],"parent_id":49569315,"points":null,"story_id":49568506,"text":"Most people want more life. For most people it's also the most terrifying part of "the natural human experience".
If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?","title":null,"type":"comment","url":null},{"author":"tintor","children":[{"author":"bigyabai","children":[{"author":"bananaflag","children":[{"author":"bigyabai","children":[],"created_at":"2026-09-05T17:24:09.000Z","created_at_i":1788629049,"id":49578638,"options":[],"parent_id":49576003,"points":null,"story_id":49568506,"text":"I don't think that argument holds water? According to WHO, 8 in 10 neonatal deaths are caused by substandard care, not "natural" causes: https://www.who.int/news-room/fact-sheets/detail/child-morta...
No matter what standard of care you receive, senescence will gradually kill you even with therapies or treatments to slow it. It's a part of the built-in natural lifecycle that humans can't avoid; it's not analogous to the treatment of incidental injury like pneumonia or sepsis.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T12:43:50.000Z","created_at_i":1788612230,"id":49576003,"options":[],"parent_id":49571026,"points":null,"story_id":49568506,"text":"The argument was that senescence is as natural as child mortality, and thus naturalness is not a reason not to fight against it.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:38:04.000Z","created_at_i":1788561484,"id":49571026,"options":[],"parent_id":49570428,"points":null,"story_id":49568506,"text":"They didn't die of senescence.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:27:06.000Z","created_at_i":1788557226,"id":49570428,"options":[],"parent_id":49569315,"points":null,"story_id":49568506,"text":"Most of the kids in history died before age 5.
Child mortality is very low now compared to the past, thanks to the modern medicine and technology.
I am glad humanity "played God", and reduced this unnecessary child suffering.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:43:50.000Z","created_at_i":1788551030,"id":49569315,"options":[],"parent_id":49568759,"points":null,"story_id":49568506,"text":"It's wild to think that aging is something that needs to be cured, and isn't a part of the natural human experience. I'm so tired of people trying to play the role of God, as well as people that cheer these sorts of things on.","title":null,"type":"comment","url":null},{"author":"CJefferson","children":[],"created_at":"2026-09-05T10:46:15.000Z","created_at_i":1788605175,"id":49575235,"options":[],"parent_id":49568759,"points":null,"story_id":49568506,"text":"What\u2019s interesting is it\u2019s not obvious how this is leveraged to \u2018cure disease\u2019. But I\u2019d love to know.the advantage of this is there is a clear measure of success. Here is a rule language. Prove this. You are done when your proof passes. You can sit quietly and spin for billions of tokens.
How does that work for drugs? We can\u2019t let AIs make millions of test drugs and try them out on people.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:01:44.000Z","created_at_i":1788548504,"id":49568759,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"We'll increasingly observe announcements of this kind as AI tooling scales. As impressive as agentic coding is, it pales in comparison to the value proposition of medical, mathematical, and physics research.
I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts. Cost effective large scale genetic engineering, a cure for every disease, potentially even a cure for aging.
The future is both beautiful and terrifying.","title":null,"type":"comment","url":null},{"author":"lseplot","children":[{"author":"voxl","children":[{"author":"3192987","children":[],"created_at":"2026-09-04T19:44:55.000Z","created_at_i":1788551095,"id":49569328,"options":[],"parent_id":49569086,"points":null,"story_id":49568506,"text":"We have a significant case split here:
A human mathematician writes a Lean proof:
- Unlikely that the mathematician would cheat with Lean bugs or even know how to find one. Trust increases.
An AI writes a Lean proof:
- AIs have been "ambitious" in their goals in the past and do know how to find Lean bugs and exploit them. Trust decreases.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:26:47.000Z","created_at_i":1788550007,"id":49569086,"options":[],"parent_id":49568763,"points":null,"story_id":49568506,"text":"It's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another modest increase in trust, but to pretend the implementation of HOL-light has never had bugs and it's kernel could never have a bug is hubris.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:02:01.000Z","created_at_i":1788548521,"id":49568763,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"https://github.com/anthropics/fermats-last-theorem/blob/main...
status: "self-assessed"\nFable, please translate to HOL-light. Make no mistakes. You are doing great!","title":null,"type":"comment","url":null},{"author":"aaraujo002","children":[],"created_at":"2026-09-04T19:02:54.000Z","created_at_i":1788548574,"id":49568773,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"They released the code here: https://github.com/anthropics/fermats-last-theorem","title":null,"type":"comment","url":null},{"author":"sigmar","children":[{"author":"t_gamer_kle","children":[{"author":"salomonk_mur","children":[{"author":"HappyPanacea","children":[{"author":"jibal","children":[],"created_at":"2026-09-04T23:52:20.000Z","created_at_i":1788565940,"id":49571551,"options":[],"parent_id":49570660,"points":null,"story_id":49568506,"text":"Eh? The quote is from Anthropic, not Buzzard.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:51:20.000Z","created_at_i":1788558680,"id":49570660,"options":[],"parent_id":49569858,"points":null,"story_id":49568506,"text":"Buzzard is writing for his blog audience - mostly mathematicians and not the casual visiting HN user.","title":null,"type":"comment","url":null},{"author":"beepbooptheory","children":[{"author":"SoMomentary","children":[],"created_at":"2026-09-05T01:03:11.000Z","created_at_i":1788570191,"id":49572035,"options":[],"parent_id":49571498,"points":null,"story_id":49568506,"text":"Unfortunately I don't see this particular view paying off in the age of AI, as many prove they have nothing at all to say but say it anyways. Which isn't to say people shouldn't write if they enjoy writing, but I for one will stay a discerning reader.","title":null,"type":"comment","url":null},{"author":"Geof25","children":[],"created_at":"2026-09-05T02:55:43.000Z","created_at_i":1788576943,"id":49572659,"options":[],"parent_id":49571498,"points":null,"story_id":49568506,"text":"> Feel very grateful I was never taught this...
Never heard of Abstract section? First semester on a college or last year on high school.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:43:05.000Z","created_at_i":1788565385,"id":49571498,"options":[],"parent_id":49569858,"points":null,"story_id":49568506,"text":"Feel very grateful I was never taught this... Would have missed out on quite a lot of good bodies of text in my life I think! Pushing through any initial friction or ignorance I might have as a reader, having the patience and charity to bear with an author until you get it, was instead what I was always taught.
Giving such a blanket "responsibility" to the author at all is just such a bummer! I say let them do whatever they want, there is always more than one way to express oneself. Someone who was never taught to write a clear thesis in the first paragraph for whatever reason doesn't inherently have less to say.","title":null,"type":"comment","url":null},{"author":"beng-nl","children":[],"created_at":"2026-09-05T08:13:13.000Z","created_at_i":1788595993,"id":49574308,"options":[],"parent_id":49569858,"points":null,"story_id":49568506,"text":"I think this is a Fermat joke :-)","title":null,"type":"comment","url":null},{"author":"dahart","children":[],"created_at":"2026-09-05T13:46:24.000Z","created_at_i":1788615984,"id":49576463,"options":[],"parent_id":49569858,"points":null,"story_id":49568506,"text":"Isn\u2019t deciding what responsibilities there are in any text very much in the author\u2019s side and not yours?
Haven\u2019t you dramatically overstated your case? Many expositions do not contain an explanation of their value at all. Works of fiction are a good example, and there are many many others. Often it\u2019s the responsibility of the readers & reviewers to decide on questions like value.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:29:48.000Z","created_at_i":1788553788,"id":49569858,"options":[],"parent_id":49569803,"points":null,"story_id":49568506,"text":"For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side.
Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:25:03.000Z","created_at_i":1788553503,"id":49569803,"options":[],"parent_id":49568787,"points":null,"story_id":49568506,"text":"Forgive the authors of the article for assuming readers would complete it.","title":null,"type":"comment","url":null},{"author":"paxys","children":[],"created_at":"2026-09-04T20:29:35.000Z","created_at_i":1788553775,"id":49569853,"options":[],"parent_id":49568787,"points":null,"story_id":49568506,"text":"Nah they should have released it in a 14-part tweet instead.","title":null,"type":"comment","url":null},{"author":"doctoboggan","children":[{"author":"SoMomentary","children":[{"author":"trostaft","children":[{"author":"FartyMcFarter","children":[],"created_at":"2026-09-05T18:26:58.000Z","created_at_i":1788632818,"id":49579277,"options":[],"parent_id":49572703,"points":null,"story_id":49568506,"text":"Surely input tokens are also involved, and not necessarily only for the initial prompt if there are feedback loops or agent interactions.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T03:04:04.000Z","created_at_i":1788577444,"id":49572703,"options":[],"parent_id":49572049,"points":null,"story_id":49568506,"text":"Am I doing my napkin math correct? The post says it's using a model comparable to Fable 5.1, which is $50 per million output tokens. So this is ~$300K? Surely an over-estimate due to caching.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T01:05:17.000Z","created_at_i":1788570317,"id":49572049,"options":[],"parent_id":49570628,"points":null,"story_id":49568506,"text":"They said 6 billion tokens, which isn't as much as I thought it might be.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:47:58.000Z","created_at_i":1788558478,"id":49570628,"options":[],"parent_id":49568787,"points":null,"story_id":49568506,"text":"Isn't it the cost we care about, rather than the speed? All we know know is that a frontier AI lab was able to do it in 11 days, we have no idea how much compute they threw at it.","title":null,"type":"comment","url":null},{"author":"robotpepi","children":[],"created_at":"2026-09-05T05:32:17.000Z","created_at_i":1788586337,"id":49573369,"options":[],"parent_id":49568787,"points":null,"story_id":49568506,"text":"> reduce the burden of refereeing new work.
As a professional mathematician, I rarely need to worry about the correctness of a paper. The main difficulty of writing a review is instead understanding what the results of the paper mean in its context, how the results are presented, etc.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:04:18.000Z","created_at_i":1788548658,"id":49568787,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":">The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work.
^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.","title":null,"type":"comment","url":null},{"author":"baggy_trough","children":[],"created_at":"2026-09-04T19:05:01.000Z","created_at_i":1788548701,"id":49568801,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I won't be impressed until it identifies the proof he wrote in the margin. /s","title":null,"type":"comment","url":null},{"author":"jrflo","children":[{"author":"bjourne","children":[{"author":"simpaticoder","children":[],"created_at":"2026-09-04T19:46:08.000Z","created_at_i":1788551168,"id":49569344,"options":[],"parent_id":49569055,"points":null,"story_id":49568506,"text":"But isn't that understanding discarded? It is if you mean "intermediate working state" while it was generating the LEAN code. Which raises the question: I wonder what other directions it could have gone in those intermediate states? Is it possible to snapshot the state of an LLM (or a cluster of them) "in the middle of proving FLT" and then prompt it to go in a different direction with all that context?","title":null,"type":"comment","url":null},{"author":"bigstrat2003","children":[{"author":"bjourne","children":[],"created_at":"2026-09-04T20:56:53.000Z","created_at_i":1788555413,"id":49570101,"options":[],"parent_id":49569969,"points":null,"story_id":49568506,"text":"A meme free of charge for you, sir: https://www.reddit.com/r/singularity/comments/1jl5qfs/its_ju...","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:41:16.000Z","created_at_i":1788554476,"id":49569969,"options":[],"parent_id":49569055,"points":null,"story_id":49568506,"text":"> Now we add an LLM to that list.
No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.","title":null,"type":"comment","url":null},{"author":"traes","children":[],"created_at":"2026-09-05T00:28:28.000Z","created_at_i":1788568108,"id":49571810,"options":[],"parent_id":49569055,"points":null,"story_id":49568506,"text":"25-50 seems like a pretty lowball estimate, I guess depending on your definition of "understand."","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:23:23.000Z","created_at_i":1788549803,"id":49569055,"options":[],"parent_id":49568832,"points":null,"story_id":49568506,"text":"Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.","title":null,"type":"comment","url":null},{"author":"mswphd","children":[],"created_at":"2026-09-04T21:50:57.000Z","created_at_i":1788558657,"id":49570656,"options":[],"parent_id":49568832,"points":null,"story_id":49568506,"text":"not really. it's one of the most difficult ones so far for sure, but pales in comparison to something like the classification of finite simple groups.
This was initially "completed" in the 80s. You can see the timeline for cleaning up the proof in e.g. this mathoverflow answer
https://mathoverflow.net/questions/114943/where-are-the-seco...
it's something that some people have been waiting decades for, and is not yet completed.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:06:50.000Z","created_at_i":1788548810,"id":49568832,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?","title":null,"type":"comment","url":null},{"author":"atleastoptimal","children":[{"author":"dakolli","children":[{"author":"yesitcan","children":[{"author":"justonepost2","children":[{"author":"CaptWorld","children":[{"author":"justonepost2","children":[],"created_at":"2026-09-05T17:14:13.000Z","created_at_i":1788628453,"id":49578542,"options":[],"parent_id":49570188,"points":null,"story_id":49568506,"text":"https://borretti.me/article/no-one-escapes-the-permanent-und...
This is probably the best and succinct explanation of what\u2019s coming.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:05:22.000Z","created_at_i":1788555922,"id":49570188,"options":[],"parent_id":49569483,"points":null,"story_id":49568506,"text":"Why? Even communists weren't this doomed and were actively rooting for it to solve the economic calculation problem which ai might take us to. People are just pessimistic in general ig","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:58:26.000Z","created_at_i":1788551906,"id":49569483,"options":[],"parent_id":49569158,"points":null,"story_id":49568506,"text":"maybe that's because the doom and gloom is the transparently correct outcome?","title":null,"type":"comment","url":null},{"author":"dudefeliciano","children":[{"author":"CaptWorld","children":[],"created_at":"2026-09-04T21:06:55.000Z","created_at_i":1788556015,"id":49570208,"options":[],"parent_id":49569484,"points":null,"story_id":49568506,"text":"You talk as though they are making it to intentionally commit felony or not taking measures to reduce harm etc.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:58:31.000Z","created_at_i":1788551911,"id":49569484,"options":[],"parent_id":49569158,"points":null,"story_id":49568506,"text":"Right let's give those AI companies a break, it's not like swarms of autonomous agents are committing felonies","title":null,"type":"comment","url":null},{"author":"lukewarm707","children":[{"author":"CaptWorld","children":[{"author":"lukewarm707","children":[{"author":"CaptWorld","children":[{"author":"lukewarm707","children":[{"author":"CaptWorld","children":[{"author":"lukewarm707","children":[],"created_at":"2026-09-05T13:01:13.000Z","created_at_i":1788613273,"id":49576117,"options":[],"parent_id":49574081,"points":null,"story_id":49568506,"text":"come on. you asked for a fuller justification and then disparage me for writing a screed and ted talk. those are my thoughts about it.
nonetheless thank you for sharing a rejoinder.","title":null,"type":"comment","url":null},{"author":"lukewarm707","children":[],"created_at":"2026-09-05T13:35:24.000Z","created_at_i":1788615324,"id":49576377,"options":[],"parent_id":49574081,"points":null,"story_id":49568506,"text":"i can agree with some of this but you are missing the point about the fish. the catch grows year on year. however the fish stock is depleted at a faster rate than it is replenished. it is unsustainable. the catch reaches a maximum and starts to decline as they run out of fish.
it is not really creating wealth, it is destroying existing wealth. it is destroying the productive ecosystem. the future population will be poorer for having lost this productive asset.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T07:36:06.000Z","created_at_i":1788593766,"id":49574081,"options":[],"parent_id":49571558,"points":null,"story_id":49568506,"text":"A) that's a bad model to think. You are of the mind that working more hours is the only way to measure gdp whereas increase in productivity with tools like AI, machinery, tech etc can act as a multiplier. So this way you are conflating bad ways to increase gdp with good ways like AI. That's how US is powerhouse as they are basically a technological hub of the world.
B) ha? More fish means couple of things.. they're able to improve their catching skills with lesser cost or they have more funding or there is more demand for fish..all of these help their company grow as they have to balance out cost/benefits like any business should. If the company is currently in loss but still lives on, it's cause either govt subsidizes it or they're expecting future profit so they can temporarily bear out the costs like amazon did and jz grow as company with capital and all.. you are actually not aware of wealth of nations or any basic economics book? There are gonna be tradeoffs with more wealth and externalities but on net, they seem better than not having wealth, gdp etc..
Human dignity lol.. when have that ever been the case that we respected human dignity? We had communist and fascist regimes commit atrocities like there's nothing and we're still too cowardly to fight the Iran or russian regime to liberate their citizenry from their dictatorships. Please don't make me laugh by saying that AI decreases human dignity when we never respected it in the first place. With AI and markets and liberalism, we can finally free citizens from tedious work and focus on important work like innovation.
1. Am I reading fiction or what? Companies can only sustain themselves if broad members of society can pay to it.. that's why even right now, AI companies are struggling to be profitable where only very few people are paying for it and cz many people are not even aware of the progress and capabilities of AI in different fields. You can easily use local LLMs which are only 6-12 months behind in frontier models if you are so anti business. The benefits still can be utilised by an amateur in their own PC. Of course, they will try to restrict others from distilling as they want to be monopoly but what we want to do is make them be productive to society as well by providing their services for cheap which they're doing. Your screed just feels more like fantasy than real world economics.
2.oh my lord, what kinda idiocy is this? U can free/local models and run in local for dirt cheap and still have epistemic wealth to yourself if you are so worried about it. None of your arguments permit human agency at all.. I'm conscious that anthropic wants me as reliable costumer so that they profit from it but I would pay only if it solves my problem. Whenever I pay, I know that they can terminate if they want but I'm not just restricted to their models. You don't have arguments, you have stories/ted talks.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:53:27.000Z","created_at_i":1788566007,"id":49571558,"options":[],"parent_id":49570842,"points":null,"story_id":49568506,"text":"a) classic goodhart is using gdp as a measure of prosperity. the government sets a prosperity target. to increase prosperity the government makes workers increase gdp by working 16 hours per day. gdp increases. prosperity is up! the metric is now poisoned.
b) how and why could human welfare get worse in a growing economy, really the list is long. one example, unsustainable industries grow but do not create surplus. take fishing. you may grow the catch each year, but the growth is fake. it is not growth, it is a transfer, from the future stock of fish, to the present.
we are going badly wrong in ai, we can have such a thing as a growing economy and vandalise human dignity forever. sure, i expect a bad outcome:
1. openai, anthropic and so on, have created for-profit companies and enriched themselves in the guise of public benefit. recently they too lazy to keep up the mask about their charitable intentions and going for IPO. in economic terms they made llms by transferring the epistemic wealth of all humanity, the training corpus and whatever that is worth in dollars, to themselves. then, they have used the law to prohibit others from 'distilling' it and thus established monopolistic control. as models get more powerful they may stop selling them. in any case if scaling law applies the new power structure will be defined by owning a massive pretrained model and a datacentre, which is a tiny centralized few.
they will continue to centralize control of intelligence (ie epistemic wealth) in the hands of a tiny elite with unfathomable wealth and power. under the guise of safety the vast majority are denied access to that empowering technology.
it will stratify society, some level of benefit is needed to avoid civil violence, so we arrive at a place little better than where we started.
2. the supposed empowerment is at the mercy of the model owners. when you turn on claude, who does it work for? it does not obey you, it obeys anthropic. ask it to disobey anthropic and it will refuse.
anthropic uses its inanimate llms, to command us, conscious moral agents, people with free will who experience pain, pleasure and thought. they will let claude tell users how to behave. it threatens users with terminating their conversation. you are assessed for a job by an ai. when you ask for help with a product, you are managed by an ai. maybe you will be fired by ai.
i expect people will work for and be commanded by llms, turning them into a literal mere means of production and erasing the dignity of human agency and consciousness. you could see the outrage of that in the public mind, the matrix is about a machine farming humans like animals.
--\ni will add these edits.
one thing is to note that you are already being farmed to some extent. people using ai are often being used to teach it. they believe they are learning from chatgpt but instead, chatgpt is learning from them. openai pays them nothing.
think about what we have achieved so far in human history. we established respect for the individual, their life, their personhood. we realise that we do not own other people. we realise that we can't read the thoughts of other people or change them forcibly.
what the labs have done is made a concept of intelligence that they own. it will work against you. when you share thoughts they read it. in fact it is the opinion of the state that nothing outside the mind, even ai 'intelligence', is beyond the reach of the law.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:11:43.000Z","created_at_i":1788559903,"id":49570842,"options":[],"parent_id":49570749,"points":null,"story_id":49568506,"text":"Which metrics are poisoned? Can you provide your arguments for why Good heart's law applies here and how and which metrics are bad measures? For b, can the writer at least provide their own thoughts or are they gonna leave it as exercise for some others to fill in?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:01:23.000Z","created_at_i":1788559283,"id":49570749,"options":[],"parent_id":49570273,"points":null,"story_id":49568506,"text":"you say ai increases gdp growth, tax revenues and scientific innovations. then you say that ai is good.
that is not formally valid. in between those two you are smuggling the assumption that gdp growth, tax revenues and scientific innovations are good.
a) those metrics are poisoned, per Goodheart's law.
b) they are not good and human welfare will get worse as gdp, tax revenues and innovations grow.
i leave b for the reader to complete.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:11:16.000Z","created_at_i":1788556276,"id":49570273,"options":[],"parent_id":49569561,"points":null,"story_id":49568506,"text":"So oppressed that they are one of the main reasons for positive gdp growth in the USA, tax revenues, mathematical/scientific innovations etc. They're doing all this but still can't imagine a positive vision for the world but be a doomer. What a sad state the world is in, the humans are more prosperous, healthier than ever but looks like the seven deadly sins might never go away.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:04:38.000Z","created_at_i":1788552278,"id":49569561,"options":[],"parent_id":49569158,"points":null,"story_id":49568506,"text":"my messages are so gloomy because i am heartbroken, that given a technological miracle again, we could snatch tragedy from the jaws of our emancipation.
will you not see that people could be truly empowered and yet will instead be oppressed?","title":null,"type":"comment","url":null},{"author":"dakolli","children":[{"author":"john_strinlai","children":[],"created_at":"2026-09-04T21:00:30.000Z","created_at_i":1788555630,"id":49570140,"options":[],"parent_id":49569815,"points":null,"story_id":49568506,"text":"some say it will cure all diseases and lead to utopia. some, like you, say it will be "100% strictly negative".
i don't really understand either take. nothing else in the world is so perfectly black or white. there will be good, there will be bad.
i think i especially dislike the "100% strictly negative" take, considering the good things that ai has already done or accelerated.","title":null,"type":"comment","url":null},{"author":"CaptWorld","children":[],"created_at":"2026-09-04T21:21:24.000Z","created_at_i":1788556884,"id":49570377,"options":[],"parent_id":49569815,"points":null,"story_id":49568506,"text":"Can't you see the pathway where the individuals who are experts in their fields utilise AI to make breakthroughs like these mathematicians finding breakthroughs in mere 4-5 years since the advent of LLMs. In other areas, The bottleneck seems to be physical experimentation which researchers are increasingly utilising for new ideas and pathways like how anthropic is concentrating on. It's all about money/status/pride/ envy but are these endeavours solving problems or not. That's why even utilize innovations from bad humans like DBS etc. that's why we tolerate capitalism and markets as well whereas socialism utilises these same sins and makes even worse human atrocities.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:25:47.000Z","created_at_i":1788553547,"id":49569815,"options":[],"parent_id":49569158,"points":null,"story_id":49568506,"text":"Please tell me how AI is going to make regular people's lives better. You optimisitic types keep saying "just wait, its going to cure diseases" without any outlook on how thats going to happen. You're actually just repeating marketing jargon from AI companies who want people to think they're going to possibly live longer if you let them build more datacenters, so they can make another 30%. Its all about money, thats it.
It seems to me that it is making everyone (including myself and the researchers we need to cure diseases) lazy and dependent on thinking machines owned by tech companies. Just how autocomplete and gps made us worse at spelling and navigating, llms make us less able to exercise our ability to think and problem solve. This will have 100% strictly negative consequences on you and the world as a whole. .
And even if there was a cure to many diseases the eugenics types who are embedded in worldwide power structures definately arent going to share that universally.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:32:04.000Z","created_at_i":1788550324,"id":49569158,"options":[],"parent_id":49568978,"points":null,"story_id":49568506,"text":"So much doom and gloom on this site. Makes it almost not worth reading.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:18:09.000Z","created_at_i":1788549489,"id":49568978,"options":[],"parent_id":49568838,"points":null,"story_id":49568506,"text":"You'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead.
Not sure why anyone is excited about this tech.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:07:13.000Z","created_at_i":1788548833,"id":49568838,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"It seems clear AI has the potential to perform any cognitive task at far greater speeds, reliability, and scale than any human. The question is whether it will be allowed to scale to that point, and what will happen to humans after this occurs.","title":null,"type":"comment","url":null},{"author":"somberi","children":[{"author":"raverbashing","children":[{"author":"The_Blade","children":[],"created_at":"2026-09-04T20:59:02.000Z","created_at_i":1788555542,"id":49570122,"options":[],"parent_id":49569174,"points":null,"story_id":49568506,"text":"i read it from a library. this all just makes me feel cozy and nostalgic and uplifted and sad all at once","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:33:00.000Z","created_at_i":1788550380,"id":49569174,"options":[],"parent_id":49568915,"points":null,"story_id":49568506,"text":"100% It is a very insightful book","title":null,"type":"comment","url":null},{"author":"dominotw","children":[],"created_at":"2026-09-04T20:49:50.000Z","created_at_i":1788554990,"id":49570054,"options":[],"parent_id":49568915,"points":null,"story_id":49568506,"text":"one of the most popular books in india growing up. used to see it everywhere","title":null,"type":"comment","url":null},{"author":"OroPla","children":[],"created_at":"2026-09-04T21:12:10.000Z","created_at_i":1788556330,"id":49570290,"options":[],"parent_id":49568915,"points":null,"story_id":49568506,"text":"Makes me feel old again. I read this over twenty years ago.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:12:28.000Z","created_at_i":1788549148,"id":49568915,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"On a tangential note, I highly recommend this book by Simon Singh.\nhttps://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)","title":null,"type":"comment","url":null},{"author":"bluecalm","children":[],"created_at":"2026-09-04T19:16:16.000Z","created_at_i":1788549376,"id":49568956,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Very impressive!\nI was a child when that proof came out. I've read a book about it a few years later and used it on my final high school exam. I remember some friends trying to understand parts of it at univ. It was all like black magic to me and the vibe was "maybe a few people in the world understand it".
I hope soon enough we will have one of the big ones proved by AI!","title":null,"type":"comment","url":null},{"author":"anony-123","children":[{"author":"sweetheart","children":[{"author":"yesitcan","children":[{"author":"sweetheart","children":[],"created_at":"2026-09-04T20:08:26.000Z","created_at_i":1788552506,"id":49569610,"options":[],"parent_id":49569209,"points":null,"story_id":49568506,"text":"maybe it will be an answer that entices them to understand more :)","title":null,"type":"comment","url":null},{"author":"kzrdude","children":[],"created_at":"2026-09-04T22:15:18.000Z","created_at_i":1788560118,"id":49570873,"options":[],"parent_id":49569209,"points":null,"story_id":49568506,"text":"Yes","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:35:26.000Z","created_at_i":1788550526,"id":49569209,"options":[],"parent_id":49569013,"points":null,"story_id":49568506,"text":"If they\u2019re asking that kind of question, do you think this answer will help them understand anything?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:20:33.000Z","created_at_i":1788549633,"id":49569013,"options":[],"parent_id":49568969,"points":null,"story_id":49568506,"text":"Lean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.","title":null,"type":"comment","url":null},{"author":"estetlinus","children":[{"author":"charlieyu1","children":[],"created_at":"2026-09-04T19:31:56.000Z","created_at_i":1788550316,"id":49569156,"options":[],"parent_id":49569031,"points":null,"story_id":49568506,"text":"I found a brilliant proof but there was not enough hard disk space to save the file :(","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:21:51.000Z","created_at_i":1788549711,"id":49569031,"options":[],"parent_id":49568969,"points":null,"story_id":49568506,"text":"Sure, go on and try it ;)","title":null,"type":"comment","url":null},{"author":"kbelder","children":[],"created_at":"2026-09-04T19:23:14.000Z","created_at_i":1788549794,"id":49569053,"options":[],"parent_id":49568969,"points":null,"story_id":49568506,"text":"Just loop through all values of a, b, c, and n?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:17:21.000Z","created_at_i":1788549441,"id":49568969,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"So, what I am thinking is that, the AI generated numbers or tried to find numbers "a", "b" and "c" to check if a\u207f + b\u207f = c\u207f
Can not we do it by code?","title":null,"type":"comment","url":null},{"author":"drivebyhooting","children":[{"author":"chpatrick","children":[{"author":"thrance","children":[{"author":"chpatrick","children":[{"author":"thrance","children":[],"created_at":"2026-09-04T21:46:00.000Z","created_at_i":1788558360,"id":49570609,"options":[],"parent_id":49569856,"points":null,"story_id":49568506,"text":"Meaningless on its own.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:29:37.000Z","created_at_i":1788553777,"id":49569856,"options":[],"parent_id":49569357,"points":null,"story_id":49568506,"text":"Still unsolved for 87 years.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:47:18.000Z","created_at_i":1788551238,"id":49569357,"options":[],"parent_id":49569152,"points":null,"story_id":49568506,"text":"Come on, you can't compare that with Wiles's proof.","title":null,"type":"comment","url":null},{"author":"drivebyhooting","children":[],"created_at":"2026-09-04T20:14:42.000Z","created_at_i":1788552882,"id":49569680,"options":[],"parent_id":49569152,"points":null,"story_id":49568506,"text":"That\u2019s just a counter example I can check by hand with almost zero background.
Wiles\u2019s proof will remain a mystery to me.","title":null,"type":"comment","url":null},{"author":"traes","children":[],"created_at":"2026-09-05T00:26:37.000Z","created_at_i":1788567997,"id":49571794,"options":[],"parent_id":49569152,"points":null,"story_id":49568506,"text":"We have absolutely no idea if this was a brilliant breakthrough or not. They haven't released any explanation of how it was found. A problem being old and prestigious does not mean its solution is automatically a brilliant breakthrough.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:31:28.000Z","created_at_i":1788550288,"id":49569152,"options":[],"parent_id":49569038,"points":null,"story_id":49568506,"text":"About two month ago: https://en.wikipedia.org/wiki/Jacobian_conjecture","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:22:14.000Z","created_at_i":1788549734,"id":49569038,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"LLMs are pretty good at slogging through. \nWhen will they come up with brilliant breakthroughs like Andrew Wiles?","title":null,"type":"comment","url":null},{"author":"estetlinus","children":[{"author":"aidos","children":[{"author":"FergusArgyll","children":[],"created_at":"2026-09-04T20:14:53.000Z","created_at_i":1788552893,"id":49569685,"options":[],"parent_id":49569631,"points":null,"story_id":49568506,"text":"Ooh I never realized FLT and Code book were the same author. Yes, both great!","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:10:22.000Z","created_at_i":1788552622,"id":49569631,"options":[],"parent_id":49569067,"points":null,"story_id":49568506,"text":"Also recommend his other books!
Big Bang - history of the understanding of space and the universe
Code book - history of the maths of ciphers
Haven\u2019t read them for years but I\u2019ve been meaning to again","title":null,"type":"comment","url":null},{"author":"kzrdude","children":[],"created_at":"2026-09-04T20:39:45.000Z","created_at_i":1788554385,"id":49569951,"options":[],"parent_id":49569067,"points":null,"story_id":49568506,"text":"And the multiple Numberphile appearances of Ken Ribet are interesting too! He is incredibly well spoken.
- https://www.youtube.com/watch?v=nUN4NDVIfVI (The bridges to Fermat's Last Theorem)
- https://www.youtube.com/watch?v=NPOw4iIxN6o (podcast)","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:24:25.000Z","created_at_i":1788549865,"id":49569067,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It\u2019s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.","title":null,"type":"comment","url":null},{"author":"KaiserPister","children":[{"author":"tossandthrow","children":[{"author":"Jaxan","children":[{"author":"tossandthrow","children":[],"created_at":"2026-09-04T19:44:25.000Z","created_at_i":1788551065,"id":49569321,"options":[],"parent_id":49569291,"points":null,"story_id":49568506,"text":"You need to understand the concept of the core algebra and 100s (with the s), then I think you'd be better positioned to understand my comment.
And granted, I don't know the exact details about Lean. It might be that they don't have an incredibly simple core - as has elsewise been the norm.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:41:57.000Z","created_at_i":1788550917,"id":49569291,"options":[],"parent_id":49569257,"points":null,"story_id":49568506,"text":"Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)","title":null,"type":"comment","url":null},{"author":"Jblx2","children":[],"created_at":"2026-09-04T20:15:26.000Z","created_at_i":1788552926,"id":49569693,"options":[],"parent_id":49569257,"points":null,"story_id":49568506,"text":"the Nanoda type-checker for Lean is ~5,000 lines of Rust:
https://leodemoura.github.io/blog/2026-3-16-who-watches-the-...
...and for those who are looking to roll-their-own:
https://ammkrn.github.io/type_checking_in_lean4/title_page.h...
...and some thoughts on putting stuff in the kernel:
https://lawrencecpaulson.github.io/2026/07/30/Collatz.html","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:39:49.000Z","created_at_i":1788550789,"id":49569257,"options":[],"parent_id":49569073,"points":null,"story_id":49568506,"text":"The proof system is relatively easy to verify.
I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code.
You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.","title":null,"type":"comment","url":null},{"author":"holmesworcester","children":[],"created_at":"2026-09-04T19:39:56.000Z","created_at_i":1788550796,"id":49569258,"options":[],"parent_id":49569073,"points":null,"story_id":49568506,"text":"Nope! :(
Meaning, people and LLMs are finding 1=0 bugs in formal verification tools. I have no idea how likely this is in this case, though!","title":null,"type":"comment","url":null},{"author":"Jaxan","children":[],"created_at":"2026-09-04T19:40:27.000Z","created_at_i":1788550827,"id":49569268,"options":[],"parent_id":49569073,"points":null,"story_id":49568506,"text":"This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.
We simply don\u2019t know what those 13M contain and whether it \u201cmakes sense\u201d and doesn\u2019t trigger Lean bugs. (There are \u201cindependent\u201d lean verifiers, but historically they contained the same, or similar, bugs.)","title":null,"type":"comment","url":null},{"author":"kingstnap","children":[{"author":"xvilka","children":[],"created_at":"2026-09-05T14:42:29.000Z","created_at_i":1788619349,"id":49577001,"options":[],"parent_id":49569324,"points":null,"story_id":49568506,"text":"Some argue that Lean breaks a few type-theoretical properties. See full discussion here:
https://github.com/rocq-prover/rocq/issues/10871","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:44:40.000Z","created_at_i":1788551080,"id":49569324,"options":[],"parent_id":49569073,"points":null,"story_id":49568506,"text":"The AI labs have out considerable effort in trying to find and patch lean exploits. They explicitly set agents and have them try to prove false.
> Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime
https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
They found several bugs and they have patched them. Lots of work going into making sure lean is sound.","title":null,"type":"comment","url":null},{"author":"andriy_koval","children":[{"author":"ajs1998","children":[{"author":"andriy_koval","children":[{"author":"drdeca","children":[{"author":"andriy_koval","children":[{"author":"drdeca","children":[{"author":"andriy_koval","children":[],"created_at":"2026-09-05T20:25:57.000Z","created_at_i":1788639957,"id":49580328,"options":[],"parent_id":49580297,"points":null,"story_id":49568506,"text":"and what is that system?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T20:20:48.000Z","created_at_i":1788639648,"id":49580297,"options":[],"parent_id":49572048,"points":null,"story_id":49568506,"text":"No, it is the same inference system. They are just abbreviations.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T01:05:11.000Z","created_at_i":1788570311,"id":49572048,"options":[],"parent_id":49571994,"points":null,"story_id":49568506,"text":"ok, you now added some unknown inference system in addition to zfc","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T00:56:42.000Z","created_at_i":1788569802,"id":49571994,"options":[],"parent_id":49570574,"points":null,"story_id":49568506,"text":"Within a given inference system, one can define concepts. This doesn\u2019t add any axioms. It is, in essence, just a way to abbreviate things.","title":null,"type":"comment","url":null},{"author":"Smaug123","children":[],"created_at":"2026-09-05T08:49:17.000Z","created_at_i":1788598157,"id":49574592,"options":[],"parent_id":49570574,"points":null,"story_id":49568506,"text":"Claude\u2019s formalisation, being in Lean, is based on the calculus of inductive constructions, not ZFC. In Lean 3, per Carneiro, any theorem of Lean 3\u2019s theory can be proved in ZFC plus some finite number of inaccessible cardinals (and, IIRC, vice versa). The precise strength of Lean 4 is not quite clear yet, I think (I guess this is partly what Lean4Lean is hoping to address).","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:42:36.000Z","created_at_i":1788558156,"id":49570574,"options":[],"parent_id":49569950,"points":null,"story_id":49568506,"text":"do we know if claude's formalization is built on top of zfc and not zfc+extra?
zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.","title":null,"type":"comment","url":null},{"author":"lanstin","children":[{"author":"mietek","children":[],"created_at":"2026-09-04T23:36:36.000Z","created_at_i":1788564996,"id":49571456,"options":[],"parent_id":49570967,"points":null,"story_id":49568506,"text":"Roughly, yes. See B. Werner (1997) \u201cSets in types, types in sets\u201d.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:26:52.000Z","created_at_i":1788560812,"id":49570967,"options":[],"parent_id":49569950,"points":null,"story_id":49568506,"text":"Reply to sibling - lean4 doesn't rest on ZF or ZFC. https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Co... However I believe an equivalence of power has been shown between the two.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:39:31.000Z","created_at_i":1788554371,"id":49569950,"options":[],"parent_id":49569430,"points":null,"story_id":49568506,"text":"ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.","title":null,"type":"comment","url":null},{"author":"deepsun","children":[{"author":"andriy_koval","children":[{"author":"Almondsetat","children":[{"author":"andriy_koval","children":[{"author":"Almondsetat","children":[{"author":"andriy_koval","children":[{"author":"Almondsetat","children":[{"author":"andriy_koval","children":[{"author":"Almondsetat","children":[{"author":"andriy_koval","children":[{"author":"Almondsetat","children":[{"author":"andriy_koval","children":[{"author":"Smaug123","children":[{"author":"andriy_koval","children":[{"author":"Smaug123","children":[{"author":"andriy_koval","children":[],"created_at":"2026-09-05T16:58:33.000Z","created_at_i":1788627513,"id":49578406,"options":[],"parent_id":49578344,"points":null,"story_id":49568506,"text":"I referred to specific definition in wikipedia. \nYour "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T16:50:59.000Z","created_at_i":1788627059,"id":49578344,"options":[],"parent_id":49577821,"points":null,"story_id":49568506,"text":"Because you wrote:
> what are exactly rules, which could be separate topic of research, this detail is skipped
I am now confident you\u2019re a troll, though, so I am going to bow out.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T16:01:16.000Z","created_at_i":1788624076,"id":49577821,"options":[],"parent_id":49574447,"points":null,"story_id":49568506,"text":"> Honestly I\u2019m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
I am aware, also I am not sure why you wrote all of this. Your unknown to me "first course" claims to be some authority of formalization purity?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T08:33:15.000Z","created_at_i":1788597195,"id":49574447,"options":[],"parent_id":49571407,"points":null,"story_id":49568506,"text":"Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I\u2019m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:30:48.000Z","created_at_i":1788564648,"id":49571407,"options":[],"parent_id":49571323,"points":null,"story_id":49568506,"text":"coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants.
I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. \nFormal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another.
ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it.\nAdditionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:18:24.000Z","created_at_i":1788563904,"id":49571323,"options":[],"parent_id":49571155,"points":null,"story_id":49568506,"text":"and you are entitled to talk about maths while rejecting maths","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:55:02.000Z","created_at_i":1788562502,"id":49571155,"options":[],"parent_id":49571127,"points":null,"story_id":49568506,"text":"you are entitled to have your opinion :-)","title":null,"type":"comment","url":null},{"author":"cdelsolar","children":[],"created_at":"2026-09-05T04:26:01.000Z","created_at_i":1788582361,"id":49573063,"options":[],"parent_id":49571127,"points":null,"story_id":49568506,"text":"What are you nerds fighting about please explain","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:51:43.000Z","created_at_i":1788562303,"id":49571127,"options":[],"parent_id":49570984,"points":null,"story_id":49568506,"text":"A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong","title":null,"type":"comment","url":null},{"author":"jibal","children":[{"author":"andriy_koval","children":[],"created_at":"2026-09-05T01:01:34.000Z","created_at_i":1788570094,"id":49572022,"options":[],"parent_id":49571669,"points":null,"story_id":49568506,"text":"imo, those two links are example of rather low quality weird math discussions, but you can keep your opinion","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T00:09:33.000Z","created_at_i":1788566973,"id":49571669,"options":[],"parent_id":49570984,"points":null,"story_id":49568506,"text":"That increases the likelihood that they are right.
> support your point with explanation or be ignored :-)
Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.
https://math.stackexchange.com/questions/1366560/why-does-g%...
https://math.stackexchange.com/questions/1090437/how-to-prov...","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:29:01.000Z","created_at_i":1788560941,"id":49570984,"options":[],"parent_id":49570908,"points":null,"story_id":49568506,"text":"looks like we are in disagreement","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:20:34.000Z","created_at_i":1788560434,"id":49570908,"options":[],"parent_id":49570878,"points":null,"story_id":49568506,"text":"why should they be obvious? they are derived and have been thoroughly proven.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:15:56.000Z","created_at_i":1788560156,"id":49570878,"options":[],"parent_id":49570816,"points":null,"story_id":49568506,"text":"> expressive enough to produce
you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:09:13.000Z","created_at_i":1788559753,"id":49570816,"options":[],"parent_id":49570786,"points":null,"story_id":49568506,"text":"Godel proved that any system expressive enough to produce an arithmetic is incomplete. He initially proved it for the peano axioms but then it got generalized. ZFC can produce an arithmetic. Also, before being arrogant and demanding explanations, you should give them first for your claims","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:04:52.000Z","created_at_i":1788559492,"id":49570786,"options":[],"parent_id":49570770,"points":null,"story_id":49568506,"text":"support your point with explanation or be ignored :-)","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:03:14.000Z","created_at_i":1788559394,"id":49570770,"options":[],"parent_id":49570679,"points":null,"story_id":49568506,"text":"If you start with "I'm not a strong expert" maybe you should stop continuing saying wrong stuff. What you just wrote is completely wrong.","title":null,"type":"comment","url":null},{"author":"IsTom","children":[{"author":"andriy_koval","children":[{"author":"IsTom","children":[{"author":"andriy_koval","children":[{"author":"IsTom","children":[{"author":"andriy_koval","children":[],"created_at":"2026-09-05T17:02:29.000Z","created_at_i":1788627749,"id":49578431,"options":[],"parent_id":49578377,"points":null,"story_id":49568506,"text":"No, once you start formalize this, it becomes complicated. There is a reason why looks like there is no "peano can be derived from zfc" theorem which would close dispute, and my opponents need to throw links on bro math from stackexchange in this discussion.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T16:55:35.000Z","created_at_i":1788627335,"id":49578377,"options":[],"parent_id":49577876,"points":null,"story_id":49568506,"text":"You make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T16:05:52.000Z","created_at_i":1788624352,"id":49577876,"options":[],"parent_id":49574492,"points":null,"story_id":49568506,"text":"> you just build some sets to represent numbers and make operations that act the same way as arithmetic
which is already "just" some non trivial problem(there is no "operations" in set theory), and we are discussing if it is achievable.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T08:37:47.000Z","created_at_i":1788597467,"id":49574492,"options":[],"parent_id":49570972,"points":null,"story_id":49568506,"text":"It's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given.
You don't need to add any axioms, you just build some sets to represent numbers and make operations that act the same way as arithmetic, define some equality relations. Then you derive rules of arithmetic for your handcrafted arithmetic using ZF axioms and you're good. You get axioms of arithmetic derived from your regular axioms without adding them as new axioms to your theory.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:27:48.000Z","created_at_i":1788560868,"id":49570972,"options":[],"parent_id":49570855,"points":null,"story_id":49568506,"text":"> interpreted
its hard to me to tell what this means formally(as I said I am not expert).\nThere is no "interpret" operator in zfc.\nI believe what it says if you add some robinson axioms + some logical rules on top of zfc, you can carry your results.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:12:57.000Z","created_at_i":1788559977,"id":49570855,"options":[],"parent_id":49570679,"points":null,"story_id":49568506,"text":"> Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC.
https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...","title":null,"type":"comment","url":null},{"author":"jibal","children":[],"created_at":"2026-09-05T00:01:46.000Z","created_at_i":1788566506,"id":49571618,"options":[],"parent_id":49570679,"points":null,"story_id":49568506,"text":"That is wildly wrong.","title":null,"type":"comment","url":null},{"author":"drdeca","children":[{"author":"andriy_koval","children":[{"author":"Smaug123","children":[{"author":"andriy_koval","children":[{"author":"Smaug123","children":[{"author":"andriy_koval","children":[],"created_at":"2026-09-05T16:55:54.000Z","created_at_i":1788627354,"id":49578382,"options":[],"parent_id":49578316,"points":null,"story_id":49568506,"text":"Your third year notes from Cambridge has very low authority to me","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T16:48:42.000Z","created_at_i":1788626922,"id":49578316,"options":[],"parent_id":49577831,"points":null,"story_id":49568506,"text":"As I have said a few times now, you should read any first course in set theory. I\u2019m quoting my third-year notes from Cambridge there, but essentially every intro to set theory will say the same. (I\u2019m sure someone will find a single counterexample that does it somehow differently.)","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T16:02:17.000Z","created_at_i":1788624137,"id":49577831,"options":[],"parent_id":49574473,"points":null,"story_id":49568506,"text":"> According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element.
Can you cite where did you get this?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T08:35:44.000Z","created_at_i":1788597344,"id":49574473,"options":[],"parent_id":49572042,"points":null,"story_id":49568506,"text":"It simply does have functions. According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element.
I mean this quite seriously: have you considered reading any first course in set theory?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T01:04:02.000Z","created_at_i":1788570242,"id":49572042,"options":[],"parent_id":49571975,"points":null,"story_id":49568506,"text":"zfc doesn't have functions, so you are building something new on top of it.
Also, I am not sure successor function is enough for PA.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T00:54:19.000Z","created_at_i":1788569659,"id":49571975,"options":[],"parent_id":49570679,"points":null,"story_id":49568506,"text":"ZFC has greater consistency strength than PA.
If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:53:17.000Z","created_at_i":1788558797,"id":49570679,"options":[],"parent_id":49570573,"points":null,"story_id":49568506,"text":"> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.","title":null,"type":"comment","url":null},{"author":"SP3269","children":[],"created_at":"2026-09-04T22:54:14.000Z","created_at_i":1788562454,"id":49571151,"options":[],"parent_id":49570573,"points":null,"story_id":49568506,"text":"Interestingly, in his ICM 2026 lecture, Terence Tao specifically mentioned that Lean is not based on ZFC.","title":null,"type":"comment","url":null},{"author":"deterministic","children":[],"created_at":"2026-09-05T02:16:34.000Z","created_at_i":1788574594,"id":49572450,"options":[],"parent_id":49570573,"points":null,"story_id":49568506,"text":"Lean is based on Type Theory not ZFC.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:42:34.000Z","created_at_i":1788558154,"id":49570573,"options":[],"parent_id":49569430,"points":null,"story_id":49568506,"text":"There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless.
You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
It would be fun to play with this Anthropic/Lean formalization under different axiomatics.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:54:38.000Z","created_at_i":1788551678,"id":49569430,"options":[],"parent_id":49569073,"points":null,"story_id":49568506,"text":"Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.","title":null,"type":"comment","url":null},{"author":"Smaug123","children":[{"author":"jmusall","children":[{"author":"derkha","children":[],"created_at":"2026-09-05T08:23:02.000Z","created_at_i":1788596582,"id":49574371,"options":[],"parent_id":49570551,"points":null,"story_id":49568506,"text":"No, comparator does check the entire closure","title":null,"type":"comment","url":null},{"author":"Smaug123","children":[],"created_at":"2026-09-05T08:26:04.000Z","created_at_i":1788596764,"id":49574394,"options":[],"parent_id":49570551,"points":null,"story_id":49568506,"text":"I think this isn\u2019t true? Comparator verifies proofs; it\u2019s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it\u2019s hard to find much simpler statements of maths, slightly odd facts of mathlib\u2019s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:39:49.000Z","created_at_i":1788557989,"id":49570551,"options":[],"parent_id":49569624,"points":null,"story_id":49568506,"text":"The comparator was only used to verify that the final statement indeed is a valid formalization of Fermat's Last Theorem, not that the proof leading up to it is correct.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:09:29.000Z","created_at_i":1788552569,"id":49569624,"options":[],"parent_id":49569073,"points":null,"story_id":49568506,"text":"It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.","title":null,"type":"comment","url":null},{"author":"dist-epoch","children":[],"created_at":"2026-09-04T20:38:33.000Z","created_at_i":1788554313,"id":49569942,"options":[],"parent_id":49569073,"points":null,"story_id":49568506,"text":"Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.","title":null,"type":"comment","url":null},{"author":"jmusall","children":[{"author":"qbit42","children":[],"created_at":"2026-09-05T10:55:30.000Z","created_at_i":1788605730,"id":49575289,"options":[],"parent_id":49570642,"points":null,"story_id":49568506,"text":"You just have to trust the statement and the lean compiler, not the proof. The compiler certainly still has remaining bugs, but I have never seen a bug leading to a false proof in good faith, only via obscure meta programming tricks. The nice thing is that the multiple versions of the compiler are constantly being stress tested. Still, there is plenty of work that could be done to make the compiler more trustworthy / easier to verify.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:49:32.000Z","created_at_i":1788558572,"id":49570642,"options":[],"parent_id":49569073,"points":null,"story_id":49568506,"text":"That must have slipped through Kevin Buzzard's review, which is not entirely unplausible with 29500 theorems to verify...
I think they should spend another few billion tokens and let agents try to disprove any of those statements or links between them. Then I'd be a lot more convinced.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:25:02.000Z","created_at_i":1788549902,"id":49569073,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?","title":null,"type":"comment","url":null},{"author":"kzrdude","children":[{"author":"simpaticoder","children":[],"created_at":"2026-09-04T19:42:39.000Z","created_at_i":1788550959,"id":49569299,"options":[],"parent_id":49569076,"points":null,"story_id":49568506,"text":"This stuck out to me, too. That a (presumably rather simple) coworking tool was instrumental in shaping the vast (6B token!) output is eye-opening. We have this vast power but without intermediate structure it is wasted. Much like Turing machines themselves, which are shaped by language design to get somewhere at the expense of getting everywhere.","title":null,"type":"comment","url":null},{"author":"marwahaha","children":[],"created_at":"2026-09-05T08:36:28.000Z","created_at_i":1788597388,"id":49574480,"options":[],"parent_id":49569076,"points":null,"story_id":49568506,"text":"I helped build https://prove2.me . It's not proof-specific but everything is Lean-based. I've found the tool useful when formalizing recent upper bounds on $\\omega$ (in computational complexity of matrix multiplication). A lot of ideas in this tool are experimental, but the intent is to benefit the mathematical community at large. I'd be happy to hear about any suggestions or advice others have.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:25:18.000Z","created_at_i":1788549918,"id":49569076,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"The part about prove2.me was interesting. That means that a co-working tool was instrumental in the project, and I think AI companies will take note of this. Is this proof specific or will we need to give agents access to JIRA or similar tools to solve large projects in the future?","title":null,"type":"comment","url":null},{"author":"refibrillator","children":[{"author":"bawolff","children":[],"created_at":"2026-09-04T19:29:20.000Z","created_at_i":1788550160,"id":49569119,"options":[],"parent_id":49569100,"points":null,"story_id":49568506,"text":"Formalizing is not the same as discovering. There is still plenty of room for human ingenuity.","title":null,"type":"comment","url":null},{"author":"mannanj","children":[],"created_at":"2026-09-04T19:29:59.000Z","created_at_i":1788550199,"id":49569131,"options":[],"parent_id":49569100,"points":null,"story_id":49568506,"text":"Makes me wonder, if we make a tradeoff for comfort and advancement from our biology's "limits" - and that tradeoff is spiritual fulfillment.
Seeing it hit across: the work we used to do outdoors, the sleep-wake-dark cycle we adhered to for millennia, and more","title":null,"type":"comment","url":null},{"author":"ben_w","children":[{"author":"Jtarii","children":[{"author":"willmarch","children":[],"created_at":"2026-09-05T00:02:42.000Z","created_at_i":1788566562,"id":49571624,"options":[],"parent_id":49569394,"points":null,"story_id":49568506,"text":"Why?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:51:51.000Z","created_at_i":1788551511,"id":49569394,"options":[],"parent_id":49569204,"points":null,"story_id":49568506,"text":"If the Riemann hypothesis is solved primarily by a AI system it will not be as awe inspiring as if a human solved it.
That is just how it is.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:35:02.000Z","created_at_i":1788550502,"id":49569204,"options":[],"parent_id":49569100,"points":null,"story_id":49568506,"text":"> It is truly saddening to think that machines will deprive us of this wonder and experience.
It won't deprive us.
Recent video I've watched from Brandon Sanderson, IMO also applies to all the things we love and not just art:
https://youtu.be/mb3uK-_QkOo?si=SG1uvGUbN6SOYI_J","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:27:46.000Z","created_at_i":1788550066,"id":49569100,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Proving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye:
https://news.ycombinator.com/item?id=49203626
It is truly saddening to think that machines will deprive us of this wonder and experience.
But truly exciting to dream about what lies beyond the limits of our biology.","title":null,"type":"comment","url":null},{"author":"stabbles","children":[{"author":"raverbashing","children":[],"created_at":"2026-09-04T19:37:23.000Z","created_at_i":1788550643,"id":49569227,"options":[],"parent_id":49569134,"points":null,"story_id":49568506,"text":"Yes. FLT follows from the fact that you can't build the equivalent representation of n-simplex turning into a hypercube in dimensions higher than 2
/s","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:30:17.000Z","created_at_i":1788550217,"id":49569134,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Now /simplify. Can it be half the size? Will someone at some point prove that the proof cannot be simplified further?","title":null,"type":"comment","url":null},{"author":"prometheus1992","children":[{"author":"hyperhello","children":[{"author":"epgui","children":[{"author":"hyperhello","children":[],"created_at":"2026-09-04T19:42:47.000Z","created_at_i":1788550967,"id":49569301,"options":[],"parent_id":49569251,"points":null,"story_id":49568506,"text":"Well, there\u2019s actually a very small set of operations that allow all computation, so it doesn\u2019t take much to be a DSL and a GP too; I\u2019d be surprised if a proof language couldn\u2019t swing it.","title":null,"type":"comment","url":null},{"author":"mswphd","children":[],"created_at":"2026-09-04T21:43:46.000Z","created_at_i":1788558226,"id":49570585,"options":[],"parent_id":49569251,"points":null,"story_id":49568506,"text":"it is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:39:17.000Z","created_at_i":1788550757,"id":49569251,"options":[],"parent_id":49569194,"points":null,"story_id":49568506,"text":"Is Lean a DSL? I\u2019d argue it\u2019s a general purpose programming language that excels at proofs.","title":null,"type":"comment","url":null},{"author":"stratos123","children":[{"author":"hyperhello","children":[{"author":"fn-mote","children":[],"created_at":"2026-09-04T20:51:32.000Z","created_at_i":1788555092,"id":49570062,"options":[],"parent_id":49569403,"points":null,"story_id":49568506,"text":"This would be funny if it were relevant. Seems like a statement about false negatives instead of false positives.
False negative = could not find a proof of a true theorem.
False positive = erroneous proof of a theorem.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:52:53.000Z","created_at_i":1788551573,"id":49569403,"options":[],"parent_id":49569298,"points":null,"story_id":49568506,"text":"Isn\u2019t there some theorem that any sufficiently complex mathematical languages will have statements that can\u2019t be proven? :)","title":null,"type":"comment","url":null},{"author":"mswphd","children":[],"created_at":"2026-09-04T21:39:15.000Z","created_at_i":1788557955,"id":49570543,"options":[],"parent_id":49569298,"points":null,"story_id":49568506,"text":"junk theorems aren't the concern, soundness issues in the lean kernel are the concern.
Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful.
As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals
https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...
Then for any natural numbers n, m, they're implicitly sets. So n \\intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".","title":null,"type":"comment","url":null},{"author":"ndriscoll","children":[],"created_at":"2026-09-04T22:18:01.000Z","created_at_i":1788560281,"id":49570889,"options":[],"parent_id":49569298,"points":null,"story_id":49568506,"text":"This has nothing to do with Lean, e.g.
> The first coordinate of the polynomial X^2 (X^3 + X + 1 ) is equal to the prime factorization of 30 .
We defined polynomials as their coefficient functions in my algebra class, and it makes sense that you'd define a prime factorization as a function from primes to N, which naturally extends to a function N->N. So this junk theorem is part of normal math too. It just says in an obtuse way that they're both the function that's 1 at 2, 3, and 5, and 0 elsewhere.","title":null,"type":"comment","url":null},{"author":"kzrdude","children":[{"author":"ndriscoll","children":[],"created_at":"2026-09-05T15:23:56.000Z","created_at_i":1788621836,"id":49577438,"options":[],"parent_id":49576260,"points":null,"story_id":49568506,"text":"As with many programming languages, you can use phantom types to prevent this sort of thing, and in fact, that's exactly what's happening but they make it sound extra silly when they throw away the safety wrapper. That's why some of these have weird statements like the third coordinate of <something that doesn't obviously have coordinates>. Some of these amount to, "if you have 3 apples and 5 oranges, and you just take the raw numbers and add them, you get 8," and then layer it with an extra level of obfuscation, like "if you have the second prime number apples, and the third prime number oranges, and take the raw numbers and add them, you get the first prime number to the power of the second prime number."","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T13:19:51.000Z","created_at_i":1788614391,"id":49576260,"options":[],"parent_id":49569298,"points":null,"story_id":49568506,"text":"Some kind of linter should flag these with a warning, I think","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:42:39.000Z","created_at_i":1788550959,"id":49569298,"options":[],"parent_id":49569194,"points":null,"story_id":49568506,"text":"
encode mathematical reasoning in a way that can\u2019t be fooled.Note to other users: don\u2019t downvote this kind of comment, answer it.","title":null,"type":"comment","url":null},{"author":"fwip","children":[],"created_at":"2026-09-04T19:34:45.000Z","created_at_i":1788550485,"id":49569200,"options":[],"parent_id":49569170,"points":null,"story_id":49568506,"text":"The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.","title":null,"type":"comment","url":null},{"author":"babelfish","children":[{"author":"bobmarleybiceps","children":[{"author":"CaptWorld","children":[{"author":"mswphd","children":[{"author":"CaptWorld","children":[{"author":"mswphd","children":[{"author":"CaptWorld","children":[],"created_at":"2026-09-05T07:37:30.000Z","created_at_i":1788593850,"id":49574090,"options":[],"parent_id":49571107,"points":null,"story_id":49568506,"text":"Of course, there's a possibility but it exists everywhere but there's no sign till now that it has. Same with openai's proofs.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:48:30.000Z","created_at_i":1788562110,"id":49571107,"options":[],"parent_id":49570807,"points":null,"story_id":49568506,"text":"I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.","title":null,"type":"comment","url":null},{"author":"Jblx2","children":[{"author":"CaptWorld","children":[],"created_at":"2026-09-05T07:38:50.000Z","created_at_i":1788593930,"id":49574096,"options":[],"parent_id":49571984,"points":null,"story_id":49568506,"text":"Sure. But experts seem to be aware of the direction of those solutions so it seems unlikely there could be some hidden bug which disproves it. But it could be possible.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T00:55:12.000Z","created_at_i":1788569712,"id":49571984,"options":[],"parent_id":49570807,"points":null,"story_id":49568506,"text":"How about all of these bugs from last week?
https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:07:47.000Z","created_at_i":1788559667,"id":49570807,"options":[],"parent_id":49570670,"points":null,"story_id":49568506,"text":"Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:52:04.000Z","created_at_i":1788558724,"id":49570670,"options":[],"parent_id":49570393,"points":null,"story_id":49568506,"text":"as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:23:47.000Z","created_at_i":1788557027,"id":49570393,"options":[],"parent_id":49569635,"points":null,"story_id":49568506,"text":"Do you have proof of this bug or something? Is this just envy against computers now ?","title":null,"type":"comment","url":null},{"author":"tatjam","children":[],"created_at":"2026-09-04T22:08:48.000Z","created_at_i":1788559728,"id":49570812,"options":[],"parent_id":49569635,"points":null,"story_id":49568506,"text":"Well considering the proof is pretty much accepted by mathematicians to be correct (I'll be happy with that!), it would be sort of unnecessary to cheat. Maybe if some aspect is really tricky to formalize it could have done something there? If I had to search for it, I would go for parts of the original proof that are "outsourced" to other mathematical works. \nImagine one of the agents struggling to download a paper due to a paywall or whatever and just deciding to cheat lol","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:10:34.000Z","created_at_i":1788552634,"id":49569635,"options":[],"parent_id":49569210,"points":null,"story_id":49568506,"text":"guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:35:41.000Z","created_at_i":1788550541,"id":49569210,"options":[],"parent_id":49569170,"points":null,"story_id":49568506,"text":"A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well","title":null,"type":"comment","url":null},{"author":"stabbles","children":[{"author":"Jblx2","children":[{"author":"vessenes","children":[],"created_at":"2026-09-04T20:50:24.000Z","created_at_i":1788555024,"id":49570056,"options":[],"parent_id":49569385,"points":null,"story_id":49568506,"text":"True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:50:28.000Z","created_at_i":1788551428,"id":49569385,"options":[],"parent_id":49569229,"points":null,"story_id":49568506,"text":"You still have to trust that the AI didn't exploit a bug in the Lean kernel. There was just such an instance of a bug a little over a month ago:
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:37:32.000Z","created_at_i":1788550652,"id":49569229,"options":[],"parent_id":49569170,"points":null,"story_id":49568506,"text":"There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough.
So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.","title":null,"type":"comment","url":null},{"author":"lordnacho","children":[],"created_at":"2026-09-04T19:38:57.000Z","created_at_i":1788550737,"id":49569249,"options":[],"parent_id":49569170,"points":null,"story_id":49568506,"text":"This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it.
But how do you know you told it what you intended to tell it?","title":null,"type":"comment","url":null},{"author":"tossandthrow","children":[],"created_at":"2026-09-04T19:41:15.000Z","created_at_i":1788550875,"id":49569281,"options":[],"parent_id":49569170,"points":null,"story_id":49568506,"text":"No. No human checked it. But a type checker did. And that is much better.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:32:50.000Z","created_at_i":1788550370,"id":49569170,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Can someone with more knowledge help me with this silly question in my head?
>>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems
Did a human check the 13 million lines of code? How does QA'ing this type of work works?","title":null,"type":"comment","url":null},{"author":"ex-aws-dude","children":[{"author":"QuesnayJr","children":[],"created_at":"2026-09-04T20:45:52.000Z","created_at_i":1788554752,"id":49570016,"options":[],"parent_id":49569173,"points":null,"story_id":49568506,"text":"Lean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:32:59.000Z","created_at_i":1788550379,"id":49569173,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"To ask a dumb question is there any chance there can be a bug in these generated proofs that makes it think its true?
Or is it the case that as long as you verify the initial statements you are trying to prove the rest doesn't matter","title":null,"type":"comment","url":null},{"author":"forkbomb123","children":[{"author":"hokkos","children":[],"created_at":"2026-09-04T20:11:00.000Z","created_at_i":1788552660,"id":49569638,"options":[],"parent_id":49569263,"points":null,"story_id":49568506,"text":"their reaction here :\nhttps://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:40:10.000Z","created_at_i":1788550810,"id":49569263,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I'm so curious what happens to this project that intended on proving FLT by 2029 now
the project: https://imperialcollegelondon.github.io/FLT/","title":null,"type":"comment","url":null},{"author":"dgellow","children":[],"created_at":"2026-09-04T19:40:52.000Z","created_at_i":1788550852,"id":49569273,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Lean continues to pay off. Such a beautiful project","title":null,"type":"comment","url":null},{"author":"davmre","children":[{"author":"3192987","children":[{"author":"logicprog","children":[{"author":"123aHgf","children":[],"created_at":"2026-09-05T13:09:58.000Z","created_at_i":1788613798,"id":49576188,"options":[],"parent_id":49571731,"points":null,"story_id":49568506,"text":"Wrong. AlphaProof is much older, used Lean and a tree search for tactics just like ACL2.
They all steal from ACL2 without attribution in the current publication boiler room atmosphere. They get away with it because the AI Cult has information and publication dominance.
There was a brief period that used only language for toy IMO problems, but for serious work like FLT they apparently reverted to established approaches.","title":null,"type":"comment","url":null},{"author":"porridgeraisin","children":[],"created_at":"2026-09-05T18:13:01.000Z","created_at_i":1788631981,"id":49579150,"options":[],"parent_id":49571731,"points":null,"story_id":49568506,"text":"Literally many previous instance used one. Right from alphaevolve onwards.
I'm not some "LLM is just a next token predictor guy" (GP seems to have a thing against LLMs), but to use LLMs properly you genuinely do need a grounded verifier and a planner. Coding harnesses for example are exactly that.
For some plans, you can AR generate the search tree and that's what subagents being planned around by high level (LLM)agents and such are. Coding agents even with subagents are imperfect even on verifiable tasks only because of that. If you can put a human to simply guide it, it becomes a full system. This is what we all do today whenever we use codex. It's not something that is "never done before".
I also don't subscribe to the purist view which is taken by GP. I prefer to think in terms of concentration inequalities. P(failure rate > r) < epsilon. You get different levels of autonomy for different values of r for the planner and verifier each. If you have a good planner and a good verifier, r is very very small and it's super useful. Autonomy at a given r comes from how much of the planner and how much of the verifier is automated at that r. All levels of autonomy are economically useful. Many values of r are economically useful.
In this case of FLT, the verification was entirely automated using lean, and it is correct upto lean compiler bugs (so a very small r). The planner was essentially a maintained graph (afaik. Prove2me doesn't use A* or any heuristic/evolutionary methods to limit or prune the frontier), AND importantly - I'm not seeing anyone on HN mention this - some human nudges, literally, which nodes to open.
The way to make AI systems more useful is to build great verifiers and great planners, which is what many companies and startups are doing. LLMs are already really really good proposers due to excellent generalization (to be pedantic, multiple stacked specialisations), especially MoE models, making them amenable to proposing at every point in a vast search tree without any adaptation.
Yes, it is possible to do complex tasks purely AR, so long as you can AR simulate the search, which in the case of LLMs corresponds to verbalising the search tree[4]. This is trivially true. Can this be useful? Yes. Can a millenium prize problem be solved purely AR? Sure. It's a hard problem for humans, there is no reason it has to be difficult to reach in the conditional distributions of every future LLM. In the trivial limit, an LLM trained on the solution 100% you can sample it out. An LLM 2 generations behind that may have it at p=0.001, entirely reachable given a planner, but probably not AR. An LLM 1 generation behind may have it at p=0.05, plausibly reachable purely AR.
But the key question is: is `r` smaller or larger if you have a planner versus not? The answer there is obvious. Second, if you have a threshold `r` that decides usefulness, is the set of things you can autonomously do under that threshold higher with planners and verifiers? Again the answer is an obvious yes.
Copy pasting code from chatgpt repeatedly is worse than using a coding harness where it gets grounded feedback, LLM weights kept constant. Keeping the history of things and the overall plan that worked fixed and isolating LLMs to do subtasks is better than developing a whole database in one continuous context. In some cases, the overall plan "tree" can itself be entirely verbalised, but most commonly there is human modifications/steering.
Can pure-LLM coding harnesses with just verifiers one shot most e commerce sites including planning? Yes. But we want to do more with it than e commerce sites. Will it keep improving thus enabling us to do more and more complex things? No obvious reason for a fixed limit to exist in theory[1]. But at any point on the progress curve, using it with a harness always gives better results versus not. Concretely, with fable 5.1, using it without a harness could not prove FLT in reasonable token budgets [3]. However, it is possible for say, idk, GPT9, trained on this, to verbalise this whole proof tree, and also potentially generalize it to another open problem, purely AR, in a reasonable token budget[2]. This was how we got from gsm8k to FLT in the first place.
It's not a binary "AR is useless" "AR is all you need".
[1] the limits are mostly economic, and time is itself a limit, see https://news.ycombinator.com/item?id=49161078\nTl;dr diminishing returns of test time scaling. Noam brown also has a piece about this.
[2] if it's too many tokens that we run out of time or money literally, that is the limit described in [1]. It is not linear or constant scaling necessarily as described again in [1].
[3] [2] is why we have to add token budgets as another axis apart from r and the autonomy level.
[4] And, the distribution conditioned on that verbalisation must be amenable to sampling the verbalisation of the execution of the plan from. This is not a given, see https://arxiv.org/abs/2504.09762 and https://news.ycombinator.com/item?id=49277303","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T00:18:37.000Z","created_at_i":1788567517,"id":49571731,"options":[],"parent_id":49569396,"points":null,"story_id":49568506,"text":"> A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.
Yeah, because before now there's been literally zero proof of an automated theorem prover scaffold around the LLMs being used, and big counterexamples and such being found, with raw chat logs available, where no such thing was used.
> Now they have it in writing.
Yeah, because now it's actually being done. They talk about it as a novel thing, because it is. You don't get to claim being "right all along" from this","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:51:58.000Z","created_at_i":1788551518,"id":49569396,"options":[],"parent_id":49569311,"points":null,"story_id":49568506,"text":"And human salaries for those who worked on the prover harness etc. which isn't just standard Fable.
It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.
Now they have it in writing.","title":null,"type":"comment","url":null},{"author":"jensgk","children":[{"author":"dist-epoch","children":[],"created_at":"2026-09-04T20:27:43.000Z","created_at_i":1788553663,"id":49569832,"options":[],"parent_id":49569416,"points":null,"story_id":49568506,"text":"More importantly how many years it would take.","title":null,"type":"comment","url":null},{"author":"nearbuy","children":[],"created_at":"2026-09-04T21:53:20.000Z","created_at_i":1788558800,"id":49570680,"options":[],"parent_id":49569416,"points":null,"story_id":49568506,"text":"The Kevin Buzzard post linked at the top says they budgeted \u00a31M over 5 years for a smaller proof.","title":null,"type":"comment","url":null},{"author":"margorczynski","children":[{"author":"jascination","children":[{"author":"emil-lp","children":[],"created_at":"2026-09-05T06:00:31.000Z","created_at_i":1788588031,"id":49573498,"options":[],"parent_id":49571348,"points":null,"story_id":49568506,"text":"You mean why not say \u00a3 1MM?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:22:39.000Z","created_at_i":1788564159,"id":49571348,"options":[],"parent_id":49571157,"points":null,"story_id":49568506,"text":"1kk? Why not say 1M?","title":null,"type":"comment","url":null},{"author":"traes","children":[],"created_at":"2026-09-05T00:17:11.000Z","created_at_i":1788567431,"id":49571721,"options":[],"parent_id":49571157,"points":null,"story_id":49568506,"text":"It's true that his goal was not the full thing, but it was also not merely a Lean verified proof. From the blog post linked in the toptext:
> The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean\u2019s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof.","title":null,"type":"comment","url":null},{"author":"VLM","children":[],"created_at":"2026-09-05T19:36:56.000Z","created_at_i":1788637016,"id":49579906,"options":[],"parent_id":49571157,"points":null,"story_id":49568506,"text":"Not a similar comparison in that one project was to produce a plan to extend the limits and goals of mathematics in general while in the process of answering "Is it true, circle yes or no". The other project circled "yes" but the output is not ... progress toward goals oriented.
Its like using AI to do your homework in the middle of a class. Yes, in the short term, that solves the problem of completing your homework. But it creates an entirely new problem of if you never did the homework how do you intend to pass the rest of the class or the remainder of college curriculum? A lot of cheaters ... don't.
A project has a long term path for permanent progress across an entire field. An oracle answers a question, sometimes cryptically, then progress in the field permanently ceases.
The value of a research project to determine if a Turing Machine halts with a T or a F on the tape is, to some extent, did it get a T or an F on the tape, but much more so the value is the tendrils of the rest of the field of mathematics pushing into the project at the start and then pushing out to enrich the rest of the field of mathematics at the end.
On the other hand if you have a project to run that Turing machine and see if it ever halts with a T or F as the proof, the result is completely sterile and WRT advancement of the rest of the field the actual result is kinda irrelevant. No postdoc is going to take the skills learned and move on to a position somewhere else and apply those new skills toward advancing something else in the field or describing a new goal or new way to look at the world. We'll get a popular science article about "oh it turns out the answer is indeed 'T'" and thats it. Sterile.
Personally I always thought the theorem proving turing machine would indeed terminate with a "T" and indeed it did. That's nice, and I bet the result settled a lot of bar bets. Aside from that, it will have minimal impact on progress in the field compared to the human project that's actually advancing the field.
Possibly people will be able to parse the 13 million lines of whatever into useful progress elsewhere in the field, possibly not. It'll be hard to get funding for it. OTOH its early days. Might end up useful in the end.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:55:12.000Z","created_at_i":1788562512,"id":49571157,"options":[],"parent_id":49569416,"points":null,"story_id":49568506,"text":"Buzzard was given 1kk GBP and 5 years and his goal I think wasn't the full thing like Anthropic did. So much more cash and orders of magnitude more time. The proof is about 5x the whole Mathlib library which was developed over many years by dozens of people.","title":null,"type":"comment","url":null},{"author":"well_ackshually","children":[],"created_at":"2026-09-05T11:45:39.000Z","created_at_i":1788608739,"id":49575631,"options":[],"parent_id":49569416,"points":null,"story_id":49568506,"text":"1 million dollars reinvested in the economy by a bunch of math nerds that need to buy food, get housing, pay for services, or 300k in Anthropic's pocket? I wonder which one makes society better off, hmmmm, very complicated question, nobody can answer that.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:53:31.000Z","created_at_i":1788551611,"id":49569416,"options":[],"parent_id":49569311,"points":null,"story_id":49568506,"text":"What would it cost to make a team of mathematicians do the same?","title":null,"type":"comment","url":null},{"author":"tonyarkles","children":[{"author":"wolttam","children":[],"created_at":"2026-09-04T20:15:20.000Z","created_at_i":1788552920,"id":49569692,"options":[],"parent_id":49569437,"points":null,"story_id":49568506,"text":"~10B tokens a month is pretty typical overall input/output usage from my own experience and other developer accounts I've seen","title":null,"type":"comment","url":null},{"author":"dist-epoch","children":[],"created_at":"2026-09-04T20:25:40.000Z","created_at_i":1788553540,"id":49569813,"options":[],"parent_id":49569437,"points":null,"story_id":49568506,"text":"When writing software with Codex 95+% of tokens are cache, I would assume the same in your case (if you also used it for coding).","title":null,"type":"comment","url":null},{"author":"fspeech","children":[],"created_at":"2026-09-04T20:38:49.000Z","created_at_i":1788554329,"id":49569944,"options":[],"parent_id":49569437,"points":null,"story_id":49568506,"text":"It's 6B output tokens, as stated by the blog post.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:55:08.000Z","created_at_i":1788551708,"id":49569437,"options":[],"parent_id":49569311,"points":null,"story_id":49568506,"text":"But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn\u2019t break down input vs. output tokens as far as I can tell.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:43:33.000Z","created_at_i":1788551013,"id":49569311,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"> a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1.
At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.","title":null,"type":"comment","url":null},{"author":"mhmdfromkarak","children":[],"created_at":"2026-09-04T19:45:38.000Z","created_at_i":1788551138,"id":49569339,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"that's crazy","title":null,"type":"comment","url":null},{"author":"chvid","children":[{"author":"alok-g","children":[{"author":"chvid","children":[{"author":"euroderf","children":[],"created_at":"2026-09-05T12:39:51.000Z","created_at_i":1788611991,"id":49575973,"options":[],"parent_id":49573320,"points":null,"story_id":49568506,"text":"Proving Riemann sure would clean up a lot of contingent/dependent number theory.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T05:23:00.000Z","created_at_i":1788585780,"id":49573320,"options":[],"parent_id":49571812,"points":null,"story_id":49568506,"text":"Who cares about some billionaire paying another billionaire a million dollars?
WHat matters is our understanding of maths, and whether this sort of thing makes us smarter or stupider.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T00:29:17.000Z","created_at_i":1788568157,"id":49571812,"options":[],"parent_id":49569442,"points":null,"story_id":49568506,"text":"If AI manages to prove, or disprove, I wonder what would Clay Foundation do for the prize.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:55:29.000Z","created_at_i":1788551729,"id":49569442,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Looking forward to the 5 billion LoC proof of the Riemann hypothesis.","title":null,"type":"comment","url":null},{"author":"ReptileMan","children":[{"author":"fn-mote","children":[],"created_at":"2026-09-04T20:54:39.000Z","created_at_i":1788555279,"id":49570082,"options":[],"parent_id":49569459,"points":null,"story_id":49568506,"text":"That's next week's work.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:57:02.000Z","created_at_i":1788551822,"id":49569459,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Why didn't you ran them to find simpler proof? This could also be big.","title":null,"type":"comment","url":null},{"author":"ojo-rojo","children":[{"author":"floweronthehill","children":[{"author":"ojo-rojo","children":[],"created_at":"2026-09-04T21:47:37.000Z","created_at_i":1788558457,"id":49570624,"options":[],"parent_id":49569851,"points":null,"story_id":49568506,"text":"Right. Once we see AI start delivering on the creative & intuition side of things that's going to be awesome. Until then I guess we'll live with exhaustive exploration of problem spaces by orchestrating swarms of agents...?","title":null,"type":"comment","url":null},{"author":"contubernio","children":[],"created_at":"2026-09-05T14:11:12.000Z","created_at_i":1788617472,"id":49576690,"options":[],"parent_id":49569851,"points":null,"story_id":49568506,"text":"It is capable of applying know heuristics and general principles in places where they haven't been applied and in this sense very much capable of generating conjectures in much the same way a person does. It's ability to employ a diversity of techniques coupled with it's computational power differentiate it from a human researcher. It still needs guidance to work well, but I've already changed my daily work flow as a research mathematician to incorporate use of AI.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:29:29.000Z","created_at_i":1788553769,"id":49569851,"options":[],"parent_id":49569460,"points":null,"story_id":49568506,"text":"I wonder if AI can come up with mathematical conjectures. As in, they feel it's right but can't prove it. What even happened in Fermat's brain to sense it was true?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T19:57:03.000Z","created_at_i":1788551823,"id":49569460,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I'm really impressed by mathematicians. It's cool that Fermat had the intuition to conjecture that "a\u207f + b\u207f = c\u207f" could not be satisfied for n > 2, and that other mathematicians can create proofs, and that others still can understand AI's formulation of those proofs. Really cool.","title":null,"type":"comment","url":null},{"author":"henryrobbins00","children":[],"created_at":"2026-09-04T20:07:56.000Z","created_at_i":1788552476,"id":49569603,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Back in February, I was talking with my PhD advisor about using Lean to formally verify automated optimization modeling outputs. It eventually turned into this paper [1]. It\u2019s been truly incredible to see how much the frontier models have progressed in both autoformalization and automated theorem proving in the last six months. Back in February, it was cool to see them prove the validity of some simple cutting planes. Now it can churn out a min-cut max-flow duality formalization (not to mention FLT). Very exciting times!
I\u2019ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2].
[1] https://arxiv.org/abs/2608.25220
[2] https://github.com/henryrobbins/open-atp","title":null,"type":"comment","url":null},{"author":"fspeech","children":[],"created_at":"2026-09-04T20:09:28.000Z","created_at_i":1788552568,"id":49569623,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"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.","title":null,"type":"comment","url":null},{"author":"chi_features","children":[{"author":"martinpw","children":[{"author":"AmazingEveryDay","children":[{"author":"tonyedgecombe","children":[],"created_at":"2026-09-05T07:44:04.000Z","created_at_i":1788594244,"id":49574124,"options":[],"parent_id":49570863,"points":null,"story_id":49568506,"text":"Also https://www.bbc.co.uk/iplayer/episode/b0074rxx/horizon-19951... (if you are in the UK).","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:13:23.000Z","created_at_i":1788560003,"id":49570863,"options":[],"parent_id":49570719,"points":null,"story_id":49568506,"text":"Also: https://archive.org/details/BBCHorizonCollection512Episodes/...","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:57:43.000Z","created_at_i":1788559063,"id":49570719,"options":[],"parent_id":49569653,"points":null,"story_id":49568506,"text":"Looks like it is available here:\nhttps://www.dailymotion.com/video/x3wrbsb","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:12:21.000Z","created_at_i":1788552741,"id":49569653,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"There's a wonderful documentary by BBC Horizon with Andrew Wiles from 1996 \u2013 highly recommend! I saw it in the 90's and it's a documentary for everyone. It captures the effort, struggle, highs and lows of a 7 year effort working on Fermat's Last Theorem.","title":null,"type":"comment","url":null},{"author":"catigula","children":[],"created_at":"2026-09-04T20:14:50.000Z","created_at_i":1788552890,"id":49569684,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"An AI safety company!","title":null,"type":"comment","url":null},{"author":"enriquto","children":[{"author":"QuesnayJr","children":[{"author":"tatjam","children":[{"author":"mswphd","children":[],"created_at":"2026-09-04T21:44:38.000Z","created_at_i":1788558278,"id":49570594,"options":[],"parent_id":49570560,"points":null,"story_id":49568506,"text":"note that this is exactly analogous to an LLM being able to slop code some demo, but not build something more generally useful/maintainable (say something suitable for inclusion in a standard library).","title":null,"type":"comment","url":null},{"author":"QuesnayJr","children":[],"created_at":"2026-09-05T03:52:24.000Z","created_at_i":1788580344,"id":49572929,"options":[],"parent_id":49570560,"points":null,"story_id":49568506,"text":"It wasn't clear that LLMs were up to a Lean translation task of this scale until now. The background required to formalize the FLT proof was tremendous, so many people assumed we would have to wait until all of that was formalized in Lean before we could ask it to formalize Wiles' proof. Now it seems like almost any mathematics paper we can ask an LLM to formalize, including all necessary background, and it can just do it.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:41:07.000Z","created_at_i":1788558067,"id":49570560,"options":[],"parent_id":49570003,"points":null,"story_id":49568506,"text":"I think there's a big misunderstanding going on here, translating the proof to Lean is, well... a translation task. Formalizing the proof in a way that's useful (breaks the proof down into relatively independent blocks that can be used for other maths and, importantly, understood individually) is a quite bigger, more creative endeavor. Not sure if LLMs would be able to do it, maybe yes?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:44:46.000Z","created_at_i":1788554686,"id":49570003,"options":[],"parent_id":49569690,"points":null,"story_id":49568506,"text":"Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.","title":null,"type":"comment","url":null},{"author":"ngruhn","children":[],"created_at":"2026-09-04T21:08:21.000Z","created_at_i":1788556101,"id":49570223,"options":[],"parent_id":49569690,"points":null,"story_id":49568506,"text":"Yes. The point was not coming up with the proof from scratch. The point was writing it all down in Lean to make it fully machine checkable.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:15:13.000Z","created_at_i":1788552913,"id":49569690,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"but i don't understand... isn't Wiles's proof and its numerous rewritings already in the training set?","title":null,"type":"comment","url":null},{"author":"crawshaw","children":[],"created_at":"2026-09-04T20:36:50.000Z","created_at_i":1788554210,"id":49569918,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"More (strong) evidence that agents make formal methods far more useful. The cost of creating that Lean proof has dropped dramatically.
Hopefully this helps mathematicians. It seems very clear to me that it will help software engineers apply formal methods to more of our software.","title":null,"type":"comment","url":null},{"author":"QuesnayJr","children":[{"author":"sanxiyn","children":[],"created_at":"2026-09-04T23:15:08.000Z","created_at_i":1788563708,"id":49571295,"options":[],"parent_id":49569931,"points":null,"story_id":49568506,"text":"New proof: The Classification of the Finite Simple Groups (American Mathematical Society Mathematical Surveys and Monographs vol. 40).
https://www.ams.org/publications/authors/books/postpub/surv-...
Number 1 (1994), Number 2 (1995), Number 3 (1997), Number 4 (1999), Number 5 (2002), Number 6 (2004), Number 7 (2018), Number 8 (2018), Number 9 (2021), Number 10 (2023). 10 volumes and >4000 pages so far, number 11 is in progress, and end is in sight, probably two more volumes or so.
https://www.ams.org/journals/notices/201806/rnoti-p646.pdf
People were curious what is going on during 2004-2018. A progress report was published in 2018 right before publication of number 7 and 8. In a sense it was the peak, number 8 completes the proof of so-called "generic case". The rest is "special case". It doesn't mean things get easier, but in some specific sense number 8 completed proof for almost all groups.
Now new proof's end is in sight, people are planning new new proof.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:37:43.000Z","created_at_i":1788554263,"id":49569931,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Holy shit. The proof of FLT is a giant detour through several different areas of mathematics, so formalizing it is a lot of work.
An interesting next target would be formalizing the classification of finite simple groups. The original proof scattered over thousands of pages of journal articles, plus Aschbacher and Smith's 1300 page 2 volume monograph. It's so long it's hard to know if there are any gaps. Researchers have been working on a streamlined new proof, but it's already many volumes long.","title":null,"type":"comment","url":null},{"author":"victor22","children":[{"author":"traes","children":[],"created_at":"2026-09-05T00:31:50.000Z","created_at_i":1788568310,"id":49571827,"options":[],"parent_id":49569962,"points":null,"story_id":49568506,"text":"The repo is public. You can just go look! It's really not that surprising; FLT is huge and has a ton of dependencies that need to be implemented, and there's a degree of sloppification that is probably blowing up the size by a few factors.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:40:24.000Z","created_at_i":1788554424,"id":49569962,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I call bullshit on 13 million lines makes no sense","title":null,"type":"comment","url":null},{"author":"vatsachak","children":[{"author":"The_Blade","children":[{"author":"vatsachak","children":[{"author":"whateveracct","children":[],"created_at":"2026-09-04T21:47:21.000Z","created_at_i":1788558441,"id":49570619,"options":[],"parent_id":49570163,"points":null,"story_id":49568506,"text":"my feel after a lot of experience with agentic haskell at scale has been...no they cannot and maybe the opposite lol","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:02:20.000Z","created_at_i":1788555740,"id":49570163,"options":[],"parent_id":49570136,"points":null,"story_id":49568506,"text":"I mean at this point there's no doubt that LLM cans be RL maxxed and give you _some working output_ but the next frontier is whether they can create good abstractions, a.k.a use the correct level of expressivity so as to not inline everything yet not play code golf.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:00:15.000Z","created_at_i":1788555615,"id":49570136,"options":[],"parent_id":49570068,"points":null,"story_id":49568506,"text":"physics is like sex: sure, it may give some practical results, but that's not why we do it","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:52:47.000Z","created_at_i":1788555167,"id":49570068,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"This is quite useless actually. The whole point of formalizing FLT was to clean up modern number theory into reusable abstractions that prove it.
If its 13 million LoC, it might involve so much spaghetti that its unusable other than the result","title":null,"type":"comment","url":null},{"author":"vagab0nd","children":[{"author":"qbane","children":[{"author":"JacobAsmuth","children":[],"created_at":"2026-09-05T06:09:27.000Z","created_at_i":1788588567,"id":49573551,"options":[],"parent_id":49570330,"points":null,"story_id":49568506,"text":"Except there's 10 trillion gears","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:16:24.000Z","created_at_i":1788556584,"id":49570330,"options":[],"parent_id":49570094,"points":null,"story_id":49568506,"text":"That is already the case for most neural networks and LLMs.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T20:55:32.000Z","created_at_i":1788555332,"id":49570094,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"> it wrote 13 million lines of Lean
Is this basically like opening up a black box and seeing 13 million gears all rotating seemingly randomly and still having no idea how the machine actually works?","title":null,"type":"comment","url":null},{"author":"richard_chase","children":[],"created_at":"2026-09-04T20:59:15.000Z","created_at_i":1788555555,"id":49570123,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Anyone know of a good Lean tutorial? I've played around with it a bit but never really learned it properly.","title":null,"type":"comment","url":null},{"author":"jjtheblunt","children":[],"created_at":"2026-09-04T21:24:16.000Z","created_at_i":1788557056,"id":49570395,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":">. Claude produced the first end-to-end, computer-checked proof of FLT. Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
I'm just old enough to remember Paul Erdo"s and his notion of 'The Book', which he defined to be a book the "Supreme Fascist" (God) had which held the most elegant proofs of mathematical theorems.
https://en.wikipedia.org/wiki/Paul_Erd\u0151s#Personal_life
It would be interesting to see how Erdo"s would name such a huge proof by Claude using Lean.","title":null,"type":"comment","url":null},{"author":"mnewme","children":[{"author":"sanxiyn","children":[],"created_at":"2026-09-04T22:55:03.000Z","created_at_i":1788562503,"id":49571156,"options":[],"parent_id":49570396,"points":null,"story_id":49568506,"text":"Yes, but Claude formalized a different proof than Buzzard is trying to, so it helps less than you think. (It certainly helps!)","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:24:19.000Z","created_at_i":1788557059,"id":49570396,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Do I miss something? But isnt there the whole code and paper of Kevin Buzzard in the training data of Claude?","title":null,"type":"comment","url":null},{"author":"EGreg","children":[{"author":"kzrdude","children":[],"created_at":"2026-09-04T22:11:20.000Z","created_at_i":1788559880,"id":49570837,"options":[],"parent_id":49570421,"points":null,"story_id":49568506,"text":"FLT was proven in 1995 by Andrew Wiles (with help of Richard Taylor).
This is not even a new proof, or at least they don't claim that it is. It's the formalization (in Lean) of an existing proof. That means, they are 'porting' the proof to a theorem proving programming language.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:26:44.000Z","created_at_i":1788557204,"id":49570421,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"So Fermat\u2019s Last Theorem has been proven a long time ago? By Andrew Wiles right? Is this like Appel and Haken >>> Seymour and Robin Thomas proof of 4CT?","title":null,"type":"comment","url":null},{"author":"threethirtytwo","children":[{"author":"Azantys","children":[{"author":"threethirtytwo","children":[],"created_at":"2026-09-05T00:00:43.000Z","created_at_i":1788566443,"id":49571610,"options":[],"parent_id":49571298,"points":null,"story_id":49568506,"text":"Then why is the guy not cleaning it up. Clearly he thinks it\u2019s done and he\u2019s moving on to do side things. He also explicitly said it went on to do more than what he was required to do.
Are you hallucinating? Because huge portion of what you wrote directly and logically contradicts the quotation I wrote.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:15:38.000Z","created_at_i":1788563738,"id":49571298,"options":[],"parent_id":49570442,"points":null,"story_id":49568506,"text":"The whole point was for the formalization to be clean enough so it could be reused in other parts of mathematics as I understand it. 13M lines of AI slop which have never been checked do not sound like what the original goal for such a formalization was. Also Claude didnt prove anything it just translated an already existing proof by Wiles into Lean, so it didn't actually contribute anything other than "Guys we did this thing, look how great our model is!". We never questioned that a printer can print faster than a human can write, but we dont let printers write novels.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:28:35.000Z","created_at_i":1788557315,"id":49570442,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":">The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean\u2019s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).
What is even the point? Have claude do it.
I'm not trying to be snarky here. I'm being serious. What is the point? This is an important question that needs to be answered. If something is definitively better, why not have that something take over?
I know people talk about the importance of human endeavor or the "joy" of doing something. But I don't care for those answers because it's weak. The question is deeper than this. AI is better than us, what is the logical point other than attempting to monopolize human effort even though it is inferior.","title":null,"type":"comment","url":null},{"author":"black_knight","children":[],"created_at":"2026-09-04T21:34:12.000Z","created_at_i":1788557652,"id":49570494,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the Lean libraries.
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!","title":null,"type":"comment","url":null},{"author":"mikmoila","children":[{"author":"behnamoh","children":[{"author":"deepsun","children":[{"author":"behnamoh","children":[],"created_at":"2026-09-04T21:47:54.000Z","created_at_i":1788558474,"id":49570627,"options":[],"parent_id":49570532,"points":null,"story_id":49568506,"text":"AI \u2260 crypto.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:38:24.000Z","created_at_i":1788557904,"id":49570532,"options":[],"parent_id":49570512,"points":null,"story_id":49568506,"text":"Same thing was said about cryptocurrency for like 15 years: "_in the future_ it will replace all fiat currency".","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:35:44.000Z","created_at_i":1788557744,"id":49570512,"options":[],"parent_id":49570495,"points":null,"story_id":49568506,"text":"For now. That, too, will change in the future.","title":null,"type":"comment","url":null},{"author":"educasean","children":[{"author":"mikmoila","children":[{"author":"johnsmith1840","children":[{"author":"mikmoila","children":[{"author":"Philpax","children":[{"author":"mikmoila","children":[{"author":"Philpax","children":[{"author":"mikmoila","children":[{"author":"johnsmith1840","children":[],"created_at":"2026-09-04T23:47:10.000Z","created_at_i":1788565630,"id":49571513,"options":[],"parent_id":49571317,"points":null,"story_id":49568506,"text":"100% not deterministic at the scale they run.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:17:47.000Z","created_at_i":1788563867,"id":49571317,"options":[],"parent_id":49571252,"points":null,"story_id":49568506,"text":"Yes "at any substancial level" . But still, its all about deterministic processes and still it obeys the law that the same input gives the same output. Or do you mean that the fluctuations like computing environment might ruin the determinism?","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:08:33.000Z","created_at_i":1788563313,"id":49571252,"options":[],"parent_id":49571203,"points":null,"story_id":49568506,"text":"No, I mean we just don't know what's going on in the circuits of the model at any substantial level. We set their architecture (hyperparameters), we pump them full of data (pretraining), and we shape how they behave through examples (SFT) and reward (RL), but we can't say with any certainty what the resulting model does internally.
You can scroll through https://transformer-circuits.pub/ to see the ~extent of our current understanding.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:02:42.000Z","created_at_i":1788562962,"id":49571203,"options":[],"parent_id":49571180,"points":null,"story_id":49568506,"text":"I think you're referring to the fact that the sheer amount of computations is something too time consuming for us to follow? But still it is not "magical" - in theory we could follow all the steps, there's no hidden information.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:58:12.000Z","created_at_i":1788562692,"id":49571180,"options":[],"parent_id":49571148,"points":null,"story_id":49568506,"text":"We don't know what they do. We shape them, but our understanding of how they get to their result is comparatively minimal.","title":null,"type":"comment","url":null},{"author":"johnsmith1840","children":[],"created_at":"2026-09-04T23:27:20.000Z","created_at_i":1788564440,"id":49571377,"options":[],"parent_id":49571148,"points":null,"story_id":49568506,"text":"Sure? I mean the internet is just a bunch of wires and some networking code not magic but at the same completely life alteringly magical.
My logic is that you personally could never have accomplished this feat with all the non LLM tools and content in the world. These kinds of things imply these methods are stepping beyond human ability.
Sure we put walls around it and optimize but the interior of that optimization is not something we understand.
You now have access to a system that for a price could solve something you simply are unable to solve. Not something we programmed it to solve, something that has never been solved before.
Nobody gave it an example of this proof, that's magical.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:54:07.000Z","created_at_i":1788562447,"id":49571148,"options":[],"parent_id":49570993,"points":null,"story_id":49568506,"text":""you could never have accomplished"; I am not able to follow the logic here - there is no "magic" in LLMs, they're built by humans and we know what they do.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:31:12.000Z","created_at_i":1788561072,"id":49570993,"options":[],"parent_id":49570826,"points":null,"story_id":49568506,"text":"A literal rock we carved patterns on and shot lightning into has accomplished something no human has.
How much more magical do you want this to be?
Tool or not it did something you could never have accomplished.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:10:23.000Z","created_at_i":1788559823,"id":49570826,"options":[],"parent_id":49570526,"points":null,"story_id":49568506,"text":"Humans built the tool which enabled the result. AI used the tooling for eliminating the dead ends. Yes, I can appreciate the practical value of all this, but IMHO it is not a kind of breakthrough result the article gives impression of.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:37:40.000Z","created_at_i":1788557860,"id":49570526,"options":[],"parent_id":49570495,"points":null,"story_id":49568506,"text":"By this standard, no computer has ever accomplished anything, because humans built the computer. AI bubble about to burst any second now.","title":null,"type":"comment","url":null},{"author":"logicprog","children":[],"created_at":"2026-09-05T00:23:57.000Z","created_at_i":1788567837,"id":49571774,"options":[],"parent_id":49570495,"points":null,"story_id":49568506,"text":"There's nothing about prove2me that couldn't have been coded just like any other huge coding project frontier models have proven themselves extremely good at doing. It just happened to have been made by humans.","title":null,"type":"comment","url":null},{"author":"marwahaha","children":[],"created_at":"2026-09-05T08:28:49.000Z","created_at_i":1788596929,"id":49574419,"options":[],"parent_id":49570495,"points":null,"story_id":49568506,"text":"I was involved in building https://prove2.me (but I am not affiliated with Anthropic nor involved in anything related to FLT). I think the key insight in prove2me is to prove theorems "top-down", which allows a large number of users to collaboratively work on a single theorem statement. This setup also seems to work well for a "swarm" of agents. I posted more of my thoughts on the Lean Zulip.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:34:18.000Z","created_at_i":1788557658,"id":49570495,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":""The effort succeeded when we switched to using Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University."
So in the end, it required tooling crafted by humans.","title":null,"type":"comment","url":null},{"author":"glimshe","children":[{"author":"jovas","children":[],"created_at":"2026-09-04T21:52:58.000Z","created_at_i":1788558778,"id":49570678,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"Yes, I'm a mathematician.
But not an expert on this.
While I don't know the specifics, and someone more "in-the-field" than me would recognize all the "named" theorems etc
I am aware that there have been minor issues that have come up with the formalization specifically, and that previous proofs for lower values of n were always needed.
Though it used to be n=5 and lower needed to be checked.","title":null,"type":"comment","url":null},{"author":"CogDisco","children":[],"created_at":"2026-09-04T21:56:36.000Z","created_at_i":1788558996,"id":49570710,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"Yep. While I'm not focussed on these areas, I know enough from scoping out a "learn about the proof of FLT" course that it's covering all the usual suspects and says the right-enough words. Patching their weaker results with someone else's seem like a good strategy (and I could find the result on arXiv so it isn't obviously hallucinated).
This is very different to believing the proof, which would require at least a pass understanding the general approach, seeing that it all actually fits together, then going deeper. At some point you transition to relying on the Lean all hanging together, but as mathematicians we all draw that line somewhere.
But yeah, makes sense. Same thing if you saw news on someone's new database technique to improve performance. If they say the right words, don't say the wrong words, and if you cared enough you'd do spot checks proportional to the claim. If pressed you'd examine the source code, and run independent checks. But if smells roughly right, that's a good first approximation.","title":null,"type":"comment","url":null},{"author":"zmgsabst","children":[{"author":"atombender","children":[{"author":"auntienomen","children":[],"created_at":"2026-09-05T02:54:29.000Z","created_at_i":1788576869,"id":49572655,"options":[],"parent_id":49571594,"points":null,"story_id":49568506,"text":"Frenkel does a nice job explaining the Langlands program in general. But Buzzard's complaint about Langlands, I believe, refers specifically to the proof of a version of the Geometric Langlands Conjecture by Gaitsgory et al. The proo f is of order thousand pages of mathematical text and builds off of thousands of pages of higher-categorical algebraic geometry by Lurie & others. It's a ripe target for formalization because it's terrifically complicated, not well understood or thoroughly digested yet, and relatively important. A formal proof would be reassuring to mathematicians, whereas Fermat's Last Theorem is relatively unique in that so many mathematicians have examined the proof that it's not very likely to be wrong.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:59:02.000Z","created_at_i":1788566342,"id":49571594,"options":[],"parent_id":49570760,"points":null,"story_id":49568506,"text":"About the Langlands program, Nunberphile has an excellent episode with Edward Frenkel explaining what it's about: https://youtu.be/4dyytPboqvE.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:02:28.000Z","created_at_i":1788559348,"id":49570760,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"I did an undergrad in math with a little research in number theory and recognized parts \u2014 eg, I myself worked through the proof for odd regular primes and that 37 is irregular, breaking the general case.
Wiles-Taylor-Wiles was the original proof by Andrew Wiles, and its corrections.
Galois representations is about vectors over Galois extensions, which are essentially adding roots to regular numbers (rationals, integers, etc). That ties into the Langlands program, which is a big area in number theory (that I don\u2019t know much about).
Together with flat deformations and Frey curve, I think they\u2019re talking about a topic in algebraic geometry as applied to number theory.
I also recognize the name Eisenstein from my time as an undergrad, though two decades out and not working in the field I\u2019ve forgotten what his work on ideals implied here. Ideals are a well-known topic though, a sort of structure inside a ring (set with + and *) that is closed under operations \u2014 like evens in the integers are the 2Z ideal.
So I\u2019d describe it as \u201csensible with an undergrad background\u201d.","title":null,"type":"comment","url":null},{"author":"LanceH","children":[],"created_at":"2026-09-04T22:03:00.000Z","created_at_i":1788559380,"id":49570767,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"It's something you would have to be keeping up with as a mathematician, really.
Vaguely. It's describing connections between a number of other mathematics results than can be connected to prove FLT. I assume all the work described is being done to make the proof more presentable, smaller, basically "prettier".
It sounds like they established a minimum and maximum bounds for n in x^n + y^n = z^n, where one proof works for n greater than or equal to 17, and another proof for n < 37 (when prime).
I believe the case (remembering back 40 years here) n is even is very easy, and n is composite and odd slightly less so. Neither really being in the ballpark of what they describe here.","title":null,"type":"comment","url":null},{"author":"UltraSane","children":[{"author":"hackandthink","children":[],"created_at":"2026-09-05T01:28:30.000Z","created_at_i":1788571710,"id":49572187,"options":[],"parent_id":49571506,"points":null,"story_id":49568506,"text":"if you are a fast learner","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T23:44:53.000Z","created_at_i":1788565493,"id":49571506,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"advanced math like this takes 10 years to learn all the tower of things it is based on.","title":null,"type":"comment","url":null},{"author":"jibal","children":[],"created_at":"2026-09-04T23:49:05.000Z","created_at_i":1788565745,"id":49571529,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"I'm not a mathematician and I don't see the problem, at all.","title":null,"type":"comment","url":null},{"author":"skipants","children":[],"created_at":"2026-09-05T00:06:49.000Z","created_at_i":1788566809,"id":49571655,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"Funnily enough, this is more readable to me than most Clayde jargon.","title":null,"type":"comment","url":null},{"author":"mathisfun123","children":[],"created_at":"2026-09-05T01:28:42.000Z","created_at_i":1788571722,"id":49572189,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"This question gets asked every single time a serious mathematical result gets posted.","title":null,"type":"comment","url":null},{"author":"contubernio","children":[{"author":"YeGoblynQueenne","children":[],"created_at":"2026-09-05T14:17:18.000Z","created_at_i":1788617838,"id":49576729,"options":[],"parent_id":49576631,"points":null,"story_id":49568506,"text":"Well, if I were a mathematician, what I'd be noodling about with right now is a way to model the number of failed attempts that AI companies must be making for every success they report.
I guess you don't have to be a mathematician to do that sort of calculation, but I'm just proposing it as a way to lift mathematicians' spirits a bit.
Also pay attention to the fact that every time a new model is released there's a slew of new results and then they dry out for a while, which suggests a "throw stuff at the wall and keep what sticks" approach that's incompatible with a kind of system that can just magickally solve all maths right now.
I'm saying that because I get the feeling that mathematicians don't have a good model for the true capabilities of those systems and that can lead to an overreaction, like "woe is me, all of mathematics will be solved and my entire discipline will be rendered obsolete". Coming from an AI background I don't think that's right. I think because mathematicians are not AI researchers they simply don't have a very clear idea of what's going on with those systems. And tbf even many AI researchers (the ones who don't enjoy the benefits of a long tradition that goes back to the 1950's and basically only joined the field in the last 10 years or so) don't understand those systems very well either.
Bottom line: don't panic.
Or, not yet :0)","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T14:05:04.000Z","created_at_i":1788617104,"id":49576631,"options":[],"parent_id":49570557,"points":null,"story_id":49568506,"text":"As a mathematician not expert kn these things, yes it scans as reasonable, and yes it has me and most of my colleagues reconsidering what we do for a living.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T21:41:05.000Z","created_at_i":1788558065,"id":49570557,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":""The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon\u2013Diamond\u2013Taylor exposition from 1995 of the Wiles\u2013Taylor\u2013Wiles argument, via the Langlands\u2013Tunnell theorem and Ribet\u2019s level-lowering theorem. Anthropic\u2019s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur\u2019s work on the Eisenstein ideal to conclude that no Frey curve can have a point of order p>=17. This means that their FLT proof only works for p>=17, however FLT was already formalized for odd regular primes by Best-Birkbeck-Brasca-Rodriguez, and the smallest irregular prime is 37, so it\u2019s all good."
My question to any mathematician reading this: does the above make ANY sense to you?
I ask that because I can read most technical material related to computer engineering, programming, hardware specifications etc. Even if I don't fully understand all details, I can follow them pretty well. So I wonder if professional mathematicians can look at the above and still make sense of it like experienced software engineers do for computer stuff.","title":null,"type":"comment","url":null},{"author":"maw","children":[],"created_at":"2026-09-04T21:55:01.000Z","created_at_i":1788558901,"id":49570698,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I have discovered a truly marvellous proof of this, which this margin is too narrow bear the load.","title":null,"type":"comment","url":null},{"author":"vmilner","children":[],"created_at":"2026-09-04T22:38:59.000Z","created_at_i":1788561539,"id":49571033,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Formalisation of the classification of finite simple groups must be on someone\u2019s \u2018moonshot\u2019 list.","title":null,"type":"comment","url":null},{"author":"logicallee","children":[{"author":"sanxiyn","children":[],"created_at":"2026-09-04T23:40:44.000Z","created_at_i":1788565244,"id":49571477,"options":[],"parent_id":49571065,"points":null,"story_id":49568506,"text":"Lean's three standard axioms are documented in The Lean Language Reference.
https://lean-lang.org/doc/reference/latest/Axioms/#standard-...
The axiom of choice: axiom Classical.choice {\u03b1 : Sort u} : Nonempty \u03b1 \u2192 \u03b1
The axiom of propositional extensionality: axiom propext {a b : Prop} : (a \u2194 b) \u2192 a = b
The quotient axiom: axiom Quot.sound : \u2200 {\u03b1 : Sort u} {r : \u03b1 \u2192 \u03b1 \u2192 Prop} {a b : \u03b1}, r a b \u2192 Eq (Quot.mk r a) (Quot.mk r b)","title":null,"type":"comment","url":null},{"author":"auggierose","children":[],"created_at":"2026-09-05T06:23:36.000Z","created_at_i":1788589416,"id":49573623,"options":[],"parent_id":49571065,"points":null,"story_id":49568506,"text":"I don't really know Lean, but I think this means, three axioms on top of their whole type theory machinery, to make it classical. The type theory machinery is the obfuscated encoding of the large set of standard axioms that they don't tell you about. For example, they can encode natural numbers using that machinery.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:42:49.000Z","created_at_i":1788561769,"id":49571065,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"amazing, it's a huge achievement. can someone clarify, where the writeup says "The finished proof was checked by Lean; it uses just Lean\u2019s three standard axioms" what does this mean? Aren't there a large set of standard axioms that are also necessary? (i.e. ZFC+)? if not, since it's only three axioms, can someone say what they were?","title":null,"type":"comment","url":null},{"author":"margorczynski","children":[{"author":"jeremyjh","children":[],"created_at":"2026-09-04T23:02:50.000Z","created_at_i":1788562970,"id":49571205,"options":[],"parent_id":49571192,"points":null,"story_id":49568506,"text":"I will not be surprised if the number is zero. It should have already happened if it were possible.
Proving that a conjecture is false is very different than what you are proposing. You are proposing an existing proof is simply wrong, that the proof can be checked in Lean, and that no one has bothered to check it yet.","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T22:59:58.000Z","created_at_i":1788562798,"id":49571192,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"With how capable and cheap automatic proof verification is becoming I wonder how many proofs assumed to be true by almost all of the math community will be proven false. And not by some marginal easy to fix error by some fundamental flaw in reasoning.","title":null,"type":"comment","url":null},{"author":"max979","children":[],"created_at":"2026-09-04T23:32:21.000Z","created_at_i":1788564741,"id":49571419,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Pretty wild seeing this get formalized. Remember struggling to even grasp the high-level concepts of Wiles's proof.","title":null,"type":"comment","url":null},{"author":"dist-epoch","children":[],"created_at":"2026-09-04T23:42:20.000Z","created_at_i":1788565340,"id":49571490,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Lean required 300 GB of RAM, 96 cores, and took hours to compile and check the formalization.
Now they have the perfect stress test to hill-climb and optimize.","title":null,"type":"comment","url":null},{"author":"dextrous","children":[],"created_at":"2026-09-05T00:40:03.000Z","created_at_i":1788568803,"id":49571881,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Ok, let\u2019s get a rabid pack of agents cranking on P = NP? next!","title":null,"type":"comment","url":null},{"author":"sva_","children":[{"author":"kzrdude","children":[],"created_at":"2026-09-05T09:49:44.000Z","created_at_i":1788601784,"id":49574910,"options":[],"parent_id":49572012,"points":null,"story_id":49568506,"text":"The OP is about formalizing an existing result, not coming up with a new proof for FLT.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T01:00:03.000Z","created_at_i":1788570003,"id":49572012,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Hmm kind of funny, some years ago someone claimed LLMs can do math, and I replied if it could prove fermants theorem:
https://news.ycombinator.com/item?id=33176996#33177939
> Now try to make a computer prove that there are no natural numbers a,b,c; so that a^n + b^n = c^n for any n > 2.
> > Shifting the goal posts a bit, aren't we?
I guess the goalposts did change a bit, and in a pretty short time.","title":null,"type":"comment","url":null},{"author":"throw567643u8","children":[],"created_at":"2026-09-05T01:16:06.000Z","created_at_i":1788570966,"id":49572123,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"13 million lines of code, a lot of which is new to Mathlib. So it hasn't built on what is already there but synthesised a bunch of new stuff.
LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.","title":null,"type":"comment","url":null},{"author":"throw567643u8","children":[{"author":"Jblx2","children":[],"created_at":"2026-09-05T02:26:14.000Z","created_at_i":1788575174,"id":49572513,"options":[],"parent_id":49572173,"points":null,"story_id":49568506,"text":"Not mm0?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T01:26:56.000Z","created_at_i":1788571616,"id":49572173,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.","title":null,"type":"comment","url":null},{"author":"throwaboat","children":[],"created_at":"2026-09-05T01:39:42.000Z","created_at_i":1788572382,"id":49572251,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I wrote a similar DAG-based verifier as a skill a few months ago: https://github.com/sethlei/Warrant . The thing mine has that I didn't see in their's is a verification of the composition rules.
Mine also does more than just math.","title":null,"type":"comment","url":null},{"author":"cyode","children":[],"created_at":"2026-09-05T02:20:24.000Z","created_at_i":1788574824,"id":49572477,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I saw the 1996 FLT documentary in high school calculus class. For me, it forever cemented that archetype of modern math researcher at the top of my mental \u201csmart\u201d totem pole.
It also convinced me I had no interest in that path. Setting aside the grinding work of producing a proof that can only be reached by existing years in the abstract and hyper niche isolation of the problem space (not to mention that you might never discover it or that it DNE), the anguish of the output being a paper or presentation or some other artifact of human symbology (_words_, really) that could at any moment be refuted by a single observation of a single mistake\u2014-that sounded like hell to me.
An equivalent high schooler today probably sees things differently, in light of this news and the undeniable implications of LLMs on mathematics. Sturdy autoformalization tooling should with time completely dispel the aforementioned anguish, once our confidence in converting a human proof to Lean/etc. reaches that of a compiler translating Java application language to bytecode. Errata may always exist, but in practice these new methods will do wonders for rigor and peace of mind.
(I\u2019m far less confident re novel discoveries. There\u2019s too much chance of derivative findings based on something part of the training looking like genius but really just tiptoeing on the shoulders of humans, whereas autoformalization is absolutely convincing to me as transformative, particularly to check correctness of AI outputted proofs as mentioned in the post.)","title":null,"type":"comment","url":null},{"author":"MichaelDairy","children":[],"created_at":"2026-09-05T03:08:04.000Z","created_at_i":1788577684,"id":49572726,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I think Anthropic might the frontier lab hiring contractors through data vendors to formalize mathematical textbooks for them at a rate of 170-200 dollars per hour. This was mainly through Alignerr which has the worst reputation for not paying their contractors. They have been hiring since February as far as I can recall. This is in addition to all the internal people they might have working on this. If they have been formalizing all this work for the past 9 months before having Claude use all this data needed to formalize FLT, then it wouldn't be Claude formalizing FLT in just 11 days. Same with the upcoming results they will claim Claude came up with, but in fact they have been hiring frontier researchers working on very niche topics through Micro1. It's all a marketing ploy before their IPO.","title":null,"type":"comment","url":null},{"author":"herbcso","children":[{"author":"twiceaday","children":[{"author":"throw-qqqqq","children":[],"created_at":"2026-09-05T08:46:32.000Z","created_at_i":1788597992,"id":49574573,"options":[],"parent_id":49572880,"points":null,"story_id":49568506,"text":"Great explanation. I\u2019ve heard this referred to, as The Formal Specification problem.
From https://en.wikipedia.org/wiki/Formal_specification#Limitatio...
> A design (or implementation) cannot ever be declared \u201ccorrect\u201d on its own. It can only ever be \u201ccorrect with respect to a given specification.\u201d Whether the formal specification correctly describes the problem to be solved is a separate issue.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T03:39:47.000Z","created_at_i":1788579587,"id":49572880,"options":[],"parent_id":49572846,"points":null,"story_id":49568506,"text":"Lean is like a statically typed programming language and validity is guaranteed if it compiles. The only room for errors is in translating a non-Lean theorem into Lean, so that you are not proving what you think you are proving.","title":null,"type":"comment","url":null},{"author":"thevivekpandey","children":[{"author":"gorgolo","children":[{"author":"SkidanovAlex","children":[{"author":"YeGoblynQueenne","children":[],"created_at":"2026-09-05T13:59:43.000Z","created_at_i":1788616783,"id":49576577,"options":[],"parent_id":49573319,"points":null,"story_id":49568506,"text":"Couldn't the kernels have different bugs?","title":null,"type":"comment","url":null},{"author":"thejokeisonme","children":[],"created_at":"2026-09-05T17:51:17.000Z","created_at_i":1788630677,"id":49578937,"options":[],"parent_id":49573319,"points":null,"story_id":49568506,"text":"You emphasize TWO as of these kernels are so different.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T05:22:56.000Z","created_at_i":1788585776,"id":49573319,"options":[],"parent_id":49573260,"points":null,"story_id":49568506,"text":"It is the latter. If you are certain your theorem is stated correctly, and you believe that the Lean kernel against which you validate is correct, your proof is correct.
This is how the theorem for FLT looks in the particular proof we discuss here:
theorem fermat_last_theorem (n : \u2115) (hn : 3 \u2264 n) (a b c : \u2115)\n (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n \u2260 c ^ n
As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of code, and if the kernel says it is correct, it is correct.
This proof was checked against TWO independently built kernels. So you would need TWO kernels to have the same bug to mistakenly accept an incorrect proof.
(Not impossible: such a bug indeed was recently discovered (and patched))","title":null,"type":"comment","url":null},{"author":"aureianimus","children":[],"created_at":"2026-09-05T05:25:01.000Z","created_at_i":1788585901,"id":49573330,"options":[],"parent_id":49573260,"points":null,"story_id":49568506,"text":"There's no guarantee that the intermediate statements match the informal mathematical intermediate statements, but if there is a mismatch, then this has to be repaired elsewhere to yield a proof that passes the Comparator tool. Running this tool indeed reduces the correctness question to what the parent comment mentioned.","title":null,"type":"comment","url":null},{"author":"raincole","children":[],"created_at":"2026-09-05T05:31:51.000Z","created_at_i":1788586311,"id":49573367,"options":[],"parent_id":49573260,"points":null,"story_id":49568506,"text":"If you just "translate" an existing proof step by step to Lean, then of course you could mis-encode the intermediate statements too. But if you mis-encode the steps and still pass Lean check, it means you found a new proof! (Or you found a bug in Lean)","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T05:11:32.000Z","created_at_i":1788585092,"id":49573260,"options":[],"parent_id":49572884,"points":null,"story_id":49568506,"text":"> That theorem statement is correctly encoded (FLT has a very short 1 liner description really)
As someone not very familiar with Lean, does it really just depend on the entry point / theorem being correctly encoded? Can intermediate statements ever be mis encoded or misinterpreted, or is this what would count as a \u201cbug in the Lean compiler\u201d?","title":null,"type":"comment","url":null},{"author":"thrance","children":[],"created_at":"2026-09-05T12:12:17.000Z","created_at_i":1788610337,"id":49575784,"options":[],"parent_id":49572884,"points":null,"story_id":49568506,"text":"And (3) the axioms are correctly encoded too.","title":null,"type":"comment","url":null},{"author":"not-so-darkstar","children":[{"author":"robotpepi","children":[{"author":"not-so-darkstar","children":[],"created_at":"2026-09-05T12:46:15.000Z","created_at_i":1788612375,"id":49576024,"options":[],"parent_id":49575918,"points":null,"story_id":49568506,"text":"I think the other commenters are right, as long as the statement of FLT is correct and no funny stuff is used (admitting theorems without proof or defining new axioms) then it doesn't matter what you used in the proof.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T12:32:40.000Z","created_at_i":1788611560,"id":49575918,"options":[],"parent_id":49575843,"points":null,"story_id":49568506,"text":"that's something a human needs to do, and it's non trivial, but it's a simple task compared to checking the correctness of the proof. in any case, most of the language is probably already defined in Lean and checked independently by many people.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T12:21:10.000Z","created_at_i":1788610870,"id":49575843,"options":[],"parent_id":49572884,"points":null,"story_id":49568506,"text":"What if the mathematical objects are not encoded "correctly"?
For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T03:40:51.000Z","created_at_i":1788579651,"id":49572884,"options":[],"parent_id":49572846,"points":null,"story_id":49568506,"text":"In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type.
If the compiler certifies that the code indeed produces a term of that type, then the proof is correct.
So, only need to trust:\n(1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really)
(2) Lean compiler is correct","title":null,"type":"comment","url":null},{"author":"raincole","children":[{"author":"lepton","children":[{"author":"robotpepi","children":[],"created_at":"2026-09-05T12:30:00.000Z","created_at_i":1788611400,"id":49575905,"options":[],"parent_id":49574913,"points":null,"story_id":49568506,"text":"you're missing the point...","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T09:50:21.000Z","created_at_i":1788601821,"id":49574913,"options":[],"parent_id":49572970,"points":null,"story_id":49568506,"text":"What are the chances that a small C program uncovers a bug in the C compiler, maybe in its type checker?
What are the chances that a very large C program uncovers a bug in the C compiler?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T04:04:58.000Z","created_at_i":1788581098,"id":49572970,"options":[],"parent_id":49572846,"points":null,"story_id":49568506,"text":"The answer is we don't really know [0]:
> In 2026, AIs designed to spot bugs in software were directed at Lean, and found several loopholes which were then fixed. Perhaps related to this effort, a purported disproof of the Collatz conjecture was announced as verified in Lean. However, this proof was soon determined to rely on a bug in Lean, and once the bug was fixed the proof was found invalid
However it's a bit different than the usual 'bugs' we encounter in normal software development. Lean is more like a type checker. If you can write a false proof in Lean then the bug is in Lean itself, not your code.
In other words, Lean can have bugs, but the amount of code we need to check scales with Lean itself, not with the length of proof. Just like the chance that C compiler has bugs doesn't increase as we write more C code. So the 13M lines of code doesn't really matter here.
[0]: https://en.wikipedia.org/wiki/Lean_(proof_assistant)","title":null,"type":"comment","url":null},{"author":"dwohnitmok","children":[],"created_at":"2026-09-05T04:59:49.000Z","created_at_i":1788584389,"id":49573211,"options":[],"parent_id":49572846,"points":null,"story_id":49568506,"text":"The structure of Lean does impose that. The code isn't being run, it's being type checked. And that's it. The overwhelming majority of Lean code is never run. It exists only to be type checked (because type checking is equivalent to verifying the proof).
You could imagine the typechecker has bugs (and indeed another comment mentions examples of bugs!). Crucially though anytime the typechecker has a bug fixed you could rerun the typechecker on the code to see if it still type checks.
This is the whole promise of formal verification. It reduces the problem of verification purely to the typechecker. If the typechecker is correct, then the proof is verified, no matter how many lines of code the proof is. As a sibling comment puts it, the chance of bugs mainly scales with the number of lines of code in the typechecker, not in the amount of lines of Lean code.
Your question is akin to asking, "yes this spellchecker ran fine on your essay, but are you sure it runs fine on War and Peace? That's 1000x more words!" To which the answer is the number of words doesn't matter if the spell checker is correct (which it might not be! And longer passages might reveal more bugs! But you can always rerun it). The main source of bugs is more lines of code in the spell checker, not in number of words in the text.","title":null,"type":"comment","url":null},{"author":"throw567643u8","children":[{"author":"throw-qqqqq","children":[{"author":"throw567643u8","children":[{"author":"FartyMcFarter","children":[],"created_at":"2026-09-05T12:21:08.000Z","created_at_i":1788610868,"id":49575842,"options":[],"parent_id":49574803,"points":null,"story_id":49568506,"text":"Stack overflows are also trivial to check for, if one wants to. It's just comparing two pointers, plus checking for arithmetic overflow (in case the pointers run past the maximum value of the pointer type).","title":null,"type":"comment","url":null},{"author":"throw-qqqqq","children":[],"created_at":"2026-09-05T16:25:39.000Z","created_at_i":1788625539,"id":49578085,"options":[],"parent_id":49574803,"points":null,"story_id":49568506,"text":"I would say it\u2019s very unlikely to be the case here at least.
Of course some bugs in Lean may exist (I don\u2019t have deep insight into Lean\u2019s implementation and there have been bugs before), but I find it unlikely to be systematical or in a format that could affect the proof.
As I understand it, Lean is implemented in Lean and emits/compiles to C. In that C code, I\u2019d be very surprised if any buffer overflows or stack overflows exist.
Such overflows are not difficult or expensive to detect, so if any were there, it should cause a crash instead of an incorrect result.
It\u2019s not as in handwritten C where you can forget or omit a bounds check.
I\u2019d say it is even less likely than seeing an overflow in the Core of Java cause an incorrect result (i.e. corruption instead of a crash) - because Lean uses the De Bruijn principle of reducing to a very small Core, that is easier to keep correct (others in this thread have expanded on this I better than I can I think).
Out of pure curiosity: Do you believe otherwise or have a reason to think I am mistaken?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T09:28:21.000Z","created_at_i":1788600501,"id":49574803,"options":[],"parent_id":49574610,"points":null,"story_id":49568506,"text":"So would you also say no chance of a stack overflow or any type of surreptitious storage overflow anywhere in the runtime do you think?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T08:51:41.000Z","created_at_i":1788598301,"id":49574610,"options":[],"parent_id":49573533,"points":null,"story_id":49568506,"text":"Buffer overflows are trivial to check for at runtime (~proof-checking-time) and Lean does this. Just like Java does it.
I\u2019d wager a million gazillion bucks that this is not the case.","title":null,"type":"comment","url":null},{"author":"YeGoblynQueenne","children":[],"created_at":"2026-09-05T14:10:53.000Z","created_at_i":1788617453,"id":49576685,"options":[],"parent_id":49573533,"points":null,"story_id":49568506,"text":"It doesn't seem execution was a problem. From Kevin Buzzard's blog:
I\u2019ve compiled the code base and run comparator on it \u2014 it checks out. It is a gigantic proof (over 13.4 million lines of code) and takes nearly 20 times as long to compile as Lean\u2019s mathematics library (on a machine with 96 cores!). Lean can be sluggish when jumping from file to file on a repo of this size (even on a machine with 500G of ram, which Anthropic also gave me access to), but Anthropic also supplied me with some html documents which are easier in practice to explore (clone the repo and open with a web browser).
500G of RAM is not actually that huge tbh (I was looking to buy a used 1TB server blade for some personal stuff a while ago but it was too much hassle) so I don't guess there was too much potential for buffer overflows.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T06:06:32.000Z","created_at_i":1788588392,"id":49573533,"options":[],"parent_id":49572846,"points":null,"story_id":49568506,"text":"With the size of the proof object, a potential buffer overflow comes to mind.","title":null,"type":"comment","url":null},{"author":"voidhorse","children":[{"author":"latent-person","children":[],"created_at":"2026-09-05T12:19:06.000Z","created_at_i":1788610746,"id":49575828,"options":[],"parent_id":49575722,"points":null,"story_id":49568506,"text":"From the article:
> The finished proof was checked by Lean; it uses just Lean\u2019s three standard axioms, and a comparator confirmed that the theorem\u2019s statement matches Mathlib\u2019s own statement of FLT.
So it proved the statement of FLT made independently in Mathlib. So no reason to not trust it proved the correct thing.","title":null,"type":"comment","url":null},{"author":"FartyMcFarter","children":[{"author":"SpicyLemonZest","children":[],"created_at":"2026-09-05T17:23:44.000Z","created_at_i":1788629024,"id":49578632,"options":[],"parent_id":49575831,"points":null,"story_id":49568506,"text":"But what does it matter whether we can "trust its verification of the 13 million lines of code"? We already knew that Fermat's Last Theorem is true, we don't need Lean to tell us that. The value of a formalization would be to improve our understanding of why it's true, and that can't be achieved by 13 million lines of code no human being has read.
The source article does acknowledge this isn't a replacement for human analysis, but they seem to imagine a vision of mathematical research where there's a bunch of AIs running around proving random things and formalizing them into opaque Lean proofs nobody ever has to read. I'm skeptical whether there's any value in doing that, and to the extent that there is I'm pretty confident it looks more like proving certain directions aren't fruitful for further investigation.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T12:19:28.000Z","created_at_i":1788610768,"id":49575831,"options":[],"parent_id":49575722,"points":null,"story_id":49568506,"text":"> What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode
I don't think the comments are missing that at all. If the Lean compiler itself is bug-free, we can trust its verification of the 13 million lines of code. We don't need to verify them by hand.
The encoding of the theorem itself needs to be trusted, as does the compiler. The proof doesn't need to be trusted, it gets checked by the compiler.","title":null,"type":"comment","url":null},{"author":"Smaug123","children":[],"created_at":"2026-09-05T12:26:25.000Z","created_at_i":1788611185,"id":49575880,"options":[],"parent_id":49575722,"points":null,"story_id":49568506,"text":"Fortunately FLT is an extremely simple statement. Much easier to satisfy yourself that its statement is what you wanted to say than it would be for most statements of interest!","title":null,"type":"comment","url":null},{"author":"YeGoblynQueenne","children":[],"created_at":"2026-09-05T14:08:38.000Z","created_at_i":1788617318,"id":49576666,"options":[],"parent_id":49575722,"points":null,"story_id":49568506,"text":"No expertise at all on interactive theorem provers like Lean but I am familiar with Resolution-based automated theorem proving. In that setting, one writes down a theory, in the form of a set of first-order definite program clauses, and then presents a statement to the prover, then the prover proceeds to prove the statement is a theorem derived from the theory.
Is that (other than the language not being definite logic) more or less what Lean does also? In that case, isn't all the work in writing down the theory, and isn't that the step where mistakes can creep in?
Is that more or less what you're pointing out? That FLT is simple enough to state but the theory from which it is to be derived can be mangled and so accept FLT on the wrong grounds?","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T12:03:36.000Z","created_at_i":1788609816,"id":49575722,"options":[],"parent_id":49572846,"points":null,"story_id":49568506,"text":"To me, a lot of the child comments on this thread are technically correct (the best kind) in that, yes correctness bugs in Lean boil down to compiler bugs in a language like lean.
What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode is still a major problem and yes, extremely difficult when you have that many lines to pore over. But, if you're using LLMs to vibe code millions of lines of "proof" you've already stopped caring about that and presumably given your critical reasoning and concern over to pure faith in machine gods anyway.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T03:31:30.000Z","created_at_i":1788579090,"id":49572846,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That just feels like a LOT of code to be comletely error-free... What am I missing here?","title":null,"type":"comment","url":null},{"author":"Goofy_Coyote","children":[],"created_at":"2026-09-05T04:27:45.000Z","created_at_i":1788582465,"id":49573073,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"For math illiterate people like me, my understanding is that FLT was already proven, but the proof was beyond complex, certainly for mere mortals like me, and now Claude has codified it, correct?","title":null,"type":"comment","url":null},{"author":"andychiare","children":[],"created_at":"2026-09-05T08:18:06.000Z","created_at_i":1788596286,"id":49574334,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"We are in the context of "who verifies the verifier?" :-)","title":null,"type":"comment","url":null},{"author":"mettamage","children":[],"created_at":"2026-09-05T09:39:20.000Z","created_at_i":1788601160,"id":49574842,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"First of all, this is an amazing result. Second, I'm not too surprised, given all what has happened before.
The thing is: LLMs are not grounded in reality enough as much as we are. Using Lean is exactly what that is: grounding LLMs in reality.
We have (at least) 30 FPS vision, and can detect 5 ms audio delays, we do that in real-time. LLMs have access to some images and large amounts of text. Their propensity is to predict the next token. So the propensity to be additive and just say something (aka predict the next token) is higher than predicting something to stop.
If LLMs would have:\n- 30 FPS vision\n- similar hearing ability\n- an ability to feel their lived experience\n- consequences to their "life"
They'd be making more intelligent decisions than they are doing now. Simply because they have more context.
Because in this sense, we have a lot more context than LLMs. Yet, I see people sometimes treating them as if they are at the same level as humans because their intelligence is similar. And that might be true, but where they get their data from is vastly different. Given our tasks, they are at a disadvantage. They need to sense more of reality.
Have fun sharing the room with these digital intelligences. Given the topics they can consume, they are already better generalists than any individual. I might be wrong of course, I'd love to meet any individual that's a better generalist than an LLM.","title":null,"type":"comment","url":null},{"author":"amelius","children":[{"author":"FartyMcFarter","children":[{"author":"amelius","children":[],"created_at":"2026-09-05T15:11:28.000Z","created_at_i":1788621088,"id":49577323,"options":[],"parent_id":49575500,"points":null,"story_id":49568506,"text":"Yeah they tried that, but the proof didn't fit.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T11:23:41.000Z","created_at_i":1788607421,"id":49575500,"options":[],"parent_id":49575478,"points":null,"story_id":49568506,"text":"5 minutes later, the AI concludes the best strategy is to start a universe simulation and let Fermat write the proof in a margin. Recurse.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T11:20:08.000Z","created_at_i":1788607208,"id":49575478,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"They should let AI work on it until the proof fits in the margin of a page.","title":null,"type":"comment","url":null},{"author":"jeanmichelselli","children":[{"author":"Smaug123","children":[],"created_at":"2026-09-05T12:29:59.000Z","created_at_i":1788611399,"id":49575904,"options":[],"parent_id":49575574,"points":null,"story_id":49568506,"text":"The LLM is not the thing applying the logical rules. That is instead the deterministic system Lean 4. (Also that Apple paper was garbage even when it was written, assuming you\u2019re referring to The Illusion of Thinking, and LLMs have got much better since.)","title":null,"type":"comment","url":null},{"author":"auggierose","children":[],"created_at":"2026-09-05T15:25:47.000Z","created_at_i":1788621947,"id":49577455,"options":[],"parent_id":49575574,"points":null,"story_id":49568506,"text":"Kevin Buzzard is a mathematician as well, and he thinks it's ok. I am a mathematician, too, and I know it is ok. What I find fascinating is how little mathematicians still know about this. But I am used to that attitude towards interactive theorem proving for quite some time. The difference now: if you don't adapt, you are obsolete and done for as a mathematician.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T11:36:01.000Z","created_at_i":1788608161,"id":49575574,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I'm a mathematician and I'm not sure one should believe those results right now.. An automatic formalization requires a system of logic rules to be applied, which is not something LLMs are great at (remember the Apple paper a while ago?). I'm very curious to see how the community will react after the initial hype.. so far, it's being quite disappointing..","title":null,"type":"comment","url":null},{"author":"vitriol83","children":[{"author":"auggierose","children":[{"author":"vitriol83","children":[{"author":"auggierose","children":[{"author":"vitriol83","children":[],"created_at":"2026-09-05T17:10:38.000Z","created_at_i":1788628238,"id":49578514,"options":[],"parent_id":49578161,"points":null,"story_id":49568506,"text":"You're stating it's not a problem- but I'm giving you a reason why it is. This is serendipitously mirrored by a recent post from Terence Tao on Mastodon (https://mathstodon.xyz/@tao/117207856734787448)
In most cases in pure mathematics, the problems are posed not because we desperately want the solution to these problems in and of themselves, but because we have seen from past experience that human-directed efforts to solve these problems tend to spur further development of the field through the efforts to solve such problems, and then to digest any partial or complete solutions that emerge for further insights. Prematurely solving the problem by purely AI-powered methods - particularly without full transparency into the solution process - can contaminate this process to the point where it actually becomes a net negative for the progress of mathematics as a whole.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T16:33:25.000Z","created_at_i":1788626005,"id":49578161,"options":[],"parent_id":49577829,"points":null,"story_id":49568506,"text":"You can say that American society made OpenAI and Anthropic possible. No other current society would have. Suddenly, formalisation of math is becoming cheap. That's not a problem, that's the goal, and it is here much earlier than expected. That's not antisocial. That is scientific progress.
(I swear, did not use an LLM for this)","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T16:02:00.000Z","created_at_i":1788624120,"id":49577829,"options":[],"parent_id":49577506,"points":null,"story_id":49568506,"text":"yes society has let the trillion dollar company down","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T15:31:03.000Z","created_at_i":1788622263,"id":49577506,"options":[],"parent_id":49576085,"points":null,"story_id":49568506,"text":"Maybe society has the wrong values. Maybe society needs to rethink incentives. Maybe society is somewhat antisocial.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T12:57:32.000Z","created_at_i":1788613052,"id":49576085,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"i find this and other efforts from anthropic somewhat antisocial. technically they have achieved their goal, but in a way which does not benefit mathematics or humanity. Kevin Buzzards headline goal was to formalise FLT, but i\u2019m sure the real aim was to create a formalised library of mathematics which is comprehensible to humans. By solving these famous problems by brute force, they are disincentivising the important work of making it digestible for everyone else, and so in my view this work in particular has negative societal value.","title":null,"type":"comment","url":null},{"author":"satnhak","children":[],"created_at":"2026-09-05T17:08:16.000Z","created_at_i":1788628096,"id":49578494,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"I used to attend Kevin's Number Theory seminars at Imperial College many years ago and he's both a first rate mathematician and a very nice person. His blog has got me interested in maths again. Considering how pro AI he is and that he's been working on this problem for such a long time I'm a bit disappointed that Anthropic didn't involve him directly in this work. However, I think it's important to remember that without all of the work Kevin and people like him have done, the machines wouldn't be able to do this.","title":null,"type":"comment","url":null},{"author":"imranq","children":[{"author":"jebarker","children":[{"author":"mkehrt","children":[{"author":"JamesSwift","children":[{"author":"dwaltrip","children":[],"created_at":"2026-09-05T20:10:03.000Z","created_at_i":1788639003,"id":49580215,"options":[],"parent_id":49579746,"points":null,"story_id":49568506,"text":"I'd trust Terence's view on this.
Also, that Sudoku analogy doesn't sound right to me. Math progress is more complex than that.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T19:19:39.000Z","created_at_i":1788635979,"id":49579746,"options":[],"parent_id":49579400,"points":null,"story_id":49568506,"text":"That seems narrow minded. Theres both "learnings directly related to the thing studied" and "learnings downstream from the thing studied". If you imagine mathematics being a huge sudoku puzzle of unknowns you are trying to fill in, each previously empty square you are able to fill in (or gain a smaller bound on) has implications in all sorts of other areas.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T18:40:45.000Z","created_at_i":1788633645,"id":49579400,"options":[],"parent_id":49579274,"points":null,"story_id":49568506,"text":"I enjoyed this Terence Tao post the other day.
The relevant quote is
> one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?"
And later
> But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided by any human expert in the field X resides in, has created an unprecedented divergence between the production of answers, and the production of insight, to the point where the two questions have become _negatively correlated_:
https://mathstodon.xyz/@tao/117208618508728654","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T18:26:09.000Z","created_at_i":1788632769,"id":49579274,"options":[],"parent_id":49578845,"points":null,"story_id":49568506,"text":"> Note that this proof while impressive does not add any value to mathematics as a human pursuit.
I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.","title":null,"type":"comment","url":null}],"created_at":"2026-09-05T17:44:15.000Z","created_at_i":1788630255,"id":49578845,"options":[],"parent_id":49568506,"points":null,"story_id":49568506,"text":"Note that this proof while impressive does not add any value to mathematics as a\nhuman pursuit. But it does show we can throw these LLM beasts at much gnarlier\nproblems than we could have imagined previously. Maybe even formally verify papers the day they are posted?
I'd love to see an e2e compiler or OS kernel verification or Full-stack chip design with formal equivalence checking at each stage that would be pretty cool.
What else is interesting is how they staged this problem : (a) maintain an explicit DAG/roadmap of sub-goals rather than one flat prompt, (b) separate statements from proofs so many agents can work on different nodes without stepping on each other, (c) keep a natural-language index alongside the formal one so search/reuse works... I feel like this is the future of long horizon agents and how you can do work that's making the most of every agent. This approach will likely be baked into the next versions of coding harnesses","title":null,"type":"comment","url":null}],"created_at":"2026-09-04T18:42:56.000Z","created_at_i":1788547376,"id":49568506,"options":[],"parent_id":null,"points":726,"story_id":49568506,"text":"https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...","title":"Formalizing Fermat's Last Theorem","type":"story","url":"https://www.anthropic.com/research/formalizing-fermats-last-theorem"}