Drafting a Creative Commons Textbook for Lean

Stream: general

[Charles Hoskinson]

Hi Lean community,

I was recently introduced to lean by Professor Buzzard and I think it holds great pedagogical promise for the mathematical community. I run a mid-sized cryptographic research and software development company in the United State (https://iohk.io) and we use formal methods regularly in our workflow (for example https://github.com/input-output-hk/cardano-ledger-specs). We are also quite interested in funding open source initiatives for education in the hard sciences.

We'd love to finance a free, creative commons textbook for mathematics undergraduates to learn how to write proofs using Lean 4 and contribute to the Lean community. I'm curious if anyone here would be willing to write one? We'd cover all costs and help with distribution. IOHK also has several formal methods engineers who would love to assist in the drafting and I'd also be willing to attach a professional editor.

If you (or someone you could refer) would like to explore this idea, then send me an email at Charles.Hoskinson@iohk.io and we can setup a meeting.

[Johan Commelin]

@Charles Hoskinson Thanks for this fantastic offer! And welcome to Zulip :hello:
As you can see from the :tada: emoji reaction to your post, many people think this is a great idea. However, I think that it is still slightly early to write a textbook for maths undergrads about maths in Lean 4.
As a community we are currently exploring and learning how Lean 4 works, and are making plans for porting mathlib from Lean 3 to Lean 4. So my estimate is that a couple of months from now, we will be in a much better position to start working on such a textbook. (This is my personal opinion, I am not a spokesman for the community.)