&gt; it can come off really bad if you approach them and ask them to explain it to you so that you can understand it in a fraction of the time<p>But it works like that with software libraries. Even if they are the product of arduous work, they should come with documentation, examples, introductory material. Why should proofs be any different?<p>The Curry-Howard isomorphism should apply to documentation, too!