Comment by lionkor
15 hours ago
Can someone who is more into math or AI explain why so many people are so incredibly excited about this?
If OpenAI started opening hundreds of PRs on long-open issues on popular open source projects, would we rejoice, or would the first reaction be "they are unreviewed, so slop until proven otherwise" (it would be that).
I cannot possibly see how these are so impactful, especially the ones that don't come with lean proofs.
LLMs have the ability to make millions of mistakes per day, whereas humans can only make so many. How are we suddenly all so confident that there's no extensive hallucinations or "gaming the system" going on?
> How are we suddenly all so confident that there's no extensive hallucinations or "gaming the system" going on?
What would that look like for the proofs that have lean attached?
I said "especially the ones that don't come with lean proofs", but even for those with lean attached, lean is software, it has over 1k open issues, and I would not put it past an LLM to identify a bug and exploit it to pass the gate.
"I still don't like AI, and I'm 'just asking questions'."
I use AI every day, for hours, and it's not because someone is forcing me to.
Asking questions is reasonable when these tools are so very fallible.