The contamination framing is a proxy for a deeper problem: we have no tools to track the provenance of ideas in model weights.
OpenAI saying they "cannot rule out" training on user data isn't a hedge. It's an accurate description of the epistemic situation for anyone in their position. Current interpretability methods can't answer questions like "did this proof technique originate from training on Session X?" The ideas in a model's weights don't have clear lineage -- they're smeared across millions of examples in ways we can't localize. This is different from citation in human research, where influence is presumed to flow through legible chains (reading, citing, corresponding). In a trained model, the nearest equivalent to "you read their work" is undetectable.
Lean makes this worse, not better. It verifies that the proof is correct, but provides zero information about its intellectual genealogy. So OpenAI now has a proof that is formally verified and provably mysterious about its origins. The "we cannot rule it out" statement is the honest answer, but it's also an answer that can never become more certain in either direction with current tools.
The researchers are pointing at something structurally new: the normal academic attribution apparatus depends on influence being legible. If AI intermediaries can soak up ideas from private conversations, synthesize them, and produce outputs that are formally correct but intellectually unattributable, we don't have norms for that situation yet. This specific case may or may not involve misconduct. But the structural problem it reveals exists independently of OpenAI's behavior.