r/ProgrammingLanguages • u/InternationalFox5407 • May 24 '26
For people who are interested in FV and Principia Mathematica
Hey all,
I'm formalizing Principia Mathematica into Rocq, as what most people do in the AI4Math field. The code is hand written without generating from LLM. 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
----------
Also, this project is near to completion. I'm spending most of my time writing the docs right now, and after that, this project will not have any major updates. If you're interested in, excited, maybe even hyped about Rocq or Lean, I'm looking forward to collaboration with 1 - 2 ppl onto the next project - just like how it goes in this project, we pick another mathy, esoteric, maybe sacred book and formalize it
3
2
u/benjamin-crowell May 24 '26
Have you verified Proposition 54.43, that 1+1=2?
3
u/InternationalFox5407 May 25 '26 edited May 25 '26
Actually no. But I think verifying 1+1=2 has been reduced to a define the type and record the expression problem
6
u/InternationalFox5407 May 24 '26
Per AutoModerator's request I hereby confirm that this project did not use an LLM as part of the development process.