Natural numbers game Lean4

Stream: Lean for teaching

[Apurva Nakade]

Hi,

I recently tried playing around with NNG4 and I found it very difficult to parse!

I remember really enjoying NNG when I first learned Lean3, and looking back the simplicity of each page really helped. With the Lean4 NNG, I'm just finding it hard to keep track of so many things on the page.

I understand that it must have taken a lot of effort to get this site running (which I'm grateful for), but I think that the pages are really cluttered and difficult to learn from. IMO, the Lean3 NNG UI was much more conducive to learning.

I'm curious to hear what other people think about this.

[Apurva Nakade]

Here are the first levels of "Addition World" on the two sites for quick reference:

Screenshot-2023-09-06-at-1.41.48-PM.png

Screenshot-2023-09-06-at-1.42.02-PM.png

[Kevin Buzzard]

What's the difference? Is it just that NNG3 had folded-up tactics and theorem names?

[Apurva Nakade]

Not just that, there is "Proof History", "Objects", "Assumptions". There is a commentary going on above the goal window and the Goal window looks nothing like in VSCode.

[Patrick Massot]

You can click on the editor mode button if you want to get back an editor.

[Patrick Massot]

I think you are too much used to the VSCode interface to be impartial. You are so used to it that you forgot it was also very complicated to understand.

[James Gallicchio]

but that could be accomplished by having a page explain the infoview :p
infoview is a pretty well-designed UI, and if it's the primary way people interact with Lean I'd rather be introduced to it quickly as a beginner

[James Gallicchio]

but it's probably good to have a choice, since I imagine some people would prefer a softer introduction

[Apurva Nakade]

Yeah, switching to the editor mode is the first thing I did xD

But isn't VSCode the defacto method of interacting with Lean (I so wish it wasn't)?

[Apurva Nakade]

I just noticed that even the Goals are split in two: "Current Goal" and "Further Goals" :(

[Apurva Nakade]

And there is a third "Goal" at the bottom :(

[Kevin Buzzard]

I really like that. In NNG3 I had to emphasize that tactics only acted on the top goal.

[Apurva Nakade]

For me, NNG3 was the perfect learning guide! I never had students complain about any aspect of it.

[Apurva Nakade]

My gripe with NNG4 is just with the UI. The site is really cool and clearly a lot of work went into it. But why change the UI so drastically?

[James Gallicchio]

honestly having the objects and assumptions and current goal and future goals separated seems fine to me. a couple UI things I don't love:

• the goal is below the input line (?) which feels quite confusing to me, since I have to go back and forth from top to bottom to get all the information
• in editor mode, the example line doesn't actually correspond to current tactic state: image.png
  
• black text on blue background is pretty hard to read. if anything, I'd prefer the code be distinguished from the text, not the text be distinguished from the code. I also find the different background color on code snippets to be very distracting

thoughts?

[Kevin Buzzard]

I am certainly not an expert in UI, I just design the levels. I'll mention again that in September there will be a big revamp/expansion of the game but at the end of the day I'm just writing lean code and it's lean4game which is translating it into a website

[James Gallicchio]

is lean4game still running lean on the host server instead of in browser?

[Patrick Massot]

Yes, unless you managed to compile Lean 4 to WASM (with a reasonable size) and forgot to tell us.

[James Gallicchio]

got it, I'll maybe put together a PR on that repo then

[Jon Eugster]

@Apurva Nakade thank you for the feedback! You will be pleased to know that many of the concerns have already been addressed when we redesigned the UI after that first draft, in particular decluttering it. This basically just waits on deployment.

Some thoughts on various other points mentioned here:

[Jon Eugster]

James Gallicchio said:

but that could be accomplished by having a page explain the infoview :p
infoview is a pretty well-designed UI, and if it's the primary way people interact with Lean I'd rather be introduced to it quickly as a beginner

In which case you can just download MIL and learn lean that way ;)

[Jon Eugster]

honestly having the objects and assumptions and current goal and future goals separated seems fine to me. a couple UI things I don't love:

• the goal is below the input line (?) which feels quite confusing to me, since I have to go back and forth from top to bottom to get all the information

:check: That's already done, too. I had the same strong feelings about this :wink:

• in editor mode, the example line doesn't actually correspond to current tactic state: image.png

I have to look at this. That is definitely related to lean4game#84.

• black text on blue background is pretty hard to read. if anything, I'd prefer the code be distinguished from the text, not the text be distinguished from the code. I also find the different background color on code snippets to be very distracting

I always thought that blue background is not ideal for anybody who has problems with lower contrasts... So far I haven't changed the default values but that's a trivial change.

[Apurva Nakade]

Jon Eugster said:

Apurva Nakade thank you for the feedback! You will be pleased to know that many of the concerns have already been addressed when we redesigned the UI after that first draft, in particular decluttering it. This basically just waits on deployment.

Some thoughts on various other points mentioned here:

This is great! I'm really looking forward to it.

[Jon Eugster]

James Gallicchio said:

is lean4game still running lean on the host server instead of in browser?

Yes, and it's unlikely that will change. But it means you will be able to play the new design on your mobile, once that's live :)

and please feel welcomed to submit PRs! I'm also happy to talk about it and any open issues we know of.

[James Gallicchio]

thanks for the response!! and for maintaining NNG post-port :)

[Kevin Buzzard]

I think that ability to play on mobile is fabulous news

[Flo (Florent Schaffhauser)]

Yes, that will be a hit with students!

[Hypatia du Bois-Marie]

anyone knows what i should do when https://github.com/leanprover-community/lean4game/issues/102...?

[Jon Eugster]

I dont think codespaces has ever been setup at all to start the game locally, yet. I'll have a look later and see if I can set that up

[Treq]

Was the removal of the proposition worlds (from NNG3 to NNG4) done to try to refocus the game on ℕ? I thought function and proposition world were a cheeky (fun) way of showing Curry–Howard correspondence.

[Kevin Buzzard]

Yes and yes. I have always had terrible problems with the apply tactic, and I thought that by showing it all in this level of abstraction would help. But in NNG4 I decided a different approach -- persuade someone to write apply ... at. Preliminary testing seemed to indicate that this was a really good idea, mathematicians understand it much better, so I didn't need to stress the analogue that a proof is a function, so I ripped out all the abstract proposition stuff precisely, as you say, because it's not about numbers. Think of it as an opportunity -- there's now plenty of room for a logic game! The issue is that every proof in the logic game is tauto, whereas by the time to have got to advanced addition world one has to sometimes start thinking.

[Kevin Buzzard]

In my experience it's the CS people who like the abstract Prop stuff more, and the maths people who complain about it, and I am very much targetting the maths people.

[Treq]

I'm a beginner, but I assume once you're doing predicate logic you can't just tauto all of it. If I understand the description in NNG4, tauto can prove anything whose semantics can be denoted by a truth table.

Maybe a separate logic game would be fun. I wonder if Lean would let me create puzzles in sub-structural or multiple-valued logics in a way that's still ergonomic/fun. I'm not sure if anybody has any intuition if such a project would be fruitful. Might be a good back-burner project as I learn some lean :)

[Dan Velleman]

I've been playing around with the idea of a set theory game--which would be pretty close to a logic game, since, for example, complement, intersection, and union are closely related to "not", "and", and "or", and intersections and unions of families of sets are closely related to "for all" and "there exists".

[Flo (Florent Schaffhauser)]

Sounds fun! Plus, it would give the interested user a chance to see how basic logical connectors are implemented as inductive types in Lean. Let me know if you need more people to work on this (→ a logic game) :smile:

[Treq]

That's not a bad idea, but of course you'd still have to introduce FOL if you're going to be foundational. Set theory (any of its various forms) is not just theories of sets; they are theories of sets and propositions. Pretty quickly you'll have to create an account of the rules for forming first-order formulas. Which can be type theoretic, but amounts to some ambient logic. At least that's how I understand what's happening...

One of the things that makes type theory interesting is that first-order logic in type theory is just a special case of the type-forming rules. A proposition is merely a certain type; to prove it is to exhibit an element of that type. Set theory doesn't have that, so you need specify how all logical formulas are to be interpreted. Which I think means either assuming how that's done or starting with a logic game that turns into a set-theory game.

[Patrick Massot]

Treq, I think you misunderstood the proposal. I guess Dan met naive set theory, not set theory as a foundation.

[Treq]

SI just stumbled across this: though it would need to update it for lean 4. https://lean-lang.org/logic_and_proof/sets_in_lean.html

Patrick; yeah, I suppose that's right. NNG4 introduces and uses the tactics that manipulate logical formulas without really being a logic game. So there's no reason you can't do the same with a set theory game.

[Patrick Massot]

Logic and proof is unlikely to be updated to Lean 4 soon, but that section should be very close to the corresponding section in #mil

[Dan Velleman]

Yes, Patrick is right. What I have in mind is naive set theory, and at a pretty elementary level. The idea would be to use set theory as a vehicle to introduce some basic Lean tactics and theorems.

[Treq]

@Dan Velleman That sounds like a fun game to me. I'd definitely play!

[Marcus Zibrowius]

A "logic game" and a rudimentary "naive set theory game" are planned as parts of the Formaloversum game, a first version of which can also be found at https://adam.math.hhu.de. My aim for this game is to cover topics from the first year of lecture courses at a typical German university, in the order in which they typically appear — regardless of the merits of that choice of topics or that particular order. I would simply like students to be able to play this alongside of their lectures.

[Marcus Zibrowius]

The "logic game" is ready for consumption. It consist of the three planets Logos, Implis, and Quantus, and ends with a formalization of the drinker's paradox. If 'apply at' gets included in mathlib, I would be keen to rewrite the levels accordingly.

[Marcus Zibrowius]

The "naive set theory planet" is not ready. It will be rewritten.

[Marcus Zibrowius]

The development of the Formaloversum has stalled a bit, simply because I did not sufficiently anticipate how much work would need to go into the Lean game engine. But we are still hopeful we can make significant progress next year.

[Kevin Buzzard]

apply at is already in mathlib.

[Marcus Zibrowius]

Sorry, I missed that. This community is too fast for me.

[Treq]

Are there any circumstances in which ... := by exact expr would differ from ... := expr? where expr is just some well formed expression?

[Damiano Testa]

Sure: this is a recent example.

[Treq]

Ah, awesome. I should've searched first! Thanks for your help.

[Treq]

So the Peano axioms are used to define MyNat, right? Would it be correct to not think of them as axioms in this context? MyNat is built on-top of some type-forming axioms, so it's not like you could alter the definition to create an inconsistent system that proves False. We can't prove that calc of constructions is consistent, but when defining MyNat we haven't taken on any additional burden in that regard?

[Kevin Buzzard]

Sure you can think of them as axioms. They don't have proofs after all. We've just assumed CIC

[Scott Morrison]

There are equiconsistency results. Mario's thesis is a good place to start if you're interested in this: https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Treq]

Kevin Buzzard said:

Sure you can think of them as axioms. They don't have proofs after all. We've just assumed CIC

I suppose that's my question. Doesn't CIC just give us MyNat? That feels sort of proof-like to me.

This is sort of how I'm understanding this at the moment: Lean's dependent type theory has type forming rules that let you form a new type from constants and functions that create terms of that type. This is what allows NNG4 write something like inductive MyNat where ... and Lean can interpret MyNat as an inductive type. Is that not a sort of constructive proof from the point of view of CIC or am I thinking about this poorly?

My 1000" view is that Lean offers dependent function types, inductive types, and a hierarchy of universes with Prop at the bottom as it's axioms. Thereafter deductive rules basically define how terms are constructed and simplified. This foundation is enough to encode the propositional operators like ∧ ∨ ¬ → ↔ and objects like MyNat but there are things this simply can't do. For example, to encode a tactic like xyzzy, your system requires an additional axiom - after which it's easy to show your system is no longer sound.

[Kevin Buzzard]

Yes CIC just gives us MyNat.

[Mario Carneiro]

The things that a system "just gives us" are usually called axioms. If rules for inductives were tweaked just a bit it would allow you to have types like

inductive Foo where
  | mk : (Foo -> False) -> Foo

from which one can prove a contradiction.

[Treq]

Mario Carneiro said:

[...] from which one can prove a contradiction.

Ah, I see. Though, just to clarify... it's true (as far as we know) that introducing a new inductives (as they exist today) doesn't allow us to prove contradictions. It seems like otherwise we would be forever wondering if a formalization is hiding a contradiction.

[Mario Carneiro]

This is the content of my paper #leantt

[Mario Carneiro]

it's a surprisingly nontrivial claim (actually I suppose it's not that surprising that the claim would be complicated to prove). Probably an even better argument than the proof is the social proof: It's used as the basis for a proof assistant so there are many people with a vested interest in ensuring you can't prove false in it, and if the theory happens to be broken we'll fix the theory until it isn't broken anymore

[Treq]

Mario Carneiro said:

This is the content of my paper #leantt

Awesome. @Scott Morrison linked it last night and I've started reading it, though I'm a relative beginner in all this so it's a slow going process.

[Treq]

Also, yes - I don't really think the theory can be broken in any serious way. Or at least, I don't think I can. I'm not coming at this from a perspective of skepticism, just one curiosity. I've been reading a bit about syntax vs semantics and the role of axioms in various deductive systems. Just making sure I have the right ideas about what parts of the language are functioning in which capacity.

[Mario Carneiro]

I come from the perspective of someone who has found soundness bugs in lean and other systems in the past. Without a formal proof I don't have a very strong belief that the system is actually completely correct, while the social proof is more a reflection of the beliefs and goals of the community around the tool. (Which is part of why I've been working on https://github.com/digama0/lean4lean as a formalization of #leantt, because I am still not entirely convinced even though I am the one who wrote the paper proof.)

[Mario Carneiro]

#leantt is not really beginner reading though. Regarding terminology, in CIC we do not usually call inductive types axioms (even though with my proof theory hat on they absolutely are), and reserve that term for constants that have no "computation rules" associated to them (and in lean these are the ones you construct with the axiom keyword). Lean 4 also muddies the water here because it has a thing called opaque which are constants with no computation rules, but which do not incur any additional soundness burden because they are typechecked like a def, so you can only inhabit types that are already inhabitable.

[Treq]

Thanks you for your time. I think you've answered my questions very well and given me a bit of extra context too. :)