Formalizing Principia Mathematica using Lean
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…
In plain words
This project formalizes the first volume of Bertrand Russell's Principia Mathematica using the Lean theorem prover. It translates Russell's mathematical proofs into machine-verifiable code while adhering closely to the original arguments, adding minimal statements beyond those necessary for formalization. The work targets mathematicians and formal verification researchers interested in classical logic foundations and serves as an alternative formalization to existing versions in other proof assistants.
written from the facts on this page · September 2026
From the sources
In the maker’s words, at launch
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
More work this month
the category →
The app store for voice native apps that lives in your notch
Work · 28d ago · voiceos.com
The New Calendly▲211Handle all of the work before, during, and after meetings
Work · 17d ago · calendly.com
Launched alongside, April 2025
the whole month →- IB
Hi everyone, I built PyXL — a hardware processor that executes a custom assembly generated from Python programs, without using a traditional interpreter or virtual machine. It compiles Python -> CPython Bytecode -> Instruction set designed for direct hardware execution. I’m sharing an early benchmark: a GPIO test where PyXL achieves a 480ns round-trip toggle — compared to 14-25 micro seconds on a MicroPython Pyboard - even though PyXL runs at a lower clock (100MHz vs. 168MHz). The design is stack-based, fully pipelined, and preserves Python's dynamic typing without static type restrictions.…
Dev tools · 2025 · runpyxl.com
- UC
Life & fun · 2025 · filiph.github.io
- IB
https://the-pocket.github.io/Tutorial-Codebase-Knowledge/
AI · 2025 · github.com
