It took Russell and that other guy 360 pages to prove that 1+1=2. That's how rigorous math is.

This page summarizes the projects mentioned and recommended in the original post on /r/rmathcirclejerk
Logic history-of-philosophy coq coq-ecosystem formal-logic

WorkOS
Our great sponsors
  • WorkOS - The modern identity platform for B2B SaaS
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • SaaSHub - Software Alternatives and Reviews
Our great sponsors

  • principia

    The Principia Rewrite (by LogicalAtomist)

    • It's crazy to think that we didn't really know for sure whether 1+1=2 until ~1910, yet it's true. That's when Bernard Russell (best known for Russell's teapot, exposing a logical fallacy in Christianity) and some other dude actually proved it from axioms. They laid out the foundation of 1+1 in a book called Principia Mathematica. They worked so rigorously that it took them 360 pages to even prove something as basic as 1+1=2 using the axiomatic method. If you want to use a modern tool like Coq to verify 1+1=2, then the best way of doing this is to formalize Principia Mathematica in Coq.

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

    WorkOS logo
NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts