principia VS Coq-Equations

You can check it out here: https://www.principiarewrite.com/

It's crazy to think that we didn't really know for sure whether 1+1=2 until ~1910, yet it's true. That's when Bernard Russell (best known for Russell's teapot, exposing a logical fallacy in Christianity) and some other dude actually proved it from axioms. They laid out the foundation of 1+1 in a book called Principia Mathematica. They worked so rigorously that it took them 360 pages to even prove something as basic as 1+1=2 using the axiomatic method. If you want to use a modern tool like Coq to verify 1+1=2, then the best way of doing this is to formalize Principia Mathematica in Coq.

There are people trying to make it more readable.

Principia

A work from the early 20th century, mathematics, logic.

I think some expert called Bertrand Russell's and A.N. Whitehead's "Principia Mathematica" initiative a "bizarre" piece of work, when seen from the perspective of a programming language designer.

I can't make a qualified statement about this, as I am neither a mathematician nor a language designer. And I cannot find the exact quote on the internet, sorry. Just saying.

In code? See for yourself :

https://www.principiarewrite.com/

Whitehead and Russell’s Principia rewritten in Coq\ (44 comments)

I'd say Agda is more similar to Idris than Coq. Coq has a different syntax and isn't as good for programming with dependent types as Agda and Idris (Agda and Idris both put a huge emphasis on dependent pattern matching, something that Coq only recently gained support for through the Equations package).