mathzoo

Stream: general

[Daniel Selsam]

We are excited to announce a new repository for recreational mathematics in Lean: mathzoo. Mathzoo is organized as a collection of "gems" that are both standalone (a short file that depends only on mathlib) and deadend (nothing will ever depend on it). The two main goals of the project are to be fun for students (& others) all over the world and to support AI research in mathematical problem solving.

To get started, we seeded mathzoo with the IMO problems in mathlib and with all of miniF2F. Please submit your favorite gems and spread the word.

[Jason Rute]

Is mathzoo going to stay up to date with mathlib?

[Junyan Xu]

Minimal maintainance. Gems need not be kept up-to-date with mathlib. Instead, every file must begin with a comment -- #mathlib YYYY-MM-DD <commit> indicating the last known commit against which the file will build.

[Daniel Selsam]

Jason Rute said:

Is mathzoo going to stay up to date with mathlib?

The official policy (discussed in the README) is that each gem must start with a "-- #mathlib YYYY-MM-DD <commit>" line indicating a commit that it is known to compile against, and that gems need not necessarily be kept-up-to-date. We will try to keep everything up-to-date but will not be able to guarantee this (depending on the number and diversity of submissions).

[Adam Topaz]

I guess one more thing to note is that there seems to be no CI in this repo. I suppose the honor code applies for those who want to submit something?

[Daniel Selsam]

Adam Topaz said:

I guess one more thing to note is that there seems to be no CI in this repo. I suppose the honor code applies for those who want to submit something?

We will add CI as soon as we can -- depending on the rate of submissions in the meantime, I may just manually check them.

[Jason Rute]

So you won’t allow sorrys? That can definitely mess with AI training.

[Daniel Selsam]

Jason Rute said:

So you won’t allow sorrys? That can definitely mess with AI training.

The plan is to allow axiom for statements without proof, but not allow "half-proofs" with sorries in them. Can you please explain your concern?

[Jason Rute]

Just that if you mine training data from proofs, you have to be careful to avoid training on proofs with sorry or your model might start to predict it. It is true there are a number of points that you can catch sorries and if it is literally sorry it is easy to filter. The synonyms can be harder to find and account for.

[Jason Rute]

I explain some more of the difficulties here: https://github.com/openai/lean-gym/issues/7

[Reid Barton]

For axioms you don't have this credit attribution problem at least, right? Because if the model tries to use an axiom that isn't there, it will fail immediately and not at the final kernel check.
Another perspective is that mathlib changes all the time anyways, and an axiom is just a lemma that we imported from a future version of mathlib.

[Reid Barton]

The rule could be something like "only allow axioms that are actually true" (e.g. definitely not axiom f : False).

[Eric Rodriguez]

axiom iutt : abc_conjecture? ;b I feel like this can easily fall into traps if we're not careful, such as binder-order nonsense

[Daniel Selsam]

@Bhavik Mehta suggested encoding statements as def ... : Prop := ... rather than axiom, which would let us avoid axioms but they are more cumbersome to change into theorems since you end up with all variables on the right of the colon.

[Daniel Selsam]

@Reid Barton This is not explicit in the README but I was assuming any axiom would be a deadend, i.e. just encode a yet-to-be-proven statement, and would not be allowed to be used in a later proof in the gem. Using def would preempt this issue entirely.

[Daniel Selsam]

Jason Rute said:

Just that if you mine training data from proofs, you have to be careful to avoid training on proofs with sorry or your model might start to predict it.

Isn't this an argument for not allowing sorrys in the zoo?

[Reid Barton]

Yeah I hadn't read the whole README yet, I thought this was about using axioms in proofs. If axiom is being used to formalize conjectures rather than prove things then maybe that should be explicit metadata somewhere, or maybe we just say that axiom is self-describing as being for this purpose.

[Reid Barton]

I guess once upon a time there was conjecture, right?

[Daniel Selsam]

A conjecture command that is sugar for def ... : Prop := ... might work. Another option is to just go back to not allowing statements without proofs.

[Reid Barton]

I think the status quo is fine--I assume it's easy enough for anyone processing Lean input to just ignore axiom declarations

[Reid Barton]

From what I understand, implementing a def-like command is not that trivial.

[Reid Barton]

Might be worth clarifying whether "sorry-free" also means without adding axioms.

[Reid Barton]

BTW, I'm a fan of the boldly incongruous terminology "zoo" and "gem".

[Daniel Selsam]

Reid Barton said:

BTW, I'm a fan of the boldly incongruous terminology "zoo" and "gem".

:laughing: @Rob Lewis commented on this as well -- if anyone has a candidate for a good, congruent pair of names (one for the repo, one for the individual problems) it isn't too late to change. I personally like "mathzoo" and "gem" so much individually that I am willing to overlook the incongruity.

[Jason Rute]

@Daniel Selsam sorry my original statement was ambiguous of where the negative was. Sorry can mess things up and removing them is good. I think you are doing it correctly. Sorry for the confusion.

[Matthew Ballard]

mathagerie/specimath ?

[Daniel Selsam]

MathGems could work but mathgems looks "phlegmy" to me.

[Rob Lewis]

I had suggested MathMine, but the metaphor is backwards, you don't put gems into a mine. It also has echoes of bitcoin

[Rob Lewis]

And it's fun to imagine Daniel as a zookeeper with a diamond-studded zookeeper's hat

[Mario Carneiro]

if it's a zoo, then wouldn't the files be exhibits?

[Adam Topaz]

(deleted)

[Adam Topaz]

(I'm not insinuating anything about the actual content of the gems.)

[Mario Carneiro]

Oh my, is it a backhanded compliment for high-schooler proofs?

[Adam Topaz]

Mario Carneiro said:

Oh my, is it a backhanded compliment for high-schooler proofs?

Sorry... too much potential for that joke to be taken the wrong way...

[Adam Topaz]

In any case, do you think the word "gem" might confuse some ruby folks?

[Adam Topaz]

I don't know anything about ruby except for the fact that they use "gems"

[Yakov Pechersky]

Gems remind of "functional pearls" from Haskell and other places

[Adam Topaz]

Oh yeah!

[Kyle Miller]

I thought of Ruby gems, too, but then it reminded me of functional pearls as well, and in any case it's not a library of libraries in the same way as ruby gems.

[Kyle Miller]

I like how at https://complexityzoo.net/Complexity_Zoo they have a zookeeper, a veterinarian, and a conservationist.

[Rob Lewis]

ITP uses "proof pearl" in its call for papers: "concise and elegant worked examples of formalizations (proof pearls)"

[Kyle Miller]

Mario Carneiro said:

if it's a zoo, then wouldn't the files be exhibits?

GEMs Exhibit Mathematics