Technically,Godel showed you can make proofs say anything. all LEAN does is proof consistency. It does not validate the starting blocks.