Me too, I want to follow

https://github.com/blanchette/logical_verification_2023

The hitchhiker's guide

I tried Lean twice and what caused me to stop both times was a severe lack of documentation. That's a shame, because it's an awesome language.

I also tried to get into it recently, and I feel theorem proving has been pretty substantially oversold. It seems that if you wanted to work through the proofs in even an advanced undergraduate or early graduate textbook, you would basically have publishable material at the end because of the lack of cohesive libraries. There is a lot that gets buried in and is still open to implementation details, and I don't see any clear way of simply proceeding. It started to feel like a major distraction from just doing the mathematics rather than an aid, like it's supposed to be. It feels a little like the Rust ecosystem, where there is a land grab rush to introduce various libraries.

I agree that there's generally too little results in mathlib and for that matter in any theorem prover, but I didn't think that work on formalizing such stuff (advanced undergrad results / early grad results) is publishable. Was I wrong in this?

There are plenty of published papers about newly formalized proofs, even in "undergrad" math. A formal proof development generally brings to light new information about the original proof, both by plugging all potential inaccuracies/missing steps and in being especially easy to refactor, abstracting out common patterns that might be reused elsewhere.

Same, I also found no good "for programmers" introduction.

There is a short one[1] from Functional Programming in Lean, which is itself an introduction to Lean 4 from the programming's perspective. Highly recommended if you're interested in dependent types.

[1]: https://leanprover.github.io/functional_programming_in_lean/...

Because the audience isn't "programmers".

I think that is unnecessarily hostile; I believe Lean 4 can become a very capable programming language for mundane tasks!

Hostile? I just stated that the audience isn't programmers.

The age of guilds has long passed

Are people like these not programmers? https://leandojo.org/

How can the audience of a general-purpose programming language not be "programmers"?

I don’t think that your post is hostile. But from what I’ve heard, it is untrue because Lean 4 is intended to be a general purpose programming language, not only a theorem prover. I can’t find a source that directly states this goal but at the least this paper by Leo de Moura and Sebastian Ullrich presents it as a programming language:

https://link.springer.com/chapter/10.1007/978-3-030-79876-5_...

Microsoft also sponsored David Thrane Christiansen’s book, Functional Programming in Lean[1] (which I’m sure you know about!). That is another indication that they intend to reach programmers.

[1] https://leanprover.github.io/functional_programming_in_lean/

It seems general programming is more in focus now, but for context, the "Programming in Lean" book was only completed recently as compared to the multiple theorem proving documents which have been around for a while. The Christiansen book looks worth waiting for though and I really hope Lean can gain popularity as a general purpose language.

I'm not looking to use it as a programming language, but I'd like to see an introduction to theorem proving using Lean that is more explicit in its explanation of semantics than the ones that assume an existing math background

Theorem Proving in Lean 4: https://leanprover.github.io/theorem_proving_in_lean4/

I only had a basic knowledge of first-order logic and set theory before reading TPiL4. It wasn't easy, but now I can prove theorems in Lean. By the way, I still can't write a program in any language.

Kinda agree but Mathlib and its documentation makes for a big corpus to learn by example from. Not ideal but it helps.

https://github.com/leanprover-community/mathlib

A https://learnxinyminutes.com/ for Lean and Lean Mathlib would be a helpful resource

On the contrary, I think the basics are covered pretty well by the official documentation, but it's lacking the more advanced stuff.

I agree; for simple and "beginning intermediate" tasks, Functional Programming in Lean has it all; but the more advanced features are only documented in the source code and doc-strings. There is also a lack of general listings: for data structures, for file access API, for algorithms etc.

Is there an eBNF+PEG or similar grammar for the language parser that a more complete language reference can be generated from?

Does Lean have docstrings with embedded markup like Python?

The Python Language Reference: https://docs.python.org/3/reference/

The Python Language Reference > 10. Full Grammar specification: https://docs.python.org/3/reference/grammar.html

LearnXinYminutes > Where X=Python: https://learnxinyminutes.com/docs/python/

In the language and then the docs, Python's collections.abc Abstract Base Classes did not initially exist. There's now a table of ABCs in the docs: https://docs.python.org/3/library/collections.abc.html#colle...

In Python, they're not interfaces, they're ABCs.

Get on Zulip[1] and ask for help when stuck. The community is friendly and has gotten quite large although they are mostly mathematicians at the moment.

[1] https://leanprover.zulipchat.com/