See what people are saying (1)
README
Neo Principia
Continuation of Principia Mathematica's formalization by Landon Elkind.
Why working on it
- 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
How well have you formalized?
Which means 3 questions:
- How much can you formalize? Theoretically, the whole book. See overview for analysis and features.
- How much have you formalized? 199 - 94 = 105 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.
Running the code
Coq/Rocq version: >= 8.20.0, < 9.0, installed with the opam environment:
opam update
opam install coq
opam pin add coq 8.20.0
Running the project:
make
The 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.
Running the code, line by line
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.
To contribute
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.
Related works
- 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
Other useful links
- 1 Discussion of the 4-color theorem, as a reflection.
- 2 PM SEP
- 3 PM Wiki
- 4 MO QA
- 5 MO QA 2
- 6 A rare post that goes over chapter 20 giving insights to PM!
- 7 One link that helps me understand what is matrix
- 8 Another random material that I think related to the matrix in PM
- 9 A site containing nice papers with better technologies to digest, although unused in this project
- 10 Landini, Gregory. (2022). Note on Principia's *38 on Operations. Russell: the Journal of Bertrand Russell Studies. 41. 10.15173/russell.v41i2.5046.
Contributors
1,497 commits
6 commits
Similar repos
Languages
Rocq Prover
99.9%
See what people are saying (1)
README
Neo Principia
Continuation of Principia Mathematica's formalization by Landon Elkind.
Why working on it
- 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
How well have you formalized?
Which means 3 questions:
- How much can you formalize? Theoretically, the whole book. See overview for analysis and features.
- How much have you formalized? 199 - 94 = 105 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.
Running the code
Coq/Rocq version: >= 8.20.0, < 9.0, installed with the opam environment:
opam update
opam install coq
opam pin add coq 8.20.0
Running the project:
make
The 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.
Running the code, line by line
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.
To contribute
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.
Related works
- 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
Other useful links
- 1 Discussion of the 4-color theorem, as a reflection.
- 2 PM SEP
- 3 PM Wiki
- 4 MO QA
- 5 MO QA 2
- 6 A rare post that goes over chapter 20 giving insights to PM!
- 7 One link that helps me understand what is matrix
- 8 Another random material that I think related to the matrix in PM
- 9 A site containing nice papers with better technologies to digest, although unused in this project
- 10 Landini, Gregory. (2022). Note on Principia's *38 on Operations. Russell: the Journal of Bertrand Russell Studies. 41. 10.15173/russell.v41i2.5046.
Similar repos
Contributors
1,497 commits
6 commits
Languages
Rocq Prover
99.9%