数学家应了解的 Lean Theorem Prover：可靠性与 AI 自动形式化现状

> Autoformalization has become a practical reality in 2026

Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.