Lean4 formal proofs of "An Infinitely Large Napkin".
Note
This project is still very incomplete.
# Build the project
lake build
# Type-check specific files in CLI
lake env lean NapkinProofs/Obviouslib.lean
lake env lean NapkinProofs/Chapter1.lean| Learning materials | References |
|---|---|
|
|
Â
napkin-community/proofs is primarily distributed under the terms of the GNU Affero General Public License v3.0 or any later version. See COPYRIGHT for details.