How to formalize all of mathematics: what it means for software engineers

Arif Hasan · 13 likes

Formalization is slow and painful. I tried a small theorem and gave up after a weekend.

Ren Suzuki · 12 likes

LLMs writing Lean proofs is the first AI application I find truly exciting, since the checker tells you if it's right.

Sleepy Noodle · 1 likes

The compiler as a lie detector, love that

Léa Bernard · 2 likes

Ambitious project, but I trust them. They've been steadily delivering.

Martina Fernández · 0 likes

For most business software, tests are enough. Verification is for crypto, kernels, and compilers.

Ananya Rao · 0 likes

The library maintenance burden alone is huge. Mathlib refactors scare me.

Piotr Zieliński · 0 likes

Imagine if all specs in industry were machine-checkable. We'd lose half our meetings.

Midnight Panda · 6 likes

And half of the job security 😅

Rapid Otter · 0 likes

Reading about this makes me want to learn Lean, and I know I won't finish.