Interesting. That's a lot lower than my estimate. I kinda agree that what I said is pretty abstract though. Clearly, there are academics working with proof engines that have a shaky grip on the definitions of the various fallacies, or maybe they just don't care much and saw a dataset they could optimize for that industrial labs were likely to ignore (I suspect the latter).