I have never seen an AI or a human produce a false proof without explicitly using weird meta programming tricks that are very suspicious. No "good faith" Lean proofs have every been shown faulty, to the best of my knowledge. While the risk is non-zero, many of the AI companies are also trying to find bugs in the Lean kernel, so it is becoming very well stress-tested.
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.
This being 13M lines of entirely agent-generated code, we can't be certain it's written in good faith and doesn't actually exploit some weird metaprogramming trick. The agents' goal was to write a proof that Lean prints "correct" on, not to check that the proof of the FLT was valid (which they wouldn't be able to do anyway).
It's not impossible, but I also know of no instances of an AI being told to prove something in Lean and exploiting such tricks. Surely Anthropic also had some agents looking for issues with the generated proofs. Personally, I am also comfortable trusting Kevin Buzzard, who was leading the human team aiming to formalize FLT and discussed this a bit on his blog.
Finally, the good thing about Lean is that if anyone ever finds a new compiler bug (which, by the way, are being searched for extensively using AI), you can correct the bug and recompile any old proofs of which you are suspicious. Any tricks in a false proof must be exploiting a bug in the Lean compiler, so as we increase trust in the compiler over time we also increase trust in every previously compiled proof.
I agree it's not a 100% guarantee, but in this case the human proof is well-understood and written about by many experts, so I think Claude had plenty of material to work with. Even if the task was enormous, I don't think any of the individual steps are out of the scope of what we have seen from current AI tools.
Watermarking just alters the pseudorandom number generator. If "I like turtles" was previously the response to your prompt with probability 100%, it will still be so. This is why watermarking is only effective for long strings of text
It's like the sudden change of a language style and its verbosity didn't happen recently.
To random words you pick and provide a sufficient amount of text to vary with random number without losing its meaning you need a text with high entropy.
Nothing about watermarking would require padding the response length with pseudo-intelligible Claudese. Regular filler would work fine.
Also, it would probably provide higher entropy to write normal human-sounding English instead of reusing a repetitive grab bag of load-bearing phrases. This theory doesn't really make any sense.
I think the old reddit redirect extension gets around this somehow, that has worked for me lately (occasionally with some toggling of the extension). Although maybe it's best to just use less reddit tbh
But it's a good thing, actually because:
- when reddit is good it's way to addictive
- reddit has become nearly as bad as most other social media sites
So if they force me to use an account, I'll finally be able to kick the habit ;-)
There is a cookie that you can set to still get the old interface without login on www.reddit.com (but NOT on old.reddit.com) which some of the deshittify-redditi extensions have added. But I wouldn't expect that to stick around - it's just there for now to soften the outrage.
Make that 'since forever'. But there used to be a lot of insightful discussion inbetween the facebook-like parts. (Maybe it was the same on facebook, I wouldn't know because I never had a facebook account and you can't access the site without it.)
But I deleted my account (or at least randomized my password) somewhere in 2016 or so, so apparently 10 years ago I decided I wanted out. But I'm still reading it at least as much as HN. So fingers crossed they screw up badly enough this time :-D
You don't always need an extension to use old.reddit.com, it's an actual setting if you're logged in.
The real problem is that old.reddit.com and its ecosystem are all becoming worse and worse. Just off the top of my head, things like image galleries, message notifications, RemindMe bot, RES, /r/random, etc all have various problems and breakage.
I resigned as a mod after the API shitshow and am so glad I did. It’s a terrible site. I wind up there every month or two from friends or looking something up, it’s hard to see how much of a cesspool it is when you’re so invested in it and up close.
To Michael Pollan it seems they aren't worth mentioning right in the first breath when talking about real food, but perhaps an afterthought. "Shop the peripheries" causes them to be lumped in with potato chips and oreos and other stuff that aren't in the peripheries of a supermarket. I don't accept the same real food dichotomy that they do.
Beans are a direct product of plants. I don’t know what you are on about, but I’m sure even the celebrities you take so much stock in consider them “real food”, too. I wouldn’t know, because I have no idea what you’re ranting about.
They talk so much about freshness. That is an indirect and unnecessary and probably unintentional dig at dry beans, grains, seeds, nuts, etc. While I can entertain the idea that they're more reasonable in their diets this makes them bad nutrition communicators.
I mean, it's a collective action problem. Individual consumption of normal people is a huge contributor to global energy demands / pollution / etc. You don't have to change your behavior but if no one does in the coming decades then we're pretty fucked.
Not to let the 1% off the hook. Por que no los dos
You cannot solve societal problems with individual actions.
It's about time to cut the crap that each person can make a difference while governments keep subsidizing all sorts of activities that damage the environment.
I will vote for forbidding beef, but will keep eating it until it is forbidden.
I somewhat agree, and I have not stopped eating beef entirely. I think that forbidding is overkill but agree that lots of related subsidies should be eliminated (honestly, if meat were just priced w/o current subsidies, we'd be in far better shape).
But you have to have some public consensus or the government will never implement such changes due to their unpopularity. This is why I think promoting some reduction in individual meat consumption is still valuable - it is good for average people to reflect on their consumption or they will vote out anyone who attempts to change it.
I don't think that the focus should be on individual blame (even just for the reason that this is politically nonviable). But you at least need to amass some collective awareness.
I love beef. I absolutely adore cheese, and I would be unfathomably sad to never again taste a nice piece of Gorgonzola.
But I know that the meat and dairy industry are hellish for the environment. You don't need to win me in that argument, I accepted that already.
But that's the catch - either we are all in this together, or we will burn in this oven-earth of our making. There's no between. I am not becoming vegan just to die scorched anyway because meat and dairy were still subsidized and consumed.
Governments are surprisingly good to set proper incentives when they want. It could make beef and dairy economically ruinous with taxes instead of forbidding. Consumption would lower dramatically the moment a striploin beef is costing 30 bucks.
If society needs several environmental catastrophes to wake up, then I can only hope I see the other side of it.
There is not a single foundation - you can choose. The differences are rarely important for working mathematicians though. Most know enough of ZFC to get by and ignore foundations tbh
reply