[HN Gopher] How to (actually) prove it - New Frontiers of Mathem...
       ___________________________________________________________________
        
       How to (actually) prove it - New Frontiers of Mathematics and
       Computing in Lean
        
       Author : gopiandcode
       Score  : 50 points
       Date   : 2025-05-09 01:00 UTC (2 days ago)
        
 (HTM) web link (kirancodes.me)
 (TXT) w3m dump (kirancodes.me)
        
       | gnulinux wrote:
       | I personally prefer Agda to Lean or Coq [1] to prove my theorems
       | but this frontier is imho among the most exciting research in
       | theoretical CS in many many decades. I really wish more
       | programmers and mathematicians knew about automated theorem
       | proving and automated reasoning. It's nothing short of
       | revolutionary and I think next generation of pure mathematicians
       | will use these as a crucial tool in their research.
       | 
       | [1] It's a personal preference but Agda is simply a much better
       | language with almost limitless metaprogramming which allows me to
       | write proofs close to as they'd appear in prose math papers. It
       | has a smaller ecosystem though. I've never seen a proof in any
       | other language I personally didn't think would be much more
       | readable/simpler in Agda.
        
         | IngoBlechschmid wrote:
         | I'm currently creating an interactive tutorial on Agda, with
         | lots of embedded exercises (running purely in the browser/on a
         | server, no installation required), perhaps it is useful to
         | some:
         | 
         | https://lets-play-agda.quasicoherent.io/
        
       | sega_sai wrote:
       | Interesting. I always wanted to try Lean, and personally never
       | found an easy way to do it, as it requires installing a plugin in
       | vscode, create a project or reading the lean book. But following
       | the links I've found this nice interactive tutorial for proving
       | 2+2=4 in Peano arithmetic:
       | 
       | https://adam.math.hhu.de/#/g/leanprover-community/nng4/
       | 
       | It's quite instructive.
        
         | thechao wrote:
         | Ironically, the website broke, and became stuck on the
         | "rw[one_is_succ_zero]" rewrite rule, continually telling me
         | that "rfl" isn't valid. Sigh.
        
         | gfaster wrote:
         | Lean is more complex to develop in than most programming
         | languages since it relies heavily on interactive programming,
         | i.e. the context pane. The "easy way" is with a plugin.
         | 
         | If you're interested in learning more about Lean for writing
         | proofs, I would recommend The Mechanics of Proof [0]. It strips
         | out a lot of the convenience tactics in Mathlib to focus on the
         | more primitive mechanisms Mathlib builds on.
         | 
         | [0]: https://hrmacbeth.github.io/math2001/index.html
        
       ___________________________________________________________________
       (page generated 2025-05-11 23:01 UTC)