I guess it's a fraction of problems on which a model produces a LEAN proof or a counterexample.

Wouldn't they just list the number of problems solved then?

	▲	dekhn 2 hours ago \| parent [-]
		rates beat counts almost always.