writing a book in Lean 4

Stream: general

[Ethan Wu]

Hi, I'm new to lean. I was wondering if it's possible to write a book in lean4?

[Notification Bot]

A message was moved here from #general > animating Lean proofs in Blender: a video and github repo by Kevin Buzzard.

[Kevin Buzzard]

@Ethan Wu I moved your message to a new thread (you were intruding on another conversation). #mil is a book written in Lean 4.

[Asei Inoue]

@Ethan Wu You could want mdgen. This is used in metaprogramming book.

[Shreyas Srinivas]

You could give verso a try

[Ethan Wu]

Hi thank you for the info!