How is Lean useful?

Stream: lean4

[Oliver]

1. Is it worthwhile to spend so much time fixing each error in Lean for a simple proof of a simple theorem in natural language?

2. Is Lean really useful?

Thanks.

[Riccardo Brasca]

This looks like a subjective question. For some things (like checking correctness of a mathematical argument) is surely useful. It depends on what you want yo do, and "worthwhile" depends on one's goals.

[Henrik Böving]

With systems like Lean that give you a specific benefit in exchange for quite a bit of overhead the question is mostly whether you need the benefits enough to accept the overhead.

The benefits are mostly that you have additional (almost absolute) certainity in the correctness of your arguments. Furthermore as Terence Tao has noted it allows larger scale collaborative mathematical projects than is usually possible just on paper. For computer science applications its mostly about the absolute certainty as projects are usually already large and collaborative.

The overhead is that you have to...well deal with the pickiness of a computer system like Lean, if you are willing to do that to achieve the benefits its worth it.

This is of course disregarding factors like Lean simply not supporting a use case such as Homotopy Type Theory.

[Kevin Buzzard]

Just to hammer home the subjectivity: one can also ask "Is Bourbaki really useful" and also "is modern algebraic geometry really useful" or "is Fermat's Last Theorem really useful" or "is the Stacks Project really useful". You can't really make much sense of the question unless you have some baseline. For me as a professional mathematician Bourbaki and the proof of FLT and the Stacks Project are all very useful, for entirely different reasons, and Lean is also useful in my professional career.