Why isn't Isabelle/HOL being used for LLM theorem proving (like the OpenAI 10 theorems from last week)?

I am asking because I find Isabelle/HOL easier to read and understand (and I suspect that would make it easier to work with for LLMs too).

Like a lot of lay people/non-mathematicians, I am trying to get my head around today what are the key concepts in the 10 OpenAI proved theorems from last week, so I figured if the key concepts (not the actual proofs themselves) were converted into Isabelle instead it might help(??).

Has anyone here that actually is a mathematician started on an effort like that?