Why not? One can surely use math even if they have no clue about how to prove theorems. I suck at math, but I use it every day, without knowing how to advance it.

I think it might be fair to say that a proof cannot be without value if it proves something meaningful to a human, that a human can use somehow? But such proof probably doesn’t belong in a library seemingly explicitly dedicated to human-graspable proofs. Just because it violates the intent.

It’s not like such proofs mustn’t exist at all.