Comment by schleck8
15 hours ago
> 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?
15 hours ago
> 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.