[HN Gopher] Lean theorem prover mathlib
       ___________________________________________________________________
        
       Lean theorem prover mathlib
        
       Author : downboots
       Score  : 74 points
       Date   : 2025-12-14 01:49 UTC (18 hours ago)
        
 (HTM) web link (github.com)
 (TXT) w3m dump (github.com)
        
       | caladin wrote:
       | Anyone know what kinds of jobs might use lean? Or jobs that are
       | in a related space?
        
         | giltho wrote:
         | Beyond academic research, a non-exhaustive list of people using
         | either Lean or related tech:
         | 
         | - Amazon (where they even hired the creator of Lean to pursue
         | this)
         | 
         | - Microsoft (mostly cryptography but also other stuff) - ARM
         | (hardware verification)
         | 
         | - Apple (hardware verification, that I'm aware of)
         | 
         | - Lots of companies verifying things for blockchain
         | technologies if you're into that
         | 
         | - More specialised companies, e.g. Galois Inc.
        
         | griffzhowl wrote:
         | You could have a look at the job postings on the Lean zulip
         | chat. They're mainly on the academic side, though
         | 
         | https://leanprover.zulipchat.com/#narrow/channel/284757-job-...
        
       ___________________________________________________________________
       (page generated 2025-12-14 20:01 UTC)