This benchmark is useless and should die. LLMs have likely trained on it, it's too easy to game by training specifically for it, & it doesn't mean much
1,914 karma · joined April 15, 2013
I don't think this applies, isn't this just the researcher using ChatGPT Codex on their machine?
Not all of society at all. Let's discuss this when AI is better integrated and a large fraction of people are laid off in 5 years.
It's very hard for them to claim the moral high ground here.
It's like stealing an apple from the British Colonial Empire.
I understand that there are users that would prefer another option, especially in the EU.
99.999% of people will agree that reducing software vulnerabilities is desirable if they're able to understand the question, including the bad actors themselves a lot of the times.
The situations like bad state actors are already not bound by laws, and things like keeping activism legal are better fought for through other ways
Your job or the LLM's job is to write code that Lean is satisfied with, creating the link between what you're trying to prove, and mathematical axioms.
If you write a bad proof, the Lean constraint checker will tell you, unless there are bugs in Lean itself, or you defined the goal constraint incorrectly.
Curiosity is good but maturity is trusting that the problem will get hard at some point anyways, that improving the most efficient way is usually also interesting and is more likely to deliver desired things on time or at all, which can be a big deal if what you're trying to deliver it worth it, like.. a new MRI machine that detects new types of cancers, etc.
If you don't care about what you're trying to deliver, that's another problem that requires at least some questioning, though I understand people have families to take care of etc.
no one talented will come pay taxes and make your nice tech companies carry the S&P500 and in turn, everyone's retirement funds, if you treat them like hogs