hitchhikers guide lean4

Stream: general

[GabrielT]

Does anyone know if there is a version of the hitchhikers guide book in lean4? Or if there is any plans on rewriting it?

[Matthew Ballard]

Yes. They are currently working out the kinks.

[GabrielT]

Oh nice! Do you know if they are looking for beta readers or volunteers? I'm happy to help if there's help needed

[Matthew Ballard]

@Jasmin Blanchette

[Jasmin Blanchette]

Sorry for the delay in answering. We have indeed a version of the guide based on some quite old Lean 4 and mathlib4 versions (from January). I've made the main files available at https://lean-forward.github.io/hitchhikers-guide/2023/ . We also have solutions and homework files, which I won't put online now. Feedback welcome!

[Bulhwi Cha]

The link to "Lean's mathematical library (git repository)" should be changed from https://github.com/leanprover/mathlib4 to https://github.com/leanprover-community/mathlib4.