The four-color theorem appears to be case C. That was the first really long computer-assisted proof. No one has since found a concise way to do that proof, and it's been half a century now.

I'm not sure how Terence Tao's "digestion" concept holds up if the upcoming AI math results are all like that. It would be almost like humans are chewing bones under the table, while LLMs are feasting.