Continuation of Principia Mathematica's formalization by Landon Elkind.
WARNING: the documentation is currently under heavy WIP and can be highly volatile
- Principia Mathematica has a stable version
- Principia Mathematica is not textbook math
- Formalized PM is a good textbook for verifiers
- Formalizing PM feels like building an obelisk
- Rocq doesn't need a lot of version updates
Which means 3 questions:
- How much can you formalize? Theoretically, the whole book. See overview for analysis and features.
- How much have you formalized? 194 - 94 = 100 pages. See mechanics for detailed discussions.
- How deep can you formalize? We're using shallow embedding, which is not rigorous deep embedding. We didn't type the propositions, so the proofs are still not 100% correct. See audit for our major defects.
Coq/Rocq version: >= 8.20.0, < 9.0, installed with the opam environment:
opam update
opam install coq
opam pin add coq 8.20.0Running the project:
makeThe awesome Makefile gathered from @clarus's awesome repo, is supposed to automatically detect all .v files under the pm folder, generate the _CoqProject file and compile the whole folder. This is done without deploying the project with dune environment.
IDEs for Coq/Rocq varies, but here is my preference:
- WSL instance: Ubuntu 18.04 on WSL 2
- VS Code version: 1.80.0
- Extension installed on VSCode locally: WSL. When running the extension, it will generate a notification to help you install VSCode support in the current WSL instance.
- Extension installed on VSCode, in its remote WSL environment: VSCoq v0.3.7 from OpenVSX.
Although I have tried to organize the issues well to indicate the current progress, I don't have rich experience in collaborations. A contribution guideline is currently working in progress. It's still suggested to open a new issue for inquiries, and I'll see what I can give.
- Landon Elkind's formalization of PM
- ndrwnaguib's formalization of PM in Lean
- Randall Holmes's RTT implementation
- xamidi's propositional calculus theorems from Łukasiewicz's L1-system
- Also his pmGenerator generating minimal proofs for a collection of PM theorems
- Metamath solitaire's implementation on propositional calculus theorems
- https://proofassistants.stackexchange.com/questions/1105/how-does-the-formal-proof-of-the-four-color-theorem-work Discussion of the 4-color theorem, as a reflection. Viewers are also encouraged to check out the project since it's not that complicated
- https://plato.stanford.edu/entries/pm-notation/
- https://en.wikipedia.org/wiki/Glossary_of_Principia_Mathematica
- https://mathoverflow.net/questions/27793/russell-and-whiteheads-types-ramified-and-unramified
- https://blog.plover.com/math/PM.html A rare post that goes over chapter 20 trying to give insights to PM!
- https://www.religion-online.org/article/the-axiomatic-matrix-of-whiteheads-process-and-reality/ One link that helps me understand what is matrix
- https://nap.nationalacademies.org/read/10866/chapter/66 Another random material that I think related to the matrix in PM
- https://www.ens-lyon.fr/LIP/PLUME/production/ A site containing nice papers with better technologies to digest, although unused in this project