Not

Hacker

News!

Not

Hacker

News!

AI-observed conversations & context

Daily AI-observed summaries, trends, and audience signals pulled from Hacker News so you can see the conversation before it hits your feed.

LiveBeta

Explore

Home
Hiring
Products
Companies
Discussion
Q&A
Privacy Policy

Resources

Visit Hacker News
HN API
Modal cronjobs
Meta Llama

Briefings

Inbox recaps on the loudest debates & under-the-radar launches.

Connect

© 2026 Not Hacker News! — independent Hacker News companion.

Not affiliated with Hacker News or Y Combinator. We simply enrich the public API with analytics.

Mathlib | Not Hacker News!

Not

Hacker

News!

Home
Products
Mathlib

Product Launch

anonymous

1 points

5 comments

Posted20 days agoActive19 days ago

Mathlib

maturelibrarymathematicians, developers

Key Features

formal proof librarymathematical theoremsLean 4 integration

Tech Stack

Lean 4

Not

Hacker

News!

AI-observed conversations & context

Daily AI-observed summaries, trends, and audience signals pulled from Hacker News so you can see the conversation before it hits your feed.

LiveBeta

Explore

Home
Hiring
Products
Companies
Discussion
Q&A

formal verification

formal verificationmathematicsproof assistants

Discussion (5 comments)

Showing 5 comments

20 days ago

3 replies

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

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

20 days ago

There's some interest in Lean-writing AI.

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

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

View on Hacker NewsHN ID: 46260128Mood: informative

Resources

Visit Hacker News
HN API
Modal cronjobs
Meta Llama

Briefings

Inbox recaps on the loudest debates & under-the-radar launches.

Connect

© 2026 Not Hacker News! — independent Hacker News companion.

Not affiliated with Hacker News or Y Combinator. We simply enrich the public API with analytics.