> How are we suddenly all so confident that there's no extensive hallucinations or "gaming the system" going on?
replyWhat 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.
reply"I still don't like AI, and I'm 'just asking questions'."
replyI use AI every day, for hours, and it's not because someone is forcing me to.
replyAsking questions is reasonable when these tools are so very fallible.