601–610 of 1001 posts
Earlier quoted context omitted.
it is very hard for people to eat crow, as the replies will show
Really? has anyone ever claimed that ai will never be able to prove theorems and conjectures ?
i can link you likely dozens of comments from people wrong about this replying to me over the last 5 years
Earlier quoted context omitted.
> The most interesting question to me is what will be consumed by the exponential like math seems to be undergoing, and what won’t. Writing has been quite stubborn, isn't it clearly split between verifiable not verifiable ? what is interesting about that question.
I do not think it is so clear. Programming has verifiable and non-verifiable aspects. Competitive programming, passing tests, and performance can all be verified. But translating English requirements into actual software, software architecture, taste, or UI design cannot. And yet over the last couple years we’ve seen huge lifts in all of these areas, not just the verifiable ones. Verifiable areas I think are clearly…
This is _much better_ data than 1/0 verification, it is as good as a gradient.
Automatically verifiable tasks improve faster since well, its automated.
Earlier quoted context omitted.
I understand your sentiment, but I think this really is something different. This isn’t a craft going away, or even an industry being replaced, it’s potentially everything we do. It’s the ground being pulled away beneath people’s feet, everyone, everywhere all at once. I think the vacuum it leaves in people’s lives needs to be filled with something, and I haven’t heard any good ideas about this or how the transition…
There is a glaring fallacy in your “AI will change everything as it is super intelligent” hypothesis. If it is so great thinker which can do everything why not just solve this social impact thingie? Or maybe it is not so capable?
The GitHub repo with the Lean formalizations just came out a couple of hours ago: https://github.com/openai/ten-proofs It also links to a paper written by an LLM where the model "reconstructs how the proof came together" based on the unpublished reasoning traces: https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf I wish they'd publish the prompts though!
I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications) that the lean proofs are checked against. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.
People argue whether we are at y-5, y, or y+5, meanwhile we seem to be on a y=2^x exponential that keeps delivering more and more impressive results. The most interesting question to me is what will be consumed by the exponential like math seems to be undergoing, and what won’t. Writing has been quite stubborn, but I’ve noticed Fable to be quite a big step up there. How about politics? Will we develop new ways to let…
>Will we develop new ways to let people express their own values in democracies, or will we just get much better at manipulation? Is there even the tiniest reason to suspect that the people steering this progress will use it for the democratic good of all?
I feel increasingly anxious reading this. Machine research shouldn’t be merged into mainline of human knowledge.
When you can formalize it in Lean or some such, why would this be? I can understand the desire to separate out other forms of research from the human corpus. But theoretical math that is decidable/provable, I’m not sure I see the risks.
Earlier quoted context omitted.
Ask DraftKings?
You'd need this argument to be a lot more concrete as to why AI is like gambling.
But I don't think the argument needs to be "AI is like gambling". The argument only needs to be "humans often behave irrationally and even self-destructively".
Earlier quoted context omitted.
Solving math problems doesn’t require the cooperation of rival factions.
It's a tad petty, no? In the end, the contribution to a healthier society leads to more for the companies contributing.
Earlier quoted context omitted.
> We are now at the point where RSI is feasible What can be asserted without evidence can also be dismissed without evidence. - Hitchen's Razor
The evidence is abundant and nearly impossible to ignore without increasingly focused effort.
I'm enjoying learning about these hard problems, but this line about credit made me chuckle: > We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness Offering to take responsibility for the correctness of a proof written in Lean feels like volunteering to be the fall guy in case someone finds a flaw in basic arithmetic, no?
I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications), that the lean proofs are checked against, indeed correctly encode the real theorems. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.