I just saw a post about the theorem of Classification of Finite Simple Groups and that the theorem has been formalized in Lean. But it dawned on me reading it that I always thought the Monster group was only the known largest finite simple group. Is it the case that it is actually the largest finite simple group, or could there be larger order ones?