The Mechanics of Proof

One thing that&#x27;s always been a little unclear to me is this:<p>With proofs, I normally think of the &quot;work&quot; as being in the derivation of a statement that is shown to be true. That is, the value is in deriving a new true statement that was not previously known to be true.<p>In the examples I usually see for using something like Lean, there&#x27;s a true statement given, and the question is how to prove it. Although there are reasons this could be interesting, it doesn&#x27;t seem quite as valuable as deriving some truth statement that wasn&#x27;t previously known to be true.<p>Can something like Lean be used generatively, to generate multiple true statements given a set of assumptions?

I much prefer this resource over the official offerings.<p><a href="https:&#x2F;&#x2F;lean-lang.org&#x2F;theorem_proving_in_lean4&#x2F;title_page.html" rel="nofollow">https:&#x2F;&#x2F;lean-lang.org&#x2F;theorem_proving_in_lean4&#x2F;title_page.ht...</a><p>You may need to use them in tandem, but I have found it much more productive to jump to the “number theory” section of TFA then to step through the official resource.<p>This resource also has its code online: <a href="https:&#x2F;&#x2F;github.com&#x2F;hrmacbeth&#x2F;math2001&#x2F;tree&#x2F;main&#x2F;Math2001">https:&#x2F;&#x2F;github.com&#x2F;hrmacbeth&#x2F;math2001&#x2F;tree&#x2F;main&#x2F;Math2001</a><p>One major ommission from TFA is lean&#x27;s built in package manager and package builder lake: <a href="https:&#x2F;&#x2F;lean-lang.org&#x2F;lean4&#x2F;doc&#x2F;setup.html#lake" rel="nofollow">https:&#x2F;&#x2F;lean-lang.org&#x2F;lean4&#x2F;doc&#x2F;setup.html#lake</a>

What is going on in the third example?<p>&quot;Let a,b,m,n be integers, and suppose that b^2 = 2a^2 ...&quot;<p>So, (b^2)&#x2F;(a^2)=2 b&#x2F;a = sqrt(2)<p>or, in other words, sqrt(2) is rational. then it goes and uses this in the rest of the example.

Some mathematicians are afraid of being censored or only becoming mechanics.<p>&quot;What some people like to call the progress of mathematics has always consisted in the subversion of paradigms. Pierre Deligne made this point in a lecture on Voevodsky’s univalent foundations: he said it reminds him of Orwell’s Newspeak, where the ideal was to have a language where it is impossible to express heretical thoughts.&quot;<p><a href="https:&#x2F;&#x2F;siliconreckoner.substack.com&#x2F;p&#x2F;the-central-dogma-of-mathematical" rel="nofollow">https:&#x2F;&#x2F;siliconreckoner.substack.com&#x2F;p&#x2F;the-central-dogma-of-...</a>

See also the Lean Game Server at <a href="https:&#x2F;&#x2F;adam.math.hhu.de&#x2F;" rel="nofollow">https:&#x2F;&#x2F;adam.math.hhu.de&#x2F;</a> , and in particular the &quot;Natural Number Game&quot; (for Lean 4!), which has done the rounds on HN a few times.<p>Does anyone know of a Lean book that builds up the basics from absolutely nothing, not even the Lean standard library? I&#x27;m curious about the foundations that lie just above the language.

Anyone who wants to learn more about the calculational proof style as it applies to computing science would do very well to read Dijkstra.