« BackLean theorem prover mathlibgithub.comSubmitted by downboots 2 days ago
  • fjfaase 17 hours ago

    I see a lot of maintainers specialized in topology and category theory, but non in graph theory. I wonder if this is also reflected in the areas that are covered by the library.

    • caladin 2 days ago

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

      • giltho 2 days 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 a day 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-...

          • undefined a day ago
            [deleted]