MDRMay 20

Hey algorithm, please help me get exposed to people who are interested in type theory, theorem proving and Principia Mathematica. I'm formalizing Principia Mathematica in Rocq.

https://github.com/MudroadWhite/Neo-Principia/

If you want to tame the monster created a century ago by Bertrand Russell, here's your chance to pet the dragon. *pat pat* Comment if you are interested in!

#RocqProver #TheoremProving #formalverification #AI4Math #typetheory #PrincipiaMathematica

GitHub - MudroadWhite/Neo-Principia: Continuation on formalizing Principia Mathematica

Continuation on formalizing Principia Mathematica. Contribute to MudroadWhite/Neo-Principia development by creating an account on GitHub.

GitHub
Show threadsoaprootMay 20
@MDR Nice, I work on Metamath, the propositional logic section of which is in some sense a formalization of that section of Principia Mathematica.
Show threadMDRMay 20
@soaproot Hi there! If I haven't remembered it wrong Metamath should have covered chapter 1 - 5 - I don't know if it has covered chapter 9 and beyond. You have unlocked a little secret for my project: Our ch1-5 proof is valid but unsatisfying, and there will be a collaborator reconstructing this part.
Show threadsoaprootMay 20
@MDR Sounds about right. And even for chapter 1–5, Metamath doesn't take quite the same path as Principia (uses different but equivalent axioms).
Show threadsoaprootMay 20
@MDR I will confess that although I did make it partway through reading Principia, I stalled out before getting beyond chapter 5 (partly due to the unfamiliar notation especially the dots instead of parentheses)
Show threadMDR
@soaproot For dot notation: If a proposition is multi-line, then its indentation usually hints the priority, rendering the dots almost transparent. Still, when developing the proofs, type checking from Rocq does help me eliminate quite some ambiguities before the proof proceeds, without a single exception.
May 20 at 6:28pmWeb