I did this for all theorems in
set.mm, and below are the 63 requiring > 8000 $p's. It looks like dirith uses the most in terms of $p count. I didn't save the extracted .mms, but re-running it on 3 of them,
dirith.mm has 6994793 bytes,
fouriersw.mm has 7026106 bytes, and
pnt.mm has 5665034 bytes. For comparison, the current
set.mm has
36616 $p,
2587 $a, and 39486525 bytes. BTW $a includes both |- and syntax statements, so the number of axioms and definitions is about half the $a count.
8019 $p 557 $a pntlemp
8024 $p 557 $a pntleml
8030 $p 620 $a dchrisum0flblem2
8032 $p 620 $a dchrisum0flb
8033 $p 559 $a areacirc
8041 $p 622 $a dchrmusum2
8049 $p 557 $a pnt3
8049 $p 596 $a meascnbl
8049 $p 600 $a coinflippvt
8051 $p 557 $a pnt2
8053 $p 557 $a pnt
8075 $p 596 $a omssubadd
8076 $p 560 $a etransclem23
8077 $p 616 $a dchrisum0lem2a
8080 $p 616 $a dchrisum0lem2
8114 $p 608 $a dstfrvclim1
8145 $p 624 $a dchrvmasumlem3
8149 $p 624 $a dchrvmasumiflem1
8172 $p 628 $a dchrisum0fno1
8187 $p 554 $a fourierdlem111
8237 $p 620 $a dchrisum0lem3
8244 $p 568 $a etransclem46
8248 $p 604 $a omsmeas
8271 $p 620 $a rpvmasumlem
8278 $p 552 $a fourierdlem103
8278 $p 552 $a fourierdlem104
8313 $p 562 $a stirling
8334 $p 564 $a stirlingr
8417 $p 554 $a fourierdlem112
8431 $p 630 $a dchrvmasumiflem2
8447 $p 640 $a dchrpt
8455 $p 574 $a etransclem47
8465 $p 554 $a fourierdlem113
8480 $p 554 $a fourierdlem114
8481 $p 554 $a fourierdlem115
8482 $p 554 $a fourierclimd
8482 $p 554 $a fourierd
8483 $p 554 $a fourier
8483 $p 554 $a fourierclim
8483 $p 554 $a fouriercnp
8484 $p 554 $a fouriercn
8486 $p 554 $a fourier2
8498 $p 632 $a dchrvmasumif
8517 $p 574 $a etransclem48
8542 $p 576 $a etransc
8563 $p 556 $a fouriersw
8595 $p 654 $a sumdchr2
8603 $p 654 $a dchrhash
8604 $p 654 $a sumdchr
8641 $p 658 $a sum2dchr
8653 $p 684 $a sitgaddlemb
9313 $p 678 $a rpvmasum2
9331 $p 678 $a dchrisum0re
9428 $p 682 $a dchrisum0
9429 $p 682 $a dchrisumn0
9429 $p 682 $a rpvmasum
9430 $p 682 $a dchrmusumlem
9430 $p 682 $a dchrvmasumlem
9431 $p 682 $a dchrmusum
9431 $p 682 $a dchrvmasum
9502 $p 684 $a rplogsum
9505 $p 684 $a dirith2
9506 $p 684 $a dirith
Norm