What is the unit for productivity here, though? Time required to complete this one task, which was never attempted before and never will be again? That's fine, but economically uninteresting.
Ultimately, the economic analysis needs to use monetary units. How much faster can return on investment be realized, and at what scale? This analysis has proven elusive because people believe that the very definition, not just the execution, of a task can be delegated to an LLM (which in some trivial sense must be true because means and ends are never sharply distinguished).
Well, the point of the _computer_ formalization is that it's checkable.
An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.
All that needs to be checked to avoid that is the statement of the main theorem. Any divergence further inside means you proved the main theorem differently than you thought you did -- but you still proved it.
This assumes the Lean kernel itself isn't bugged, but getting it correct is a matter that affects all uses, not just this one, so the cost of making it correct is spread over all those uses.
In general checking that the definitions are correct isn't that hard and assuming at least one of the lean kernels you verify with is correct (which tbf is an assumption, the implementations are based on each other so could have a common bug) that's all you need to verify.
In this case the statement is unusually complicated but still much much easier to verify than the proof itself.
So, the specification of the theorem we are fairly solid on, formalising what a group is, and a simple group, have been done a long time and we are confident in the correctness of.
Assuming you do trust those, then assuming the formalisation passes lean (and lean has no bugs!), then the whole idea is you've got a proof of the theorem.
The papers describing lean and it's core operations are deliberately small. The kernel of a theorem prover is meant to be such that a human can check it for correctness. The kernel does not include things like type inference or execution. It literally checks the proof and that's all and everything needs to match exactly. It's fairly trivial to write such a thing.
Humans have to establish trust in this.
After that, the rest of the language is written. Yes it is possible the type inference engine is broken but in that case the kernel will reject it
I think the OPs argument (which I am not endorsing) is that they in fact enjoy a higher quality of life even if their "standard of living" (measured in purchasing power) is higher.
It's all subjective though. Asking most in a 'developed' country whether they'd trade their high rent for a dirt floor/house would result in an affirmative no. Same for health/insurance - "Would you trade your high premium for 'the nearest so called doctor is a days walk away'" is going to be a resounding no.
But then it's the same the other way around "Would you trade your dirt floors for linoleum if it meant you hard to do hard labor 40 hrs a week?" and "Would you trade your witch for the luxury of owing the doctor thousands of hours of labor?" would both also be resounding nos.
I know there is a growing contingent of those moving off of the grid and spurning modernity for log cabins built by hand, and the converse OLPC in dirt huts thing but for the most part everyone everywhere wants to have their cake and eat it too.
"The Electric Monk was a labour-saving device, like a dishwasher or a video recorder. Dishwashers washed tedious dishes for you, thus saving you the bother of washing them yourself, video recorders watched tedious television for you, thus saving you the bother of looking at it yourself; Electric Monks believed things for you, thus saving you what was becoming an increasingly onerous task, that of believing all the things the world expected you to believe." - Douglas Adams
When the test code "looks like a mess", how do you get assurance it is testing the right properties?
Like you, I've found that LLMs can improve test coverage by decreasing the amount of developer time spent writing tests. But generally, it takes a lot of manual work to set up the initial testing framework, and even then, a lot of vigilance to ensure that what is actually tested corresponds to the description of the test.
Their alternative explanation seems, uh, pretty sensible to me?
"On the other hand, cybersecurity practitioners have largely viewed these incidents as consequences of companies failing to adopt basic security precautions. They do not see the incidents as a sign of AI reaching a new milestone in cybersecurity. This is also the dominant reaction in the tech community outside AI, which has largely treated the incidents as a result of ineptitude and negligence by AI companies."
"The contemporary rate of extinction is estimated at 100 to 1,000 times higher than the natural background extinction rate—the typical rate of species loss through natural evolutionary processes."
"People weren't their strongest even when most did manual labor."
Is there good historical data on some measure of strength across representative populations over time in the modern era? I'm doubtful.
We do know that the introduction of agriculture diminished strength:
"Bone mass was around 20% higher in the foragers - the equivalent to what an average person would lose after three months of weightlessness in space.
After ruling out diet differences and changes in body size as possible causes, researchers have concluded that reductions in physical activity are the root cause of degradation in human bone strength across millennia."
Ultimately, the economic analysis needs to use monetary units. How much faster can return on investment be realized, and at what scale? This analysis has proven elusive because people believe that the very definition, not just the execution, of a task can be delegated to an LLM (which in some trivial sense must be true because means and ends are never sharply distinguished).
reply