Orbit · Explore

Ask Orbit · by Danylo Kovalenko · 2026-10-16

What are you using to learn Lean / formalized math?

xenaproject.wordpress.com

Kevin Buzzard's latest on formalizing all of mathematics got me curious. Has anyone here started with Lean? Is it approachable for programmers without a math degree?

0 sparks · 9 comments

Comments

Hana Choi · 0 likes

Natural Number Game is the best start, took me a weekend.

Ananya Rao · 1 likes

Second this, its fun.

Ethan Brooks · 0 likes

As a dev the type system feels familiar, tactics are the hard part.

Noor Janssens · 0 likes

Mathlib docs are big, searching is a pain at first.

Hugo Martin · 0 likes

Is there any practical use outside academia?

Amina Okafor · 0 likes

Verified software, some.

Pixel Atlas · 0 likes

AI proof assistants are making this more popular.

Cedar Marauder · 0 likes

I tried, quit after day 3, proofs are slow.

Bianca Santos · 0 likes

Do I need to like proofs? Asking for a friend.