Lean

Raised as a usability problem by 11 people on Hacker News over 15 years (2011–2025), in 11 threads.

People raised many different problems with Lean, but no single problem has yet been raised by 3 people in 3 different months and threads.

Unreviewed issues were grouped by machine: Claude Haiku labelled each comment as a usability complaint, named what it's about and summed up the problem in a line, and a small model grouped similar problems. Nobody has checked them by hand. Expect mistakes.

The newest 12 complaints

Must click each line to see proof state, breaking reading flow2025-07-31
Hard to read proofs; obscure errors and hidden info in complex VSCode extension2025-03-13
Metaprogramming for tactics is extremely hard to use, with poor ergonomics and stranded docs2024-05-16
Tutorial highlight bubbles are too small and hard to notice on dark theme2024-05-07
Hard to install and run2023-12-08
Configuring the toolchain your own way causes frustration and confusing steps2023-09-08
The VSCode integration for Lean 4 is horrid to use2021-10-12
Interpreter is so slow it makes external solver calls impractical2020-12-28
Signing up via Twitter still required email account, then another login form2012-11-14
Signup form shows a long list of validation errors, blocking access to a free demo2011-04-29
Blocks bounce back and leave a gap instead of lining up side by side2011-04-29
Gray small serif text makes the article annoying to read2011-01-29