Good idea, the problem is that LEAN only proves what you tell it to prove. Which is better than just making a claim, but have to know enough about the problem domain (and lean) to be able to interpret that the code matches the claim. Otherwise you can be proving something only tangentially related. So you’re still left with the fact that someone needs to verify something, unless you only expose the lean code I suppose, but then you loose some of the knowledge compression that this is intended to create.