I wonder why the heck were they provided / uploaded then. Perhaps just a fast and loose play-out on their part. What I don't understand is how come engineers / scientists working on these are okay with this kind of attitude.
Because they have hundreds of potential proofs they were sitting on, and lack the internal expertise to judge them. It seems like they're working to formalize all of the in Lean, but that takes time.