alt Hacker NewsIf we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev
Replies
lioeters • today at 4:16 PM
Oh how interesting, they're using a fork of Agda called Mikan, not Lean as I imagined before visiting the link. https://1lab.dev/Mikan.html
➕ show 1 reply
If it really is formalized, it seems like the exact ideas would be able to be translated to and from any other sufficiently capable language without gaining or losing anything.