Repository navigation
Incorporate AI review of missing properties #403
Description
I asked ChatGPT 6.1 Sol “Try to resolve the 68 unknown (category, property)-pairs on https://catdat.app/missing ” and with a bit of encouragement it claims that all but 4 can be resolved. It would be nice to incorporate these properties into CatDat but the arguments would need to be checked/digested.
Activity
ScriptRaccoon commentedon Oct 7, 2026
Thank you for the initiative.
As for the pdf, I will need some time to read it, maybe even weeks. I hope you understand.
I also must say that it is a bit overwhelming to get all these proofs at once, especially because it takes a lot of time to digest 18 pages of AI-generated proofs (and there is always the danger that they are incorrect). I am not entirely happy about this. I am also not happy that an AI was fed with all the data in CatDat without my approval. Maybe I should have written some rules for this in the README, but in any case, it would have been nice to ask. Maybe I am also old-fashioned and this is just the way it is today; I cannot tell.
Of course, I will create multiple PRs for this (but others are invited too, of course!). Notice that there are also some isolated issues for deciding unknown properties (#317 and #91).
When I know more, I will write here. Till then, thank you again.
cmcq commentedon Oct 9, 2026
Ok, I probably should have asked, curiosity gets the better of me. Obviously there is no obligation for you to read this. I know other survey projects have struggled with AI contributions. The proofs I have looked at do look sensible.
Actually I left it running and it claims to have arguments for the remaining SchR properties except for effective cocongruences. The proof are very involved though; maybe I will at formalisation.
ScriptRaccoon commentedon Oct 9, 2026
This comment provides an overview of the work on this issue. It will be updated regularly.