Maybe it could happen partially, but cryptomining has the advantage that it can adapt to the power available and barely needs any IO, so if there is a single oil well in the middle of nowhere you could use the natural gas for mining instead of flaring it.
I think AI wants large centralized data center with really good internal network.
I think a logic language is not a great fit, because it deals in absolute truths. Whereas news and non-fiction articles are more someone said something and they are usually reliable except in this particular domain where they can be a bit biased sometimes. Also the people they interviewed may have misremembered. Etc etc.
You could argue that all such things could in principle be modelled in logical formulas but... it would be way more complicated than the stated model.
On the other hand it's also unclear what the logical model actually adds. Usually logical formulas are used because they can be manipulated, and inferences can be drawn. But drawing logical inferences from sorta-kinda true statements can quickly become muddy and lead to false conclusions if you don't take into account the uncertainty of the statements.
The person suggesting it had simple heuristics like "this proposition was asserted by three sources". This has obvious flaws (e.g. I can cite three lying sources). But even on Wikipedia, there is no automatic checking that sources say what's claimed. So it wouldn't be useless despite having obvious flaws.
But anyway, if you have heuristics like this you can make them propositions and do inference with them. Instead of thinking of it as "I've proved this false" or "the citations are correct" perhaps think of it more like a lint that runs against your code base and tells you whether you've done something that falls below expectations.
A more natural way to model it would be something like a Bayesian system where you assign probabilities, build up a hierarchical model, and flow probabilities through the model. But there's something nice about a simpler system that doesn't pretend to do more than it can.
You can certainly build up a collection of probably-true-statements. That makes sense. Encoding them as logical formula makes sense. That's basically what you are describing. But OP wanted to then additionally put those formula into Lean, and that's where I disagree. Because he will likely have inconsistent statements in his collection and then he can prove all sorts of absurdities (principle of explosion).
So IIUC like if an article is covering a debate, 3 sources assert "A", and another 3 assert "~A", then the heuristic "3 sources assert means it's true", gives you a logical setup with "A ^ ~A"?
If so, then yes that's a bug in that heuristic. Like I said in my first comment, what OP is describing is impossible the way they're describing it. So I think in that sense we're in agreement.
But on the other hand, maybe OP will end up hacking together a thing that resembles probabilistic modal logic.
At the time I wrote that comment OP was being downvoted and there were no encouraging responses, which I felt wasn't representative of the math community as I know it. Now there is a good discussion of the problem space and some suggestions to check out different kinds of logic, so I'm glad to see all that going on!
Well chatgpt doesn't know if there will be a follow-up question relying on the "irrelevant" information. So in general it can't remove it. Or at least it would require some more complexity to dynamically decide what is relevant and not over the lifetime of the conversation.
Apparently serving HTML + other static content is more expensive than ever, probably because people go the most expensive routes for hosting their content. Then they complain about bots making their websites cost $100/month to host, when they could have thrown up Nginx/Caddy on a $10/month VPS and basically get the same thing, except they would need to learn server maintenance too, so obviously outside the question.
1. non-humans can create much more content than humans. There's a limit to how fast a human can write, a bot is basically unlimited. Without captchas, we'd all drown in a see of Viagra spam, and the misinformation problem would get much worse.
2. Sometimes the website is actually powered by an expensive API, think flight searches for example. Airlines are really unhappy when you have too many searches / bookings that don't result in a purchase, as they don't want to leak their pricing structures to people who will exploit them adversarially. This sounds a bit unethical to some, but regulating this away would actually cause flight prices to go up across the board.
3. One way searches. E.g. a government registry that lets you get the address, phone number and category of a company based on its registration number, but one that doesn't let you get the phone numbers of all bakeries in NYC for marketing purposes. If you make the registry accessible for bots, somebody will inevitably turn it into an SQL table that allows arbitrary queries.
i run a small wiki/image host and for me it's mainly:
4. they'll knock your server offline for everyone else trying to scrape thousands of albums at once while copying your users' uploads for their shitty discord bot and will be begging for donations the entire time too
If a time_t is used for context and the int64_t is then downcast to int32_t that could be hard to catch. Maybe you would need some runtime type information to annotate what the int64_t actually is.
Null means nothing, zero. In the context of scientific articles a null result means that the difference is zero. What difference? Well it depends. It could be difference between doing something and not doing it. The difference between before and after some intervention. Or perhaps the difference between two different actions.
In this case the difference between before and after raising the minimum wage.
Furthermore, the thing with a null result is that it's always dependant on how sensitive your study is. A null result is always of the form "we can't rule out that it's 0". If the study is powerful then a null result will rule out a large difference, but there is always the possibility that there is a difference too small to detect.
Null means something doesn't exist and proving something doesn't exist can at times especially in certain sciences be as valuable as proving something does exist. Especially if it stops the rest of the field chasing the pot of gold at the end of the rainbow.
I think AI wants large centralized data center with really good internal network.