real number game

Stream: maths

[Kevin Buzzard]

People ask me about other games like natural number game, and I've suggested several in the past, but the one which seems to get the most attention is the real number game. Gavin Thomson, a student of David Corfield in Kent, was coming up to London to work with me on it for four months, arriving in May. Of course this is all now very much up in the air. But @Daniel Keys has also expressed an interest. I will try and get David onto Zulip and we'll see if we can coordinate something here. There is already a public repo but we are nowhere near a release.

My experience in writing these games is that for each concept you either import it from Lean (if you just want to use it) or write it from scratch. If you write it from scratch you want one file with all the definitions and the coercions and the notation and a basic API for mathematicians all in term mode, and tell the mathematician not to open it. And then you need a file full of theorems, some of which are sorried and where you can supply tactic mode proofs with steps which feel like about the same pace as a book might go if they were explaining the argument carefully. Sometimes this is a challenge to do in Lean, with "basic" maths steps which seem to be tough for beginners to formalise. Is more API needed in this case?

One thing I wanted to have in the natural number game was more than one sorry to fill in on a page, possibly with the later sorry depending on the first one. I sometimes felt this was a hindrance in NNG.

Does anyone have any comments on issues they had with the natural number game which we could perhaps avoid in the real number game? I am really hoping to be able to cut down on the number of words used in the tactic descriptions, or at least get them out of the way somehow so you can see the key definition at the top of my waffle, and the key lemma in the middle of it, whilst still being able to code in a small box at the bottom.

[Jiekai]

NNG meaning?

[Mario Carneiro]

natural number game

[Daniel Keys]

Doing things from scratch like in the NNG has the advantage of possibly being able to show the players more details. But working with Cauchy sequences or Dedekind cuts does seem quite a bit more far-fetched than Peano's axioms.
Using mathlib's capabilities in data.real.basic etc. might hide some foundational stuff but is naturally amenable to teaching the tools built by the community, which is also desirable.
Could a middle way be better in this case? For example, importing at each level (or as needed) in the game a file that imports, in turn, only the needed tools. Say import from bounds.lean just is_lub and a few other related items when working on results related to the supremum, then list them in the theorems on the left.

[Gavin Thomson]

Following! thanks for the invite Kevin :)
So I still want to help but I won't be up to speed for a few weeks at least. :( So I may be a bit clueless until then. I also should admit that I don't have any experience of working with real numbers in lean yet.

I think the question of how much is built from scratch and how much is imported maybe depends on who the RNG is aimed at?

I can only speak for my own experience of undergrad analysis, but I think we saw axioms for the reals first and then proceeded along the lines mentioned on the RNG page -- sups and infs, sequences and limits, series.

I thought the NNG was good for anyone who wanted a first taste of interactive theorem proving, undergrad or professional. But I guess seeing how to build an explicit construction from scratch would be more useful for professionals than students?
I see Kevin was looking at similar questions ages ago: https://leanprover-community.github.io/archive/116395maths/43084bounds.html

I agree that a second game could use less text -- my feeling was that the NNG had to give some motivation for tactics that might seem weird without any knowledge of the nuts and bolts of type theory, term rewriting etc. But I think anyone playing RNG should have played NNG.

[Kevin Buzzard]

How much will I have to hack lean 3 or mathlib to get things like (1,3] : set real to work? Lean's conventions for intervals are nowhere near what a mathematician is used to.

[Patrick Massot]

I use [a, b] : set real in my lectures, without hacking anything.

[Kevin Buzzard]

Oh nice

[Patrick Massot]

I didn't try with (1, 3] (which is a stupid notation anyway).

[Kevin Buzzard]

I'd be happy with ]1, 3]

[Kevin Buzzard]

Can you give me a link to some code or something?

[Patrick Massot]

notation `]`a`, `b`]` := Ioc a b
#check ]1, 3]

[Kevin Buzzard]

And this is ok in practice?

[Mario Carneiro]

noooo

[Kevin Buzzard]

I promise I'll never use lists

[Patrick Massot]

Same here.

[Kevin Buzzard]

Or tuples

[Mario Carneiro]

or commas

[Patrick Massot]

And I had no trouble at all using [a, b] to mean [a, b].

[Kevin Buzzard]

Yeah we don't use commas either

[Patrick Massot]

What's wrong with you software people?

[Mario Carneiro]

I will remind you that one place lists come up is in tactics

[Kevin Buzzard]

Hmm

[Kevin Buzzard]

I wish you'd just made up your own notation

[Patrick Massot]

That will be the ultimate parser test for @Sebastian Ullrich: can we use this notation in Lean 4 without destroying Lean?

[Mario Carneiro]

how dare us use ascii

[Mario Carneiro]

I'm pretty sure that this notation is ambiguous

[Kevin Buzzard]

Not if you have a sane unifier

[Kevin Buzzard]

Remember lists don't exist in maths departments

[Kevin Buzzard]

The notation for a list is $x_1, x_2, \ldots$

[Kevin Buzzard]

Who needs brackets

[Mario Carneiro]

well, you don't have to nest that expression in anything except for english text

[Mario Carneiro]

it's not so easy in a theorem prover

[Reid Barton]

We already use various forms of absolute value/norm which seem to work all right

[Reid Barton]

If you want all of [a, b], [a, b[, ]a, b[, ]a, b] to work that adds another twist though

[Sebastian Ullrich]

Yeah, that's a no. When you declare a notation/parser starting with ], Lean 4 will not accept [a, b] anymore.

[Kevin Buzzard]

And the English versions too

[Kevin Buzzard]

When is Lean 5?

[Reid Barton]

Mario how long have you been waiting to use :maple_leaf: