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.
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.
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.
I think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.
The things mega corporations built could be even more valuable (for society) if they didn't intentionally restrict for their own and their shareholders' benefit what you can do with them.
Since they are public companies the shareholder's benefit is to society's benefit.
>"Regulating" also doesn't mean "taking shareholders' benefit
Technically true, but if the regulations are just suggestions then they won't accomplish anything. When people suggest regulation they want to control how these companies are acting, not just sending them a strongly worded letter.
> the shareholder's benefit is to society's benefit
Yes, but there can be other benefits than monetary ones. Besides, I find it rediculous to believe that wealthy people receiving more benefits automatically translates to improvements for the general society.
To add another point: The monetary value these companies create is often only possible because of their monopolistic market distortion. I don't think it can be a net benefit for society when competitors have little to no chance to offer a better product.
> When people suggest regulation they want to control how these companies are acting
That's true. In your original comment you also said "government taking over YouTube" which is why I thought we were talking about complete transfer of control à la planned economy, which is normally not the goal of regulations.
The article did not make me understand that at all.
> Since we're making a new app, we're going to want two things: an app server (which hosts our API & frontend) and a view server (which collects data from the network for us).
Yes, the user data is decoupled from the apps, but aren't both stored on some kind of instances? Also:
> Why are we listening to the event stream if we're the one making the write? Because we're not the only ones making writes! There are lots of user repos generating events, and lots of apps writing to them!
Who is hosting this event stream? Aren't we making some kind of federated network by deciding on our app server which event streams or which users/apps pushing updates to listen to?
>Yes, the user data is decoupled from the apps, but aren't both stored on some kind of instances?
There are two main kinds of "nodes" in atproto:
- Hosting aka "personal data servers" (PDS). This is dumb JSON hosting that you can query by HTTP or watch by Websocket. Super cheap to run. They don't talk to each other. You can have one per user, or one per many thousands.
- Apps. These are your normal webapps. (But they ingest data from everyone's hostings.) They also don't talk to each other.
So yes, there are "instances" in the sense of "boxes which run software" but the topology is completely different from Mastodon or such. Data flows from hosting into apps (and then apps write to hosting). There is no hosting-to-hosting or app-to-app connection. Hosting is app-agnostic, and apps are hosting-agnostic.
To make all of this practical, there are things in the middle that make the situation easier for app developers — either relays (which combine event stream from many hostings), or caches like Hubble[1] and Constellation[2] (which let you query the entire network in one request).
>Aren't we making some kind of federated network by deciding on our app server which event streams or which users/apps pushing updates to listen to?
Ideally you would listen to every relevant event from the entire network (and filter out every irrelevant one). It isn't hard today — you can either use an existing relay or run your own for ~$30/month or pool with someone. The discovery mechanism is that (1) a hosting can request any relay to crawl it, and (2) a relay can discover more hostings it hasn't crawled yet by following links — similar to how Google crawls the web.
Lol reminds me of "ITS SERVERLESS!" Which always cracks me up, as someone who does find serverless useful for very strategic scenarios, naming things as though they don't require a computer somewhere to function has been one of the weirdest trends in tech.
The name "serverless" doesn't mean that there are no servers. It means that, as a developer, you don't need to manage the server. It's abstracted out for you.
I know what it means, I pitched serverless as a new tool to a former employer back nearly a decade ago, I had to thoroughly research it because the manager would of said no if I had no idea how it worked, funnily enough, he said yes before I could finish my entire pitch.
As far as I can tell the specification only demands the code modules (pixels) to be square (which is already often ignored in "aesthetic" QR codes which use e.g. round dots instead) and arranged in a square grid. Not that each grid cell has to be filled completely by the respective module. So this might actually be compliant!
Looks like this is definitely possible, the results aren't as clean as you might hope though. Maybe they could be improved by introducing some intentional errors (which were explicitly avoided here).
I think sampling "the whole square" might actually not be that good for decoding even standard QR codes as aliasing at the edges of each code module ("pixel" of the code) in a camera image would actually make the distincion between 1s and 0s more difficult.
Your argument still partially applies though, as introducing new unrelated colors at the module edges could also lead to aliasing effects when the code is too small for example.
Coincidentally came across this after reading a comment [1] under the recent post on _for-sale DNS records, visiting milk.com and scrolling through the owner's Mastodon
With the crucial difference that these processes deterministically return correct & working results (save for bugs which can be fixed and then stay fixed). Cannot be guaranteed for LLM output, no matter how much effort we put in.
I could not find any indication that the purpose of this ever-increasing spending (while alarming) is money laundering in the essay you linked. Can you provide any other source to back up this claim? Money laundering is illegal, while spending money in of itself is definitely not.
I'm generally critical of WMF and think (1) they waste significant amount of resources on mis-managed projects, and (2) are not very honest or transparent in donation communications.
But to play devils advocate, a lot of this depends on your views of what WMF should be. Some see WMF as "keep wikimedia sites up and healthy". But the foundation is much broader:
> The mission of the Wikimedia Foundation is to empower and engage people around the world to collect and develop educational content under a free license or in the public domain, and to disseminate it effectively and globally.
As an example, one of the hundreds of projects that WMF funds is the WikiPortraits Photo Service (https://photos.wikiportraits.org). Take this with a huge grain of salt, but Sol found ~$500K of direct grants in the past 3yr; with 50k Creative Commons or public domain portraits taken as a result.
Some people might be shocked at this, and feel scammed that some of their donation to WMF is funding photographer's hotels/flights/compensation to Cannes, Fifa World Cup, etc; instead of servers or infra or 'KOTL employees'.
Others might think it's an incredibly great use of money; at just $10/photo; while contributing novel, high-quality, human-authored, freely licensed content to the world
Yes, that is a good example. I used to be cynical about these uses of money until I met a 70-year-old volunteer who regularly attends international cycling championships to take pictures of the cyclists. She is totally devoted to documenting the sport and is not by any stretch of the imagination getting rich doing that or living in luxury. So I've changed my mind: her being able to do that is a good thing for her, for Wikipedia and for the sportspeople involved in these championships. YMMV.
WikiPortraits organizer here. That funding figure is through the end of 2027. I'd estimate ~$550k total from the WMF over 4 years (accounting for additional rapid grants and funding from affiliates). So looking at an overall average of ~$135k per year out of a ~$200 million budget to (so far in 2.5 years) engage 150+ photographers who have uploaded 90k+ photos from hundreds of events. Good downstream impact as well (developing better tools for Commons, bringing on more longterm contributors to both Commons and Wikipedia, etc.).
Also want to highlight that WikiPortraits is not just covering the fancy events like FIFA and Cannes, but many more smaller and undercovered events as well (indigenous festivals, science conferences, literature festivals, and so on). World Cup coverage in particular was relatively very cheap for how high-visibility the photos are on Wikipedia (majority of matches were covered locally); we've put more towards getting wiki photographers in Benin, Ghana, and Kenya support to cover their local culture and events.
For the amount of direct impact we have on Wikipedia and Commons, I'll go to bat to say that it's a good use of money compared to a good number of other projects that have received more funding over the years (ofc I have a conflict of interest here, but still). But I do get the larger point, that this sort of project is not necessarily what people expect when they donate to Wikimedia (and Cannes and FIFA of course stand out in the list of events being covered and are what people will focus on). And I've also been critical of the WMF's approach to donation comms for this reason.
That $500K over three years represents 0.08% of the foundation’s budget in that time period. The question is, what are they spending the other 99.92%? There is a significant small chunk spent on crucial infrastructure, but it’s mostly a slush fund for board pet projects.
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.
reply