Zulip Chat Archive

Stream: general

Topic: Logipedia and Lean


Kevin Buzzard (Mar 06 2020 at 22:51):

Various people have been in touch with me concerning getting involved in various ways with Logipedia/Dedukti. Can anyone explain what these things are and what they have to do with Lean, in a way that a mathematician can understand? I'm not sure I know what Reverse Mathematics is, which doesn't help.

Kevin Buzzard (Mar 06 2020 at 22:53):

The files here look kind of terrifying.

Mario Carneiro (Mar 06 2020 at 23:16):

Those files make me feel better about the comparative quality of the MM0 -> lean translation :)

Mario Carneiro (Mar 06 2020 at 23:16):

These files look automatically generated from a proof in first order logic

Mario Carneiro (Mar 06 2020 at 23:16):

they axiomatize nat and other funny things that aren't necessary in lean

Kevin Buzzard (Mar 06 2020 at 23:32):

So the idea is that we can write one proof in one system and it turns into some very complicated things in lots of systems?

Kevin Buzzard (Mar 06 2020 at 23:32):

And then we end up not being able to prove the prime number theorem because it's about the wrong real numbers?

Mario Carneiro (Mar 06 2020 at 23:42):

Yes, that's usually what interchange languages end up doing. I think it is important to spend some time on making it look not-horrible though and that work clearly hasn't been put in for Dedukti -> Lean. (I mean seriously, ((@foo) ) is just horrible formatting and double parens are never required.)

Mario Carneiro (Mar 06 2020 at 23:44):

One way to clean it up pretty well is to pass it through lean after translation, that is, getting it parsed by lean and printed by the lean pretty printer, which of course knows a lot more about when @ signs are needed, where parentheses go, how to use indentation and so on.

Mario Carneiro (Mar 06 2020 at 23:46):

The approach I took was to skip all definitions that would otherwise be "axioms", like nat.O, and put them in a separate file for human review. By a manual process, the user makes these all definitions pointing to the correct thing (i.e. def nat.O := nat.zero) and then everything later will still typecheck and you don't need any axioms that aren't standard lean axioms.


Last updated: Dec 20 2023 at 11:08 UTC