Original Summary

For ppl who wants to know what is 1+1=2 actually about, 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. More Q&As, to ppl that are not familiar with formal verification: - Where is the video? Where are the pictures? This is not an application so I have no videos and pics. - Then what are we supposed to look at? You actually have to suffer and read Principia Mathematica, and then suffer again to read my code . The code is what you are looking at, and fortunately it's a kind of code pretty different from Python and JS. - What will be the result for running this project? The prover that the code are written on, Rocq, will check if my code contain any errors. So in short it always says my code is correct and that's it. The same happens, when you print a "HelloWorld" and exit 0. - Isn't it too r*tarded if we run the code and produce nothing at all? Rocq is an interactive theorem prover, allowing you to interact with every single line of code. Reading raw PM will not have such privilege. Ppl are supposed to just appreciate how theorems are being deduced rigorously, for a large book. Alternatively, PM-MATS should be the closest application that you guys are expecting. - Have you actually formalized 1+1=2? No, but it is under secret development in another project. DM me if you want to ask questions that far.   submitted by   /u/InternationalFox5407 [link]   [comments]

  • 情报分类：技术学习与提效
  • 分类依据：内容涉及技术、AI、软件工具或工程实践
  • 信息来源：Reddit · SideProject
  • 发布时间：2026/9/20 11:36:29