Stream: general

Topic: Logipedia

Andrew Ashworth (Mar 18 2019 at 12:00):

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

Johan Commelin (Mar 18 2019 at 12:14):

@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 (Mar 18 2019 at 12:15):

And actually more typos in that bit of text.

Kevin Buzzard (Mar 18 2019 at 12:17):

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 (Mar 18 2019 at 20:13):

That looks like a very rudimentary pretty printer for Lean

Scott Morrison (Mar 18 2019 at 21:19):

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.

Last updated: May 08 2021 at 09:11 UTC