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",
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?
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