For people who are interested in Principia Mathematica
Hey all,
I'm formalizing Principia Mathematica into Rocq, as what most people do in the AI4Math field. If you want to tame the monster created a century ago by Bertrand Russell, here's your chance to pet the dragon. *pat pat*
Several things to say for this project:
- Beginner friendly(in the sense of Rocq programming): if you just want to get hand dirty, the few chapters in the beginning start with fewer tactics than Software Foundations , the most commonly used textbook for Rocq beginners
- Expert welcoming: if you want to be challenged, go for later chapters, dig for deeper ideas, and maybe eventually prove the noted `1+1=2`
- Starting with "5-years-old" techniques to resolve meaningful "real-world" problems
- A lot of documentation. That's also why I keep this promo as short as possible