Mike PMay 20
MDR

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
May 20 at 12:29pmWeb
Show threadMDRMay 25
Behind our project formalizing Principia Mathematica, today our team has been formed. Participants consist of a leader that writes documentation 10 words in this day, an undergrad that hides his activity from Discord server since the morning, plus a professional master who haven't yet joined the Discord group from our Reddit discussions! You guys will soon find it out that you have no salary to get, no more features to add and will be fired. Welcome to the team.
Show threadMDR6d ago
Welcome to the first PR contributing to our project! Everything starts slow and grows fast. It has been 3 days since I have privately proposed the requirement, but this latency is still way better than me: longest record for myself is a full month! Such massive achievement worths a separate milestone being recorded in the docs.
Show threadMDR3d ago
Writing the documentation is such a enjoyable work: You have to write it again, because you know what you're doing is just preparing for your next rewrite! A whole week has already been dedicated to a single page, and you know it isn't even the end.
Show threadMDR1d ago
Welcome to another episode of our unofficial dev log! I have finally made the docs covering necessary details, which means it might still be unreadable! At the same time our only fellow contributor started to appreciate the readability for our proof and is slowing pacing to the right track! I hope he will be a little professional after at most 5 PRs.
Show threadtheHigherGeometerMay 20
@MDR No algo in mathstodon that I know of, but I certainly approve of this exercise, I've long thought it should be done!
Show threadMDRMay 20
@highergeometer Hi there! Thanks for the encouraging. Strictly speaking, no one including me has "done" the formalization. But I do think it is a topic that deserves more attention, and to my best knowledge it can be done.
Show threadtheHigherGeometerMay 20

@MDR I agree it can be done, Russell and Whitehead were hampered by virtue of not having a (digital) computer and a suitably-mature proof assistant to run on it!

Certainly if you find any (new) bugs that would be of historical interest, and likely to attract attention.

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 threadMDRMay 20
@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.
Show threadDr. SobekMay 21
@MDR @MonniauxD heard you know *a bit* of Rocq ?