29.
A first Lean project with mathlib weighs 7 GB (t.co)
Installing Lean through VS Code and creating a starter mathlib project produced a seven-gigabyte directory, revealing the cost of modern formal-math tooling
@arntzenius on Backlist
1 appearance on the backlist front page in the last 30 days.