Comment by bobmarleybiceps
1 day ago
I feel like at a certain point, there's is not necessarily a reason to go through the peer review publication process for some AI proofs.
Not because "ai bad," but because at some point AI outputs should probably just be treated like public knowledge. Specifically stuff that's provable by "AI please output lean showing X is true," where anyone could kind of reach the same conclusion by asking ai.
You don't want people to have to rerun the prompt though. Collaborating on a registry for proven results makes sense.
This probably looks like contributing Lean code to an open source project and writing docs.
Yeah, I don't disagree with a registry. Especially for problems that are important to humans or are expensive for AI to prove/disprove. I partly just want to avoid a situation where the volume of hard-to-search-for results that are easily-ai-proved/disproved skyrockets...
Basically, I think that for some stuff running a prompt is (or could become) easier than trying to do a search for an existing result. Partly why I think if something is fairly easily ai-proven, it should kind of be treated like it was already known, even if it wasn't actually known. :shrug: