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 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 threadtheHigherGeometer

@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.

May 20 at 12:35pmWeb