[HN Gopher] The Mechanics of Proof
       ___________________________________________________________________
        
       The Mechanics of Proof
        
       Author : segfaultbuserr
       Score  : 19 points
       Date   : 2024-03-19 21:23 UTC (1 hours ago)
        
 (HTM) web link (hrmacbeth.github.io)
 (TXT) w3m dump (hrmacbeth.github.io)
        
       | ufferop wrote:
       | I much prefer this resource over the official offerings.
       | 
       | https://lean-lang.org/theorem_proving_in_lean4/title_page.ht...
       | 
       | 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.
       | 
       | This resource also has its code online:
       | https://github.com/hrmacbeth/math2001/tree/main/Math2001
       | 
       | One major ommission from TFA is lean's built in package manager
       | and package builder lake: https://lean-
       | lang.org/lean4/doc/setup.html#lake
        
       | jml7c5 wrote:
       | See also the Lean Game Server at https://adam.math.hhu.de/ , and
       | in particular the "Natural Number Game" (for Lean 4!), which has
       | done the rounds on HN a few times.
       | 
       | Does anyone know of a Lean book that builds up the basics from
       | absolutely nothing, not even the Lean standard library? I'm
       | curious about the foundations that lie just above the language.
        
         | ykonstant wrote:
         | Your best bet lies with the introductory Functional Programming
         | in Lean: https://lean-lang.org/functional_programming_in_lean/
        
       | derbOac wrote:
       | One thing that's always been a little unclear to me is this:
       | 
       | With proofs, I normally think of the "work" 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.
       | 
       | In the examples I usually see for using something like Lean,
       | there's a true statement given, and the question is how to prove
       | it. Although there are reasons this could be interesting, it
       | doesn't seem quite as valuable as deriving some truth statement
       | that wasn't previously known to be true.
       | 
       | Can something like Lean be used generatively, to generate
       | multiple true statements given a set of assumptions?
        
       ___________________________________________________________________
       (page generated 2024-03-19 23:00 UTC)