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.
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?
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.
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).
If their platform allows any kind of processing as it sounds then anyone could just dump the data. So I don't see why they would not allow downloads for local processing.
Reading between the lines, I assume they aren't reasonably capable of serving up ~TB scale data to hundreds (thousands? more?) of separate clients per day. The usual fix for this would be something like an AWS requester pays bucket.
To your question specifically, in such a scenario they would charge an obscene amount for the bandwidth so you would be strongly incentivized not to download hundreds of GB of data from them.
The questions is, how much are you willing to pay (because the cost of this is not free, especially in this cloud era), and what is the scientific return for access to the uncalibrated data? There is significantly more value in a well designed pipeline for everyone (which is where anyone who would work on the pipeline would slot in) than bespoke pipelines which are poorly built and unmaintainable.
> It is quite sad, that we have a choice of enshittifaction and radicalization only (...)
Maybe this is a question of point of view? I find github's stance on slop extremely radical (and totally contrary to my own values). At the same time, github is obviously enshittified, so I don's see the point in using it anymore.
You still have gitlab, which is some kind of middle ground. And if you only need to store private config files, you can host a private instance of forgejo--or a bare git repo--for much less than a sourcehut subscription. I hope you find your place! (still, I'm curious why your config files are AI slop, but that is another subject)
It just sucks having to pick between two extremes.
I moved to SourceHut from Github when their site stopped functioning without a JITed JavaScript engine or when you block certain AI elements. The bloat just got insane. Now it seems like I have to move again since SourceHut moved too far in the other extreme by embracing "minimalism" not only of their service but also of their users.
> you can [self-]host
I used GitHub and then SourceHut precisely so I don't have to do this.
For a simple reason - I may one-shoot an emacs function (or several) I need for my config with claude. So, it is technically slope. I am also against self-hosting - I don’t have time and patience for it. IT is not a valuable hobby for me anymore, with LLM or without.
Just to add a datapoint to the discussion: as a paying customer of sourcehut I 100% support this anti-slop policy. I'd prefer if some terms were stated somewhat more precisely, but it's great as it is.
> a practical, albeit incomprehensible, algorithm for solving NP complete problems.
It would not not necessarily be practical, even if it ran in polynomial time. It may have cost O(n^c), with a totally out of order exponent like c=A(5,5) or whatever.
This may very well be the most epic post in HN history.
EDIT : I recall fondly algorithm D... one of my first programming experiences in the 90s was trying to implement knuth's arithmetic algorithms for addition, substraction, etc. in 8086 asm. Got them right up until long multiplication (that one was a tremendous effort). Algorithm D was too formidable to even dare me attempt. Feel extremely happy to see people in 2026 looking at these algorithms closely.
my favourites are sourcehut (that has excellent ci, and does not try to be a github clone) and codeberg (with slightly more straightforward migration path from github)
I'd guess the technically correct answer to this question is "yes". But sourcehut has very good mailing list support, that is essentially equivalent to github pull requests.
Still, I find the wording of your question a bit prejudiced... as if I asked "does github still require pull requests via a proprietary interface instead of just sending the patches?"
The specific wording sounded a bit judgy to me as well, but I think it's a totally reasonable question. They're just asking about the capability of a product.
It is prejudiced. If you like sending patches over email more power to you, but there’s a reason 99% of the world’s devs does not follow that workflow.
Email was always designed for human to human messages. Patch files need strict formatting (like anything that needs to be machine readable). That means you need to install extra tools, point them at your mail server, configure the mailing list address and proper formatting for each project, then find the right commit range and type in the description into a command line editor every time you send a patch series. The alternative is doing everything manually and that takes even more effort.
Compare that with GitHub where the workflow is push changes to fork, select branch, click to create a PR, write the description in a convenient web form and submit. Less friction and less opportunities to mess up. The solution to a centralized forge is a decentralzied forge, not no forge.
Feels like you make the email workflow sound more complicated than it is on purpose. One could do that with the PR workflow as well.
The email workflow has features that GitHub doesn't have. Most people do without them and don't really feel a need to learn about them, and that's fine. But would Linux be better off with GitHub? Not sure.
> Before GUIs, interacting with a computer was limited to strange terminal commands [...] Even though the strict syntax has been replaced with natural language
This post, and particularly the two quoted sentences, has activated anger pathways in my brain that I didn't know existed... An extremely visceral, primary, response. I find it unbelievably jarring to read.
I know what you’re referring to, and after you said this I noticed the gui’s little control palette. I watch the user click this palette and then have to click the text palette to type a command.
And my mind sympathetically found this extra click offensive. Haha. One extra click and I got there. Hehe
Are you talking about your phone here?
reply