lean4-metaprogramming-book

Tech stack & purpose

This repository contains an open-source textbook on metaprogramming in Lean 4, a formal proof assistant language. The book is authored by Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, and Siddharth Bhat, and is made available in both HTML and PDF formats through the Lean Prover Community. The source material is written in Lean files and automatically converted to markdown using the mdgen tool, with contributors expected to edit the original Lean source code rather than the generated markdown files.

Community & reference links

• leanprover-community.github.io/lean4-metaprogramming-book/

Languages

Contributors (top 30 of 34)

• 
  Kitamado99 commits · 114 followers
• 
  Arthur Paulino93 commits · 119 followers
• 
  Julian Berman41 commits · 439 followers
• 
  Henrik Böving32 commits · 182 followers
• 
  Kitamado21 commits · 114 followers
• 
  Jannis Limperg14 commits · 73 followers
• 
  Johan Commelin13 commits · 101 followers
• 
  Siddhartha Gadgil12 commits · 185 followers
• 
  Evgenia Karunus11 commits · 98 followers
• 
  damiano9 commits · 24 followers
• 
  dependabot[bot]5 commits · 0 followers
• 
  Adomas Baliuka4 commits · 6 followers
• 
  Krishna Padmasola3 commits · 7 followers
• 
  Siddharth3 commits · 809 followers
• 
  David Renshaw2 commits · 460 followers
• Rishikesh Vaishnav2 commits
• Belphegor2 commits
• 
  Samuel2 commits · 6 followers
• Joshua Barney1 commits
• Hongxu Xu1 commits
• Yuri de Wit1 commits
• 
  Mac Malone1 commits · 80 followers
• Gregory Blike1 commits
• 
  Kevin Buzzard1 commits · 946 followers
• 
  Ed Ayers1 commits · 92 followers
• 
  Martin Dvořák1 commits · 68 followers
• 
  Bryan Gin-ge Chen1 commits · 49 followers
• 
  Siddharth1 commits · 809 followers
• 
  Yan Yablonovskiy1 commits · 41 followers
• Chris Wong1 commits