Notes on books I'm currently studying
 
 
 
Go to file
Joshua Potter 8c5029f8ec Add TeX for axiomatic area definition. 2023-05-10 17:45:55 -06:00
Bookshelf Add TeX for axiomatic area definition. 2023-05-10 17:45:55 -06:00
Common Add TeX for axiomatic area definition. 2023-05-10 17:45:55 -06:00
.env Update lean toolchain and incorporate documentation generation. 2023-05-03 15:31:33 -06:00
.gitignore Rewrite as a single shared library. 2023-04-22 14:20:37 -06:00
Bookshelf.lean Rename `Exercises` to `Bookshelf`. 2023-05-08 14:08:48 -06:00
Common.lean Rename `Bookshelf` to `Common`. 2023-05-08 14:08:48 -06:00
README.md Explain color/symbol code. 2023-05-10 15:30:35 -06:00
lake-manifest.json Correct namespaces and update `bookshelf-docgen`. 2023-05-10 17:20:56 -06:00
lakefile.lean Correct namespaces and update `bookshelf-docgen`. 2023-05-10 17:20:56 -06:00
lean-toolchain Update Lean nightly. 2023-05-08 12:10:15 -06:00
preamble.tex Add TeX for axiomatic area definition. 2023-05-10 17:45:55 -06:00

README.md

bookshelf

A study of the books listed below. Most proofs are conducted in LaTeX. Where feasible, theorems are also formally proven in Lean.

  • Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
  • Avigad, Jeremy. Theorem Proving in Lean, n.d.
  • Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015.
  • Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009.
  • Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.
  • Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
  • Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.
  • Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.
  • Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.

Documentation

To generate documentation, we use bookshelf-docgen. Refer to this project on prerequisites and then run the following to build and serve files locally:

> lake build Bookshelf:docs
> lake run server

This assumes you have python3 available in your $PATH. To change how the server behaves, refer to the .env file located in the root directory of this project.

A color/symbol code is used on generated PDF headers to indicate their status:

  • Teal coloring (with a checkmark) indicates the corresponding proof is complete. That is, the proof has been written in TeX and also formally verified in Lean.
  • Magenta coloring (with a spinner) indicates the corresponding proof is in progress. That is, a proof in both TeX and Lean have not yet been finished, but is actively being worked on.
  • Red coloring (with a warning) indicates the formal Lean proof has not yet been started. It may or may not also indicate the TeX proof has been written.