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

• Chapter 1
  • Example 1.1.1 (Page) (Lean source)
  • Example 1.1.2 (Page) (Lean source)
  • Example 1.1.6 (Page) (Lean source)
  • Example 1.1.7 (Page) (Lean source)
  • Example 1.1.8 (Page) (Lean source)
  • Example 1.1.9 (Page) (Lean source)
  • Question 1.1.10 (Page) (Lean source)
  • Example 1.1.11 (Page) (Lean source)
  • Example 1.1.12 (Page) (Lean source)
  • Example 1.1.13 (Page) (Lean source)
  • Example 1.1.14 (Page) (Lean source)
  • Example 1.1.15 (Page) (Lean source)
  • Question 1.1.16 (Page) (Lean source)
  • Example 1.1.17 (Page) (Lean source)
  • Exercise 1.1.18 (Page) (Lean source)
  • Proposition 1.2.4 (Page) (Lean source)
  • Lemma 1.2.5 (Page) (Lean source)
  • Example 1.3.2 (Page) (Lean source)
  • 1.4.5 (Page) (Typst source)
  • Problem 1A (Page) (Typst source)
  • Problem 1C (Page) (Typst source)
  • Problem 1D (Page) (Typst source)
• Chapter 7 (not formalized)
  • Problem 7C (Page) (Typst source)
  • Problem 7E (Page) (Typst source)
• Chapter 8 (not formalized)
  • 8.4.3 (Page) (Typst source)
  • Problem 8A (Page) (Typst source)
  • Problem 8B (Page) (Typst source)
  • Problem 8C (Page) (Typst source)
  • Problem 8D (Page) (Typst source)
  • Problem 8E (Page) (Typst source)
  • Problem 8F (Page) (Typst source)
  • Problem 8H (Page) (Typst source)
  • Problem 8I (Page) (Typst source)
• Chapter 9 (not formalized)
  • 9.4.5 (Page) (Typst source)
  • Problem 9C (Page) (Typst source)
  • Problem 9G (Page) (Typst source)
• Chapter 10 (not formalized)
  • Problem 10C (Page) (Typst source)
  • Problem 10D (Page) (Typst source)
  • Problem 10G (Page) (Typst source)
• Chapter 11
  • Problem 11B† (Page) (Lean source)
• Chapter 64 (not formalized)
  • Problem 64A (Page) (Typst source)
  • Problem 64B (Page) (Typst source)
  • Problem 64C (Page) (Typst source)
• Chapter 65 (not formalized)
  • 65.2.6 (Page) (Typst source)
  • 65.2.12 (Page) (Typst source)
  • Problem 65C (Page) (Typst source)
• Chapter 66 (not formalized)
  • 66.1.3 (Page) (Typst source)
• Chapter 67 (not formalized)
  • 67.5.7 (Page) (Typst source)
  • Problem 67A (Page) (Typst source)
  • Problem 67B (Page) (Typst source)
  • Problem 67C (Page) (Typst source)
• Chapter 68 (not formalized)
  • Problem 68A (Page) (Typst source)
  • Problem 68B (Page) (Typst source)
• Chapter 70 (not formalized)
  • Problem 70A (Page) (Typst source)
  • Problem 70B (Page) (Typst source)
  • Problem 70D (Page) (Typst source)
• Chapter 71 (not formalized)
  • Problem 71B (Page) (Typst source)

• Chapter 5 (not formalized)
  • 5.2.25 (Page) (Typst source)
  • 5.3.8 (Page) (Typst source)
  • 5.3.11 (Page) (Typst source)

• Chapter 2 (not formalized)
  • 2.1.2 (Page) (Typst source)
  • 2.1.4 (Page) (Typst source)
  • 2.1.6 (Page) (Typst source)
  • 2.1.11 (Page) (Typst source)
  • 2.1.12 (Page) (Typst source)
  • 2.1.13 (Page) (Typst source)
  • 2.1.15 (Page) (Typst source)
  • 2.1.18 (Page) (Typst source)
  • 2.1.20 (Page) (Typst source)
  • 2.1.22 (Page) (Typst source)
  • 2.1.24 (Page) (Typst source)
  • 2.1.25 (Page) (Typst source)
  • 2.1.30 (Page) (Typst source)
  • 2.1.31 (Page) (Typst source)

• Chapter 1 (not formalized)
  • 1.2 (Page) (Typst source)
  • 1.6 (Page) (Typst source)
  • 1.8 (Page) (Typst source)
  • 1.10 (Page) (Typst source)
  • 1.12 (Page) (Typst source)
  • 1.13 (Page) (Typst source)
  • 1.15 (Page) (Typst source)
• Chapter 2 (not formalized)
  • 2.2 (Page) (Typst source)
  • 2.3 (Page) (Typst source)
  • 2.6 (Page) (Typst source)
  • 2.8 (Page) (Typst source)
  • 2.9 (Page) (Typst source)
  • 2.14 (Page) (Typst source)
  • 2.18 (Page) (Typst source)
• Chapter 3 (not formalized)
  • 3.1 (Page) (Typst source)
  • 3.2 (Page) (Typst source)
  • 3.4 (Page) (Typst source)
  • 3.5 (Page) (Typst source)
  • 3.7 (Page) (Typst source)
  • 3.11 (Page) (Typst source)
  • 3.12 (Page) (Typst source)
  • 3.14 (Page) (Typst source)
  • 3.15 (Page) (Typst source)
  • 3.17 (Page) (Typst source)
  • 3.18 (Page) (Typst source)
  • 3.20 (Page) (Typst source)
  • 3.21 (Page) (Typst source)
  • 3.22 (Page) (Typst source)
• Chapter 4 (not formalized)
  • 4.4 (Page) (Typst source)

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.

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

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.