Comment by skybrian
1 day ago
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.
1 day ago
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: