briantrumpet
Timewaster
Prize to anyone who can make baked beans do that.
Drax datacentre could create nearly twice the yearly emissions of all Gatwick flights
Drax’s planned datacentre could produce nearly double the emissions of all flights out of Gatwick airport each year by burning 4.9m tonnes of wood annually, an analysis has shown.
Not surprisingly, Alex Harvey (human) is more than a little pissed off by Amazon and their 'Andrew V. Smith' AI creation.
View attachment 17638
Haha. And then he thinks this makes it better. Maybe his wife could replace him with a turkey baster if she wants any more children.
View attachment 17644
I suppose I'd be wasting my time trying to convince him that from the child's perspective that time spent reading stories is very valuable, precious, and not wasted time in any way or form. I think it says a lot about him. Yeah, use the baster instead of the waster.
Autoformalisation is increasingly used to verify mathematical texts, including those generated by AI, as in OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations. In this process, an AI system translates the text from a natural language (NL) into a formal language such as Lean. Once this translation is done, the argument expressed in the formal language can easily be mechanically verified. The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully. In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation, is arbitrarily high up in the Solvability Complexity Index (SCI) hierarchy/arithmetical hierarchy (the SCI =∞). Hence, informally, providing semantically faithful AI autoformalisation is harder than any computational problem including the Halting problem (which has SCI =1). To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean `verifications'. These include OpenAI's announced Navier-Stokes proof. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.
I'm sceptical. Factoring large numbers is a difficult for an AI as it is for any software based on conventional processor technology. Might be these vast data centres are so stuffed full of processors it becomes faster but at significant expense.Just read a news report that AI super mathematics will soon be powerful enough to break down all encryption on the net. This includes the blockchain which holds up all cryptocurrencies.
I'm sceptical. Factoring large numbers is a difficult for an AI as it is for any software based on conventional processor technology. Might be these vast data centres are so stuffed full of processors it becomes faster but at significant expense.
The risk to widespread encryption comes from Quantum computers but even then there are steps to safeguard using structured lattices and hash maths which is hard for quantum computers as well ss conventional processors) to solve (post quantum encryption).
I'm sceptical. Factoring large numbers is a difficult for an AI as it is for any software based on conventional processor technology. Might be these vast data centres are so stuffed full of processors it becomes faster but at significant expense.
The risk to widespread encryption comes from Quantum computers but even then there are steps to safeguard using structured lattices and hash maths which is hard for quantum computers as well ss conventional processors) to solve (post quantum encryption).