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.
This probably looks like contributing Lean code to an open source project and writing docs.
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: