Logipedia

Stream: general

[Andrew Ashworth]

http://logipedia.inria.fr the encyclopedia of all formally derived math, hopefully

[Johan Commelin]

@Andrew Ashworth Thanks. Are you involved in this project?
(Typo on the about page: "These proofs, originally developed in Matita , has been expressed in a", s/has/have/)

[Johan Commelin]

And actually more typos in that bit of text.

[Kevin Buzzard]

Why can't the Lean version be displayed in unicode?

http://logipedia.inria.fr/theorems/theorems.php?md=nat&id=le_ind&kind=axiom

[Sebastian Ullrich]

That looks like a very rudimentary pretty printer for Lean

[Scott Morrison]

I'm also not sure what the point of all the whitespace is. Surely for a "rosetta stone", you want to be able to see everything at once if at all possible.