This project aims to formalize the first volume of Prof. Bertrand Russell’s Principia Mathematica using the Lean theorem prover. Throughout the formalization, I tried to rigorously follow Prof. Russell’s proof, with no or little added statements from my side, which were only necessary for the formalization but not the logical argument. Should you notice any inaccuracy (even if it does not necessarily falsify the proof), please let me know as I would like to proceed with the same spirit of rigour. Before starting this project, I had already found Prof. Elkind’s formalization of the Principia using Rocq (formerly Coq), which is much mature work than this one. However, I still thought it would be fun to do it using Lean4.
https://ndrwnaguib.com/principia/
https://github.com/ndrwnaguib/principia
Comments URL: https://news.ycombinator.com/item?id=43797256
Points: 31
# Comments: 8
Inicia sesión para agregar comentarios
Otros mensajes en este grupo.
Article URL: https://timestripe.com/magazine/blog/timezone/
Article URL: https://arxiv.org/abs/2505.23735
Comments URL: https://news.ycombinator.c
Article URL: https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/
Comments URL:
After waiting 8 months for a journal response or two months for co-author feedback that consisted of "looks good" and a single comma change, we built an AI-powered peer review system that helps re
Article URL: https://aartaka.me/this-post-is-ed.html
Comments URL: https://news
Article URL: https://susam.net/two-ideals-of-fields.html
Comments URL: http
Hey HN, I've been working on fontofweb.com on and off for the past 4 years, and I'm keen to share it with you. It lets you type in the URL of any website and see exactly how the fonts are used: al
