Has anyone published/written a \Z, \Q or \R game?

Stream: new members

[Kent Van Vels]

Quite a while ago now, I have followed the real analysis book by Terry Tao and rolled my own implementations of the integers, rationals and real numbers. In the book, he defines the integers as (equivalence classes)/quotients of two naturals, rationals as equivalence classes/quotients of integers, and the reals as equivalence classes/quotients (Cauchy sequences) of rationals. The proofs of showing commutivity, associativity, etc are (almost shockingly) straightforward using this approach. I also showed (at least for the integers and probably more, I haven't been in the code for a while) that my implementation was isomorphic to the mathlib versions. I

I am interested in publishing this as a game using the lean-game repo. I am asking for your comments and I am especially interested to know if something like this has been done already. A cursory web search hasn't found anything.

Thanks!

[Zhang Qinchuan]

There is a github repo for making Terry Tao's book a Lean game (check here).

But seems not yet finished.

[Kent Van Vels]

There is a github repo for making Terry Tao's book a Lean game (check here).

The link you provided was to this page. Did you mean to link to a different URL? Thanks.

[Kevin Buzzard]

I've thought about this in the past and my conclusions were that the natural number game was somehow intrinsically fun but the integer and rational number games were much harder to make fun, because every single proof about Int is "reduce it to a tedious question about Nat and then either do a nasty induction or use omega/nlinarith/polyrith" and then every single proof about Rat is "reduce it to a tedious question about Int and then use omega/nlinarith/polyrith" etc etc. My most recent effort to do this is here (both integers and rationals).

[Zhang Qinchuan]

Kent Van Vels said:

There is a github repo for making Terry Tao's book a Lean game (check here).

The link you provided was to this page. Did you mean to link to a different URL? Thanks.

Sorry, the github repo (https://github.com/melembroucarlitos/Tao_Analysis-LEAN) is 3 years ago and no longer updating.

[Luigi Massacci]

From the experience of doing this on paper, I have to agree with @Kevin Buzzard that these are just generally boring theorems to prove. Giving the construction is cool, but then proving the usual laws is just so mechanical (and all so similar among each other) that it’s hard to make it entertaining

[Luigi Massacci]

which is why it’s usually left as an exercise in textbooks…

[Luigi Massacci]

What might be more interesting is to make a game where you make different constructions of the real numbers (cauchy sequences, dedekind cuts, from the nonstandard rationals, Eudoxus, power series, …), and then prove them isomorphic?

[Luigi Massacci]

There was definitely someone that did the Eudoxus reals in lean at some point

[Kevin Buzzard]

I've had students do Eudoxus on at least two occasions and I think there have been more. I've never tried Dedekind but here's a tip: there's this reliance on < which is poorly behaved when multiplying by negative numbers. So my proposal for doing Dedekind would be: first make the British natural number game (start at 1 -- this has the potential to be as fun as NNG). Then make the positive rationals immediately as equivalence classes of pnat^2 (note that division is total). Then make the positive (or nonnegative) reals as Dedekind cuts. And then finally make the reals by inverting addition. This route introduces division before subtraction but I think it might solve the case split problems in the usual Dedekind cut approach. I've never checked though.

[Kent Van Vels]

I have been looking in the IUM repo. I can see why it might not be as fun a candidate for a game. I had fun doing the proofs though. I would have to look more at my files, but I think I did "bare hands" proofs, instead of linarith and the like, which were quite tedious but manageable. For me, part of the fun of the NNG was the fact that I couldn't use the powerful tactics. I also have don't understand exactly how linarith works so I it felt strange to use that to prove things about the integers that (I think) I understand pretty well.

I guess I am writing all this to get my thoughts straight and have a record of them. Ha.

@Kevin Buzzard thanks for the link. Since I followed your example on the Mod37 quotient space, my code (except for the tactics trickery, and in some cases much longer proofs) is very similar to yours. I wonder if doing the mod37 quotient space would be a good game. Do I have permission to glean through your code to make my code better? Thanks

[Kevin Buzzard]

You can use any of my code and you don't need to worry about giving me any credit. I write it to teach.

[Jireh Loreaux]

I did the real numbers via dedekind cuts about 4 years ago in Lean 3. I started from the rationals, but as Kevin suggested, I think it would have been nicer to start from positive rationals, then make the positive real numbers. You still end up need to do case splits at the end of the construction, but I'm relatively certain it would have been nicer than starting from ℚ. Multiplication of ℚ-dedekind cuts is a nightmare.

[Joseph Myers]

Kevin Buzzard said:

I've had students do Eudoxus on at least two occasions and I think there have been more. I've never tried Dedekind but here's a tip: there's this reliance on < which is poorly behaved when multiplying by negative numbers. So my proposal for doing Dedekind would be: first make the British natural number game (start at 1 -- this has the potential to be as fun as NNG). Then make the positive rationals immediately as equivalence classes of pnat^2 (note that division is total). Then make the positive (or nonnegative) reals as Dedekind cuts. And then finally make the reals by inverting addition. This route introduces division before subtraction but I think it might solve the case split problems in the usual Dedekind cut approach. I've never checked though.

Conway concludes the same thing in ONAG (p26 of the second edition): that if you use Dedekind cuts it's best to go via the positive reals.

[Yakov Pechersky]

I have to mention the de Bruijn reals which is mostly in #13964 and #13965. I never finished the proof of multiplication

[Johan Commelin]

I still think we should have "Real Number Battle": the shortest implementation of an instance of ConditionallyCompleteLinearOrderedFieldwins.

[Daniel Weber]

I think that'll be fun. With what imports?

[Johan Commelin]

If we really want to do this, we should minimalize the imports for the definition of that class.
And then a contestant is graded by the LoC needed beyond the import of that file.

[Daniel Weber]

Should the axioms also be minimized? I also don't think LoC is a good measure, you can do a lot of things in one line

[Johan Commelin]

Sure, no additional axioms beyond the 3 standard ones.

[Johan Commelin]

And every metric will have pros and cons. With LoC, I do want the < 100 chars-per-line limit.

[Johan Commelin]

But I'm happy to go with a metric like total amount of heartbeats, or build time, or something like that.

[Johan Commelin]

Whatever the codegolf guru's think is the best metric :smiley:

[Daniel Weber]

Johan Commelin said:

Sure, no additional axioms beyond the 3 standard ones.

I meant the ConditionallyCompleteLinearOrderedField "axioms", not the Lean axioms

[Daniel Weber]

Johan Commelin said:

Whatever the codegolf guru's think is the best metric :smiley:

I think the usual measure is number of bytes/characters

[Johan Commelin]

I think it's fine to minimize the axioms of ConditionallyCompleteLinearOrderedField yes. But Mathlib should have a proof that it still uniquely characterizes $\R$

[Daniel Weber]

I think I have a good minimization, I'll try to show it implies Mathlib's ConditionallyCompleteLinearOrderedField

[Daniel Weber]

Do we need 0⁻¹ = 0 there?

[Johan Commelin]

Yeah, I would think so. Otherwise you can't get uniqueness

[Johan Commelin]

Independently

chore(Order/ConditionallyCompleteLattice): split off Defs.lean from Basic.lean #19277

is doing a related import minimization by splitting a file.

[Johan Commelin]

@Daniel Weber What is the minimal axiomatization that you are proposing? Is it on a branch somewhere?

[Daniel Weber]

https://github.com/leanprover-community/mathlib4/blob/3cf535aa795f5f845e1440f14206317cd3cbf1a2/Mathlib/Algebra/Order/CompleteField.lean#L371

[Yakov Pechersky]

Looks like your order defns like sSup do not rely on the algebraic ones. So those could be factored out into another ofMinimalAxiom

[Johan Commelin]

Is this on some branch? I think this is sensible material for mathlib.

[Miguel Marco]

I think a real number game could be fun if the reals are not given by a construction, but just by stating that they are a totally ordered field with the axiom of the supremum. Then you have to deduce the properties (arquimedian, density of rationals, existence and density of irrationals, Bolzano theorem... ) by using the supremum property.

[Daniel Weber]

Yes, branch#CM_cclof. I could make a PR, but I think there could be other ofMinimalAxioms it would be cleaner to pass through

[Kevin Buzzard]

Miguel Marco said:

I think a real number game could be fun if the reals are not given by a construction, but just by stating that they are a totally ordered field with the axiom of the supremum. Then you have to deduce the properties (arquimedian, density of rationals, existence and density of irrationals, Bolzano theorem... ) by using the supremum property.

I've never tried this but this was the way I was taught the real numbers, and my initial reaction is that this idea could definitely be worth exploring.

[Miguel Marco]

Maybe a final boss could be proving that two such fields are isomorphic?

[Johan Commelin]

Or that one exists! :smiley:

[Daniel Weber]

Johan Commelin said:

Or that one exists! :smiley:

I think proving that one exists could be almost disjoint from proving properties about one from the axioms

[Johan Commelin]

It's still a boss though (-;

[Kevin Buzzard]

Existence of irrationals follows from intermediate value theorem. I think this is all worth following up. The art with a good game, I think, is to get all the levels in the right order; this is where all the thought (at my end) went into NNG (several other people thought about other things e.g. the interface! But hopefully most problems are solved here).

[Edward van de Meent]

existance of irrationals follows from a counting argument

[Edward van de Meent]

much simpler

[Johan Commelin]

Once you have a construction. But starting from the axioms, how do you start the counting argument?

[Johan Commelin]

It can certainly be done. But I'm not sure if it is much simpler.

[Edward van de Meent]

that's a fair point

[Miguel Marco]

The existence of the square root of two can be deduced from the supremum property. Its irrationality is a classical arithmetic problem (maybe out of scope for a real number game, though, but i guess it can be just a given theorem).

Once you have an irrational, the density of irrationals is a consequence of the archimedean property (plus some extra playing with the supremum property).

[Kevin Buzzard]

Miguel Marco said:

The existence of the square root of two can be deduced from the supremum property.

Sure -- I was just pointing out that it's probably not much harder to prove the IVT. In fact it might be easier to prove IVT because the supremum argument for sqrt(2) involves having to show that if x^2<2 then there's some epsilon>0 such that (x+epsilon)^2<2 and similarly for >, and these are slightly messy (not impossible, but they need doing, and they don't need doing for IVT, so the route via IVT and showing that polynomials are continuous is conceptually simpler).

[Yaël Dillies]

Kevin Buzzard said:

the supremum argument for sqrt(2) involves having to show that if x^2<2 then there's some epsilon>0 such that (x+epsilon)^2<2

Does it? Isn't the argument literally that the set is nonempty (0 ^ 2 < 2) and bounded above (if x ^ 2 < 2, then x ≤ 2)? I don't see any epsilon here!

[Kevin Buzzard]

You need it to prove that the sup satisfies x^2=2 (as opposed to < or >)

[Daniel Weber]

Is this a good thread to develop this idea, or should we move it somewhere else? We could make a list of theorems which would be fun to prove as a game

[Daniel Weber]

Given $\mathbb{R}$ it shouldn't be hard to develop $\mathbb{C}$, so we could also have a game goal of proving the fundamental theorem of algebra

[Mario Carneiro]

I actually asked a question on MSE about this once: What is the shortest proof that there is an irrational number?

[Mario Carneiro]

my takeaway is that the easiest proof is to show that sqrt(2) exists, which is easier than proving the reals are uncountable

[Mario Carneiro]

(proving that sqrt(2) is not rational is the easy part, proving it exists is the hard part)

[Kevin Buzzard]

Getting to $\mathbb{C}$ from $\R$ is https://github.com/ImperialCollegeLondon/complex-number-game (Lean 3) (instructions). I'm too busy proving FLT to get involved with this but you're welcome to use anything or everything there and I am not fussed about attribution