Logipedia and Lean

Stream: general

[Kevin Buzzard]

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]

The files here look kind of terrifying.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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]

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.