Napkin Solutions

This repository serves solutions for the problems from the book, An Infinitely Large Napkin by Evan Chen and contributors, along with Lean 4 formal proofs of the book.

The goal of this project is to port all existing solutions from the https://e.hyeon.me/napkin.svg to Typst and formalize them in Lean.

cd www
pnpm i
pnpm dev

 

Typst solutions

The typst/ directory contains Typst solutions of the book.

# Download fonts
typst/x prepare-fonts

# Check typst codes
typst/x check
typstyle --check typst

# New contributor registration
typst/x register <github-handle>

# Help
typst/x --help

Following tools are recommended for a better contribution experience:

• typstyle - Typst code formatter
• Espanso - Write mathematics symbols outside Typst.
• RanolP/Typsi - If you like typst-y symbol names, use this espanso package.

When editing the template styles, keep a live preview of the template API docs open to see your changes as you go:

# Typst in watch mode, see typst/lib/napkin-docs.pdf
typst watch --font-path typst/fonts typst/lib/napkin-docs.{typ,pdf}

This project uses the following fonts.

• Latin Modern Sans for #blue_box.
• Hakgyoansim Bareonbatang for Korean.

 

Lean proofs

The lean/ directory contains Lean 4 formal proofs of the book.

cd lean

# Build the project
lake build

# Type-check specific files in CLI
lake env lean NapkinProofs/Obviouslib.lean
lake env lean NapkinProofs/Chapter1.lean

Learn Lean

Learning materials

References

Brief A Tour of Lean Examples Lean 4 tactic cheatsheet (pdf) Game The Natural Number Game Lean Game Server Books Functional Programming in Lean (FPIL) Theorem Proving in Lean (TPIL) Mathematics in Lean (MIL), PDF version Further readings The Hitchhiker's Guide to Logical Verification (pdf) Logic and Proof The Mechanics of Proof Lean 4 VS Code extension manual Metaprogramming in Lean 4, PDF version Lean perfectoid spaces Type Checking in Lean 4 A glimpse of Lean

Docs Lean community The Lean Language Reference A mathlib overview Mathlib documentation Search Loogle, LeanExplore, Moogle, LeanSearch, Lean-Finder LLM-based assist LeanDojo, BFS-Prover-V2, Aristotle other resources REPL, Pantograph, Lean4Web

 

---

This project is primarily distributed under the terms of the GNU Affero General Public License v3.0 or any later version. See COPYRIGHT for details.