Lean theorem prover mathlib

(github.com)

71 points | by downboots 15 hours ago ago

3 comments

  • caladin 4 hours ago ago

    Anyone know what kinds of jobs might use lean? Or jobs that are in a related space?

    • giltho 4 hours ago ago

      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 3 hours ago ago

      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-...